--- 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 ())