# HG changeset patch
# User lcp
# Date 753364701 -3600
# Node ID 96d2c0fc2cd5cfb353182069f011d433c04d095a
# Parent  6b26ccac50fc5c4c0f43686585879d413073aa38
Added commentary

diff -r 6b26ccac50fc -r 96d2c0fc2cd5 src/Pure/Syntax/pretty.ML
--- a/src/Pure/Syntax/pretty.ML	Mon Nov 15 10:30:37 1993 +0100
+++ b/src/Pure/Syntax/pretty.ML	Mon Nov 15 12:58:21 1993 +0100
@@ -67,7 +67,7 @@
 val emptytext = {tx="", nl=0, pos=0};
 
 fun blanks wd {tx,nl,pos} =
-    {tx  = tx ^ repstring" "wd,
+    {tx  = tx ^ repstring " " wd,
      nl  = nl,
      pos = pos+wd};
 
@@ -92,27 +92,31 @@
      breakgain  := !margin div 20;
      emergencypos := !margin div 2);
 
+(*Search for the next break (at this or higher levels) and force it to occur*)
 fun forcenext [] = []
   | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   | forcenext (e :: es) = e :: forcenext es;
 
+(*es is list of expressions to print;
+  blockin is the indentation of the current block;
+  after is the width of the following context until next break. *)
 fun format ([], _, _) text = text
   | format (e::es, blockin, after) (text as {pos,nl,...}) =
     (case e of
        Block(bes,indent,wd) =>
          let val blockin' = (pos + indent) mod !emergencypos
              val btext = format(bes, blockin', breakdist(es,after)) text
-             val es2 = if nl < #nl(btext) then forcenext es
-                       else es
+             (*If this block was broken then force the next break.*)
+	     val es2 = if nl < #nl(btext) then forcenext es else es
          in  format (es2,blockin,after) btext  end
      | String s => format (es,blockin,after) (string s text)
-     | Break(force,wd) => (* no break if text fits on this line
-                      or if breaking would add only breakgain to space *)
+     | Break(force,wd) => (*no break if text to next break fits on this line
+			    or if breaking would add only breakgain to space *)
            format (es,blockin,after)
                (if not force andalso
                    pos+wd <= max[!margin - breakdist(es,after),
                                  blockin + !breakgain]
-                then blanks wd text
+                then blanks wd text  (*just insert wd blanks*)
                 else blanks blockin (newline text)));
 
 (*** Exported functions to create formatting expressions ***)
@@ -131,6 +135,7 @@
         | sum(e::es, k) = sum(es, length e + k)
   in  Block(es,indent, sum(es,0))  end;
 
+(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
 fun lst(lp,rp) es =
   let fun add(e,es) = str"," :: brk 1 :: e :: es;
       fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
@@ -138,6 +143,7 @@
         | list([]) = []
   in blk(size lp, list es) end;
 
+(*Put quotation marks around the given expression*)
 fun quote prt = blk (1, [str "\"", prt, str "\""]);
 
 
@@ -147,7 +153,7 @@
 
 fun setdepth dp = (depth := dp);
 
-
+(*Recursively prune blocks, discarding all text exceeding depth dp*)
 fun pruning dp (Block(bes,indent,wd)) =
       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
               else String"..."
@@ -156,9 +162,10 @@
 fun prune dp e = if dp>0 then pruning dp e else e;
 
 
-fun string_of e = #tx (format ([prune (!depth) e],0,0) emptytext);
+fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
 
 
+(*Create a single flat string: no line breaking*)
 fun str_of prt =
   let
     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
@@ -169,7 +176,7 @@
     s_of (prune (! depth) prt)
   end;
 
-
+(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   let
     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())