prooftrees (30sep19)

git-svn-id: svn://tug.org/texlive/trunk@52221 c570f23f-e606-0410-a88d-b1316a301751

6 files changed, 266 insertions, 110 deletions

diff --git a/Master/texmf-dist/doc/latex/prooftrees/README b/Master/texmf-dist/doc/latex/prooftrees/README
index 94b50f64ae3..687eddf510f 100644
--- a/Master/texmf-dist/doc/latex/prooftrees/README
+++ b/Master/texmf-dist/doc/latex/prooftrees/README
@@ -1,4 +1,4 @@
-%% Copyright 2017 Clea F. Rees
+%% Copyright 2019 Clea F. Rees
 %
 % This work may be distributed and/or modified under the
 % conditions of the LaTeX Project Public License, either version 1.3
@@ -14,7 +14,7 @@
 %
 % This work consists of all files listed in manifest.txt.
 
-This package supports drawing proof trees of the kind often used in
+This package supports drawing tableaux (proof trees) of the kind often used in
 introductory logic classes, especially those aimed at students without strong
 mathemtical backgrounds. Hodges (1991) is one example of a text which uses
 this system. When teaching such a system it is especially useful to annotate
@@ -27,13 +27,13 @@ system is provided for trees which cite line numbers in justifications for
 proof lines or branch closures.
 
 prooftrees is based on Forest and, hence, TikZ. The package requires version
-2.0.3 of Forest for expected results and will not work with version 1.
+2.1+ of Forest for expected results and will not work with version 1.
 
 The author is certain  that some of her beliefs are false, but sure that her
 belief that prooftrees has bugs is not among them.  
 
 Clea F. Rees
 ReesC21 <at> cardiff <dot> ac <dot> uk
-2017/02/08
+2019/09/30
 
 vim: set nospell: 
diff --git a/Master/texmf-dist/doc/latex/prooftrees/manifest.txt b/Master/texmf-dist/doc/latex/prooftrees/manifest.txt
index 8b50e4118f8..6d7b0c4628a 100644
--- a/Master/texmf-dist/doc/latex/prooftrees/manifest.txt
+++ b/Master/texmf-dist/doc/latex/prooftrees/manifest.txt
@@ -1,4 +1,4 @@
-Copyright 2016 Clea F. Rees
+Copyright 2019 Clea F. Rees
 
 This work may be distributed and/or modified under the conditions of the LaTeX Project Public License, either version 1.3 of this license or (at your option) any later version.  The latest version of this license is in http://www.latex-project.org/lppl.txt and version 1.3 or later is part of all distributions of LaTeX version 2005/12/01 or later.
 
diff --git a/Master/texmf-dist/doc/latex/prooftrees/prooftrees.pdf b/Master/texmf-dist/doc/latex/prooftrees/prooftrees.pdf
index 5ab39f88c1d..65c57dc0b39 100644
--- a/Master/texmf-dist/doc/latex/prooftrees/prooftrees.pdf
+++ b/Master/texmf-dist/doc/latex/prooftrees/prooftrees.pdf
diff --git a/Master/texmf-dist/doc/latex/prooftrees/prooftrees.tex b/Master/texmf-dist/doc/latex/prooftrees/prooftrees.tex
index bf00703e2f1..57f9dc05c5d 100644
--- a/Master/texmf-dist/doc/latex/prooftrees/prooftrees.tex
+++ b/Master/texmf-dist/doc/latex/prooftrees/prooftrees.tex
@@ -1,4 +1,4 @@
-%% Copyright 2017 Clea F. Rees
+%% Copyright 2019 Clea F. Rees
 %
 % This work may be distributed and/or modified under the
 % conditions of the LaTeX Project Public License, either version 1.3
@@ -20,7 +20,7 @@
 %%
 \pdfminorversion=7
 \RequirePackage{svn-prov}
-\ProvidesFileSVN{$Id: prooftrees.tex 5848 2017-02-09 02:15:38Z cfrees $}[v0.6 \revinfo]
+\ProvidesFileSVN{$Id: prooftrees.tex 8642 2019-09-30 00:20:55Z cfrees $}[v0.7 \revinfo]
 \GetFileInfoSVN*
 \let\prooftreesdocversion\fileversion
 \let\prooftreesdocbase\filebase
