Is there a more modern account of the main results of "Adding Dependent Choice" by D. Pincus? I would like to read Pincus' article Adding dependent choice, where he proves, among other things, the consistency of the theory $\mathsf{ZF+DC+O+\neg AC}$, where $\mathsf{DC}$ stands for Dependent Choice and $\mathsf{O}$ is the linear ordering principle, i.e. the statement "Every set can be linearly ordered". But in this paper Pincus uses Cohen's original presentation of forcing, which makes it (at least to me) hard to read.
Is there any newer account on his proof (in a thesis, paper etc.), which uses a more modern approach to forcing?
Thanks!
 A: No.
Most of the work of Pincus that involved these sort of iterated constructions, where one "pushes the counterexamples out" has never been reworked into modern terms.
In my Ph.D. one of the reasons to develop the notion of an iteration of symmetric extensions was to help and simplify these proofs (also the works of Gershon Sageev). If you look closely, you will see that this is not just presented in the "old method of forcing", but it is also from an era where the distinction between generic and symmetric extension wasn't fully explained in texts (indeed, you can find even papers from the early '80s that refer to what is clearly a symmetric extension as a "generic extension").
Unfortunately, so far, nobody has wanted to take on this mantle, and I have a lot on my hands as it is. I am happy to collaborate or give advice, if anyone wants to go for it.

Let me give a broad reason as to why I expect these results to fit so well into my work. Just in case it's not very clear.
Many of the complicated choice-related constructions of the time (Morris' model, Pincus' work, Sageev's work, and others) were written before a very clear understanding of forcing, iterations, and symmetric extensions. Morris' thesis, with this regards, is particularly amazing, since he's quite literally iterating symmetric extension is a very non-trivial fashion.
But when you read these, it becomes very apparent that the constructions are usually of the form "take a symmetric extension to fix some problems, then repeat", with some kind of understanding of a symmetry-based structure at limit steps.
In Sageev's work, each step is itself an iteration of symmetric extensions.
So, yes, without looking very closely, I do expect that Pincus' work will fit into the iteration framework. It may very well be necessary to extend the current understanding of the framework, which is something that I am slowly doing with one of my postdocs, Jonathan Schilhan, but at the end, if we have a general technique for iterating symmetric extensions, then a result constructed as an iteration of symmetric extensions should fit into the framework.
