prooftrees (30sep19)

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

1 files changed, 190 insertions, 85 deletions

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=@}