@@ -291,7 +291,7 @@
 % It could at least do us the favour of holding some of its much less defensible and much more inconvenient design decisions in equal contempt!!
 \defbibheading{bibliography}[\refname]{%
   \section*{#1}%
-  \markboth{#1}{#1}}
+  \markboth{#1}{}}
 
 \makeindex
 
@@ -315,7 +315,7 @@
 \bigskip
 
 \begin{figure}[!b]
-\begin{adjustwidth}{-2em}{-2em}
+\begin{adjustwidth}{-3em}{-5em}
   \centering
   \begin{minipage}[t]{.475\linewidth}
     \begin{prooftree}
@@ -387,7 +387,7 @@
           ]
         ]
       ]
-    \end{prooftree}
+    \end{prooftree}%
   \end{minipage}\hfill
   \begin{minipage}[t]{.525\linewidth}
     \begin{prooftree}
@@ -441,8 +441,8 @@
           ]
         ]
       ]
-    \end{prooftree}
-  \end{minipage}
+    \end{prooftree}%
+  \end{minipage}%
 \end{adjustwidth}
 \end{figure}
 
@@ -1488,6 +1488,22 @@ The following options affect the global style of the tree and should typically b
 The default values for the document can be set outside the \env{prooftree} environment using \cs{forestset}\marg{settings}.
 If \emph{only} proof trees will be typeset, a default style can be configured using \pkg{forest}'s \keyname*[fkeylist]{default preamble}.
 
+\DescribeKeys[fregbool]{auto move, not auto move}\vals{true,false}\AfterLastParam
+\Default{true}
+Determines whether \pkg{prooftrees} will move lines automatically, where possible, to avoid combining different justifications when different branches are treated differently.
+The default is to avoid conflicts automatically where possible.
+Turning this off permits finer-grained control of what gets moved using \keyname[fstyle]{move by}.
+The following are equivalent to the default setting:
+\begin{latexcode}
+  auto move
+  auto move=true
+\end{latexcode}
+Either of the following will turn auto move off:
+\begin{latexcode}
+  not auto move
+  auto move=false
+\end{latexcode}
+
 \DescribeKeys[fregbool]{line numbering, not line numbering}\vals{true,false}\AfterLastParam
 \Default{true}
 This determines whether lines should be numbered.
@@ -1558,6 +1574,12 @@ Distance between the symbol marking branch closure and any following annotation.
 If the format of such annotations is changed with \keyname[fregkeylist]{close format}, this dimension may require adjustment.
 \Example{close sep=\cs{baselineskip}}
 
+\DescribeKey[fregdim]{proof tree inner proof width}\val{dimension}\AfterLastParam
+\Default{0pt}
+
+\DescribeKey[fregdim]{proof tree inner proof midpoint}\val{dimension}\AfterLastParam
+\Default{0pt}
+
 \DescribeKey[fregcount]{line no shift}\val{integer}\AfterLastParam
 \Default{0}
 This value increments or decrements the number used for the first line of the proof.
@@ -1862,6 +1884,18 @@ Unless \keyname[fregkeylist]{wff format} is set to a non-default value, the foll
 Additional \TikZ{} keys to apply to this proof line.
 \Example{line options=\arg{draw, rounded corners}}
 
+\DescribeKey[fstyle]{line no override}\val{text}\AfterLastParam
+Substitute \meta{text} for the programmatically-assigned line number.
+\meta{text} will be wrapped by \keyname[macro]{\cs{linenumberstyle}}, so should not be anything which would not make sense in that context.
+\Example{line no override=\arg{n}}
+
+\DescribeKey[fstyle]{no line no}\AfterLastParam
+Do not typeset a line number for this line.
+Intended for use in trees where \keyname[foptbool]{line numbering} is activated, but some particular line should not have its number typeset.
+Note that the number for the line is still assigned and the node which would otherwise contain that number is still typeset.
+If the next line is automatically numbered, the line numbering will, therefore, ‘jump’, skipping the omitted number.
+\Example{no line no}
+
 % END subsec:lo
 % END sec:ops
 
@@ -1899,7 +1933,24 @@ This allows you to use \env{tableau} for \pkg{prooftrees} trees and \env{prooftr
 \section{Version History}\label{sec:hanes}
 % BEGIN sec:hanes
 
+\subsection*{0.7}\label{subsec:v0.7}
+
+% BEGIN subsec:v0.7
+
+Implement \keyname[fregbool]{auto move}.
+See \cref{subsec:go}.
+The main point of this option is to allow automatic moves to be switched off if one teaches students to first apply  all available non-branching rules for the tableau as a whole, as opposed to all non-branching rules for the sub-tree.
+The automatic algorithm is consistent with the latter, but not former, approach.
+The algorithm favours compact trees, which are more likely to fit on \pkg{beamer} slides.
+Switching the algorithm off permits users to specify exactly how things should or should not be move.
+Thanks to Peter Smith for prompting this.
+
+Fix bug reported at \href{https://tex.stackexchange.com/q/479263/39222}{tex.stackexchange.com/q/479263/39222}.
+
+% END subsec:v0.7
+
 \subsection*{0.6}\label{subsec:v0.6}
+
 % BEGIN subsec:v0.6
 
 Add compatibility option for use with \pkg{bussproofs}.
diff --git a/Master/texmf-dist/doc/latex/prooftrees/prooftrees_biber.bib b/Master/texmf-dist/doc/latex/prooftrees/prooftrees_biber.bib
index c2c6dba09b1..6d21cca4df9 100644
--- a/Master/texmf-dist/doc/latex/prooftrees/prooftrees_biber.bib
+++ b/Master/texmf-dist/doc/latex/prooftrees/prooftrees_biber.bib
@@ -1,27 +1,27 @@
 @BOOK{hodges-logic,
   AUTHOR = {Hodges, Wilfred},
-  ISBN = {0140136363},
   PUBLISHER = {Penguin},
+  DATE = {1977, 1991},
+  ISBN = {0140136363},
   TITLE = {Logic: An Introduction to Elementary Logic},
-  YEAR = {1977, 1991},
-}
-
-@MANUAL{saso-forest-manual,
-  AUTHOR = {Živanović, Sašo},
-  DATE = {2016-03-04},
-  EDITION = {2.0.2},
-  KEYWORDS = {TeX, LaTeX, PGF, TikZ, Forest},
-  TITLE = {Forest: A {PGF}/Ti\mkbibemph{k}{Z}-Based Package for Drawing Linguistic Trees},
-  URL = {http://spj.ff.uni-lj.si/zivanovic/},
 }
 
 @MANUAL{tantau-tikz-pgf-manual,
   AUTHOR = {Tantau, Till},
+  URL = {http://sourceforge.net/projects/pgf},
   DATE = {2015-08-29},
   EDITION = {3.0.1a},
-  KEYWORDS = {TeX, LaTeX, PGF, TikZ},
+  KEYWORDS = {TeX,LaTeX,PGF,TikZ},
   SUBTITLE = {Manual for Version 3.0.1a},
   TITLE = {The {T}i\mkbibemph{k}{Z} and {PGF} Packages},
-  URL = {http://sourceforge.net/projects/pgf},
+}
+
+@MANUAL{saso-forest-manual,
+  AUTHOR = {Živanović, Sašo},
+  URL = {http://spj.ff.uni-lj.si/zivanovic/},
+  DATE = {2016-03-04},
+  EDITION = {2.0.2},
+  KEYWORDS = {TeX,LaTeX,PGF,TikZ,Forest},
+  TITLE = {Forest: A {PGF}/Ti\mkbibemph{k}{Z}-Based Package for Drawing Linguistic Trees},
 }
 
diff --git a/Master/texmf-dist/tex/latex/prooftrees/prooftrees.sty b/Master/texmf-dist/tex/latex/prooftrees/prooftrees.sty
index fbe1ca2af31..2f0e2a2a260 100644
--- a/Master/texmf-dist/tex/latex/prooftrees/prooftrees.sty
+++ b/Master/texmf-dist/tex/latex/prooftrees/prooftrees.sty
@@ -1,4 +1,4 @@
-%% Copyright 2017 Clea F. Rees
+%% Copyright 2019 Clea F. Rees
 %
 % This work may be distributed and/or modified under the
 % conditions of the LaTeX Project Public License, either version 1.3
@@ -16,7 +16,7 @@
 %%
 \NeedsTeXFormat{LaTeX2e}
 \RequirePackage{svn-prov}
-\ProvidesPackageSVN{$Id: prooftrees.sty 5848 2017-02-09 02:15:38Z cfrees $}[v0.6 \revinfo]
+\ProvidesPackageSVN{$Id: prooftrees.sty 8641 2019-09-29 23:57:27Z cfrees $}[v0.7 \revinfo]
 \RequirePackage{etoolbox}
 % define \prooftrees@enw to hold the name of the environment
 % default is to name the environment prooftree, this ensures backwards compatibility
@@ -44,18 +44,28 @@
   not justifications,% default is for no line justifications (b/c there's no point in enabling this if the user doesn't specify any content)
   declare boolean register={single branches},% single branches: explicitly drawn branches and a normal level distance between lone children and their parents
   not single branches,% default is for lone children to be grouped with their parents
+  declare boolean register={auto move},% ble mae'n bosibl, symud pethau'n awtomatig
+  auto move,% default: symud yn awtomatig
   declare dimen register={line no width},% default will be set to the width of 99 wrapped in the line numbering style
   line no width'=0pt,% fallback default is 0pt
   declare dimen register={just sep},% amount by which to shift justifications away from the main tree
   just sep'=1.5em,% default is 1.5em
+  declare dimen register={just dist},% distance of justifications from centre of inner tree; overrides just sep
+  just dist'=0pt,
   declare dimen register={line no sep},% amount by which to shift line numbers away from the main tree
   line no sep'=1.5em,
+  declare dimen register={line no dist},% distance of line nos. from centre of inner tree; overrides line no sep
+  line no dist'=0pt,
   declare dimen register={close sep},% distance between closure symbols and any following annotation
   close sep'=.75\baselineskip,
   declare dimen register={proof tree line no x},
   proof tree line no x'=0pt,
   declare dimen register={proof tree justification x},
   proof tree justification x'=0pt,
+  declare dimen register={proof tree inner proof width},
+  proof tree inner proof width'=0pt,
+  declare dimen register={proof tree inner proof midpoint},
+  proof tree inner proof midpoint'=0pt,
   declare count register={proof tree rhif lefelau},% count the levels in the proof tree
   proof tree rhif lefelau'=0,
   declare count register={proof tree lcount},% count the line numbers (on the left)
@@ -336,11 +346,28 @@
               },
             }{},
           },
+          proof tree inner proof midpoint/.min={>{OOw2+d}{x}{min x}{##1+##2}}{fake=root,descendants},
+          proof tree inner proof width/.max={>{OOw2+d}{x}{max x}{##1+##2}}{fake=root,descendants},
+          proof tree inner proof width-/.register=proof tree inner proof midpoint,
+          proof tree inner proof midpoint+/.process={Rw+d{proof tree inner proof width}{##1/2}},
         }{},
         if line numbering={% get the x position of line numbers and adjust the location and alignment of the proof statement
           proof tree line no x/.min={>{OOw2+d}{x}{min x}{##1+##2}}{fake=root,descendants},
+          if={%
+            > Rd= {line no dist}{0pt}%
+          }{%
+            proof tree line no x-/.register=line no sep,
+          }{%
+            tempdima/.register=proof tree inner proof width,
+            tempdima:=2,
+            if={%
+              > RR< {line no dist}{tempdima}%
+            }{}{%
+              proof tree line no x/.register=proof tree inner proof midpoint,
+              proof tree line no x-/.register=line no dist,
+            },
+          },
           proof tree line no x-/.register=line no width,
-          proof tree line no x-/.register=line no sep,
           for root={%
             tempdimc/.option=x,
             x'+/.register=proof tree line no x,
@@ -360,7 +387,20 @@
         }{},
         if justifications={% get the x position of justifications and create the nodes which will hold the justification content, if required
           proof tree justification x/.max={>{OOw2+d}{x}{max x}{##1+##2}}{fake=root,descendants},
-          proof tree justification x+/.register=just sep,
+          if={%
+            > Rd= {just dist}{0pt}%
+          }{%
+            proof tree justification x+/.register=just sep,
+          }{%
+            tempdima/.register=proof tree inner proof width,
+            tempdima:=2,
+            if={%
+              > RR< {just dist}{tempdima}%
+            }{}{%
+              proof tree justification x/.register=proof tree inner proof midpoint,
+              proof tree justification x+/.register=just dist,
+            },
+          },
           append={%
             [,
               proof tree line justification,
@@ -390,96 +430,100 @@
       },
     },
     proof tree ffurf={% processed before proof tree symud auto: adjusts the alignment of lines when some levels of the tree are grouped together either whenever the number of children is only 1 or by applying the grouped style to particular nodes when specifying the tree
-      if single branches={%
-        where={%
-          >{O! _O< O &&}{grouped}{2}{level}{proof tree rhifo}%
-        }{%
-          if={%
-           >{_O= _O< &}{1}{!parent.n children}{1}{!parent,parent.n children}%
+      if auto move={%
+        if single branches={%
+          where={%
+            >{O! _O< O &&}{grouped}{2}{level}{proof tree rhifo}%
           }{%
-            not tempboola,
-            for root/.process={Ow1}{level}{%
-              for level={##1}{%
-                if={%
-                 >{_O< _O= &}{1}{!parent.n children}{1}{n}%
-                }{%
-                  tempboola,
-                }{},
-              },
-            },
-            if tempboola={%
-              proof tree toing,
-            }{},
-          }{},
-        }{},
-      }{},
-      where={%
-       >{O _O< O &&}{grouped}{1}{level}{proof tree rhifo}%
-      }{% this searches for certain kinds of structural asymmetry in the tree and attempts to move lines appropriately in such cases - the algorithm is intended to be relatively conservative (not in the sense of 'cautious' or 'safe' but in the sense of 'reflection of the overlapping consensus of reasonable users' / 'what would be rationally agreed behind the prooftrees veil of ignorance'; apologies for the inconvenience if you are an unreasonable user)
-        not tempboola,
-        for root/.process={Ow1}{level}{%
-          for level={##1}{%
             if={%
-             >{_O< _O= &}{1}{!parent.n children}{1}{n}%
-            }{%
-              tempboola,
-            }{},
-          },
-        },% Sašo:  http://chat.stackexchange.com/transcript/message/27874731#27874731, see also http://chat.stackexchange.com/transcript/message/27874722#27874722
-        if tempboola={%
-          if n children=0{%
-            if={>{OO|}{!parent.proof tree toing}{!parent.proof tree toing with}}{% we're already moving the parent and the child will move with the parent, so we can just mark this and do nothing else
-              proof tree toing with,
+              >{_O= _O< &}{1}{!parent.n children}{1}{!parent,parent.n children}%
             }{%
-              for root/.process={Ow1}{level}{% don't move a terminal node even in case of asymmetry: instead, create a separate proof line for terminal nodes on this level which are only children, by moving children with siblings on this level down a proof line, without altering their physical location
-                % this makes the tree more compact and stops it looking silly
+              not tempboola,
+              for root/.process={Ow1}{level}{%
                 for level={##1}{%
                   if={%
-                   >{_O< _O= &}{1}{!parent.n children}{1}{n}%
-                  }{% this just serves to keep the levels nice for the sub-tree and ensure things align. We need this because we want to skip a level here to allow room for the terminal node in the other branch
-                    for parent={%
-                      if proof tree rhiant cymysg={}{% we mark the parent to avoid increasing the line number of its descendants more than once
-                        proof tree rhiant cymysg,
-                        for descendants={%
-                          proof tree toing by'+=1,
-                        },
-                      },
-                    },
+                    >{_O< _O= &}{1}{!parent.n children}{1}{n}%
+                  }{%
+                    tempboola,
                   }{},
                 },
-              },% Sašo:  http://chat.stackexchange.com/transcript/message/27874731#27874731, see also http://chat.stackexchange.com/transcript/message/27874722#27874722
+              },
+              if tempboola={%
+                proof tree toing,
+              }{},
+            }{},
+          }{},
+        }{},
+        where={%
+          >{O _O< O &&}{grouped}{1}{level}{proof tree rhifo}%
+        }{% this searches for certain kinds of structural asymmetry in the tree and attempts to move lines appropriately in such cases - the algorithm is intended to be relatively conservative (not in the sense of 'cautious' or 'safe' but in the sense of 'reflection of the overlapping consensus of reasonable users' / 'what would be rationally agreed behind the prooftrees veil of ignorance'; apologies for the inconvenience if you are an unreasonable user)
+          not tempboola,
+          for root/.process={Ow1}{level}{%
+            for level={##1}{%
+              if={%
+                >{_O< _O= &}{1}{!parent.n children}{1}{n}%
+              }{%
+                tempboola,
+              }{},
             },
-            no edge,
-          }{%
-            if={%
-             >{_O= _O< &}{1}{!parent.n children}{1}{!parent,parent.n children}%
-            }{% don't try to move if the node has more than 1 child or the grandparent has no more than that; otherwise, mark the node as one to move - we figure out where to move it later
-              proof tree toing,
-            }{no edge},
-          },
-        }{no edge},
+          },% Sašo:  http://chat.stackexchange.com/transcript/message/27874731#27874731, see also http://chat.stackexchange.com/transcript/message/27874722#27874722
+          if tempboola={%
+            if n children=0{%
+              if={>{OO|}{!parent.proof tree toing}{!parent.proof tree toing with}}{% we're already moving the parent and the child will move with the parent, so we can just mark this and do nothing else
+                proof tree toing with,
+              }{%
+                for root/.process={Ow1}{level}{% don't move a terminal node even in case of asymmetry: instead, create a separate proof line for terminal nodes on this level which are only children, by moving children with siblings on this level down a proof line, without altering their physical location
+                  % this makes the tree more compact and stops it looking silly
+                  for level={##1}{%
+                    if={%
+                      >{_O< _O= &}{1}{!parent.n children}{1}{n}%
+                    }{% this just serves to keep the levels nice for the sub-tree and ensure things align. We need this because we want to skip a level here to allow room for the terminal node in the other branch
+                      for parent={%
+                        if proof tree rhiant cymysg={}{% we mark the parent to avoid increasing the line number of its descendants more than once
+                          proof tree rhiant cymysg,
+                          for descendants={%
+                            proof tree toing by'+=1,
+                          },
+                        },
+                      },
+                    }{},
+                  },
+                },% Sašo:  http://chat.stackexchange.com/transcript/message/27874731#27874731, see also http://chat.stackexchange.com/transcript/message/27874722#27874722
+              },
+              no edge,
+            }{%
+              if={%
+                >{_O= _O< &}{1}{!parent.n children}{1}{!parent,parent.n children}%
+              }{% don't try to move if the node has more than 1 child or the grandparent has no more than that; otherwise, mark the node as one to move - we figure out where to move it later
+                proof tree toing,
+              }{no edge},
+            },
+          }{no edge},
+        }{},
       }{},
     },
     proof tree symud awto={% processed before typesetting nodes: if _this_ could be done during packing, that would be very nice, even if the previous stuff can't be
-      proof tree aros'=0,
-      for proof tree symud={%
-        if proof tree toing={% this relies on an experimental feature of forest, which is anffodus
-          for nodewalk={fake=parent,fake=sibling,descendants}{do dynamics},
-          delay n={\foresteregister{proof tree aros}}{%
-            tempcounta/.max={>{OOOOw4+n}{level}{proof tree toing by}{proof tree toooing}{proof tree rhifo}{(##1+##2+##3)*##4}}{parent,sibling,descendants},
-            if tempcounta>=1{%
-              if={%
-               >{Rw1+n OOw2+n >}{tempcounta}{##1+1}{level}{proof tree toing by}{##1+##2}%
-              }{%
-                tempcounta-/.option=level,
-                tempcounta'+=1,
-                move by/.register=tempcounta,
+      if auto move={%
+        proof tree aros'=0,
+        for proof tree symud={%
+          if proof tree toing={% this relies on an experimental feature of forest, which is anffodus
+            for nodewalk={fake=parent,fake=sibling,descendants}{do dynamics},
+            delay n={\foresteregister{proof tree aros}}{%
+              tempcounta/.max={>{OOOOw4+n}{level}{proof tree toing by}{proof tree toooing}{proof tree rhifo}{(##1+##2+##3)*##4}}{parent,sibling,descendants},
+              if tempcounta>=1{%
+                if={%
+                  >{Rw1+n OOw2+n >}{tempcounta}{##1+1}{level}{proof tree toing by}{##1+##2}%
+                }{%
+                  tempcounta-/.option=level,
+                  tempcounta'+=1,
+                  move by/.register=tempcounta,
+                }{no edge},
               }{no edge},
-            }{no edge},
-          },
-          proof tree aros'+=4,
-        }{},
-      },
+            },
+            proof tree aros'+=4,
+          }{},
+        },
+      }{},
     },
     proof tree nodiadau={% processed after proof tree creu nodiadau and before before drawing tree: creates annotation content which may include cross-references, applies highlighting and additional TikZ keys to line numbers, justifications and to wffs where specified for entire proof lines
       where proof tree crefs={}{}{% resolve cross-refs in closures
@@ -605,7 +649,16 @@
       for tree={%
         if={%
          >{O _O< &}{grouped}{1}{level}%
-        }{l'=\baselineskip}{},
+       }{% osgoi overlapping nodes, if posibl: cwestiwn https://tex.stackexchange.com/q/456254/
+         not tempboola,
+         tempcounta/.option=level,
+         tempcountb/.option=proof tree toing,
+         tempcountb+/.option=proof tree toooing,
+         for nodewalk={fake=root, descendants}{if={> RO= On>  O! O! OOw2+nR= &&&&
+             {tempcounta}{level} {!u.n children}{1} {proof tree arweinydd} {proof tree phantom} {proof tree toing by} {proof tree toooing}{##1+##2} {tempcountb}
+           }{tempboola}{}},
+         if tempboola={}{l'=\baselineskip},
+       }{},
       },
     },
     before drawing tree={% set final alignment for proof lines which have been moved by effectively grouping lead nodes and moving their subtrees accordingly - this requires that each line number and justification be the child of the previous one and that if justifications are used at all, then justifications exist for all proof lines, even if empty
@@ -654,6 +707,27 @@
           }{},
         },
       }{},
+      if={%
+        > RR| {auto move}{single branches}%
+      }{}{%
+        where proof tree arweinydd={%
+          for nodewalk={%
+            save append={proof tree walk}{%
+              current,
+              do until={%
+                > O+t_+t=! {content}{}%
+              }{parent}%
+            }%
+          }{},
+        }{},
+        where level>=1{%
+          if grouped={%
+            if in saved nodewalk={current}{proof tree walk}{}{%
+              no edge,
+            },
+          }{},
+        }{},
+      },
     },
   },
   move by/.style={% this implements both the automated moves prooftrees finds necessary and any additional moves requested by the user - more accurately, it implements initial moves, which may get corrected later (e.g. to avoid skipping numbers or creating empty proof lines, which we assume aren't wanted)
@@ -701,8 +775,8 @@
                     parent anchor=parent,
                     proof tree toing by=#1-2+proof_tree_cadw_toing_by,
                     proof tree phantom,
-                    edge path/.option=!last dynamic node.edge path,
-                    edge/.option=!last dynamic node.edge,
+                    edge path/.option=!u.edge path,
+                    edge/.option=!u.edge,
                     before drawing tree={%
                       if={>{RR|}{line numbering}{justifications}}{%
                         proof tree proof line no/.process={Ow1+n}{!n=1.proof tree proof line no}{##1-1},
@@ -746,6 +820,22 @@
     },
     proof tree rhestr rhifau llinellau+/.option=#1.proof tree proof line no,% works according to Sašo's anti-pgfmath version
   },
+  line no override/.style={% 2018-02-19 ateb https://tex.stackexchange.com/a/416037/
+    before drawing tree={
+      for name/.process={Ow}{proof tree proof line no}{line no ##1}{
+        content=\linenumberstyle{#1},
+        typeset node,
+      },
+    },
+  },
+  no line no/.style={% 2018-02-19 gweler uchod
+    before drawing tree={
+      for name/.process={Ow}{proof tree proof line no}{line no ##1}{
+        content=,
+        typeset node,
+      },
+    },
+  },
   proof tree dadfygio/.style={% style for use in debugging moves which displays information about nodes in the tree
     before packing={%
       for tree={%
@@ -760,6 +850,21 @@
       },
     },
   },
+  proof tree alino/.style={% debugging / dangos dimension stuff
+    before drawing tree={%
+      tikz+/.process={%
+        RRRRw4{proof tree inner proof midpoint}{line no width}{line no dist}{just dist}
+        {
+          \begin{scope}[densely dashed]
+            \draw [darkgray] (##1,0) coordinate (a) -- (a |- current bounding box.south);
+            \draw [green] (current bounding box.west) -- ++(##2,0) coordinate (b);
+            \draw [blue] (b) -- ++(##3,0) coordinate (c);
+            \draw [magenta] (c) -- ++(##4,0);
+          \end{scope}
+        }%
+      },
+    },
+  },
 }
 \environbodyname\prooftreebody
 \bracketset{action character=@}