# HG changeset patch # User wenzelm # Date 980103209 -3600 # Node ID b520e4f1313bc920cb359c66ce212e3d63b63593 # Parent ddb9b820d8a5d796f04c8273281810576d87e844 support general indentation (e.g. for non-tt latex output); tuned; diff -r ddb9b820d8a5 -r b520e4f1313b src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Sun Jan 21 19:52:32 2001 +0100 +++ b/src/Pure/General/pretty.ML Sun Jan 21 19:53:29 2001 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/General/pretty.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Markus Wenzel, TU Munich + Author: Markus Wenzel, TU Munich License: GPL (GNU GENERAL PUBLIC LICENSE) Generic pretty printing module. @@ -56,51 +56,53 @@ structure Pretty : PRETTY = struct -(*printing items: compound phrases, strings, and breaks*) + +(** printing items: compound phrases, strings, and breaks **) + datatype T = Block of T list * int * int | (*body, indentation, length*) String of string * int | (*text, length*) Break of bool * int; (*mandatory flag, width if not taken*); -(*Add the lengths of the expressions until the next Break; if no Break then - include "after", to account for text following this block. *) -fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after) - | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) - | breakdist (Break _ :: es, after) = 0 - | breakdist ([], after) = after; - -fun repstring a 0 = "" - | repstring a 1 = a - | repstring a k = - if k mod 2 = 0 then repstring(a^a) (k div 2) - else repstring(a^a) (k div 2) ^ a; - -val spaces = repstring " "; -(*** Type for lines of text: string, # of lines, position on line ***) +(** output text **) + +val output_spaces = Symbol.output o Symbol.spaces; +val add_indent = Buffer.add o output_spaces; +fun set_indent wd = Buffer.empty |> add_indent wd; -type text = {tx: Buffer.T, nl: int, pos: int}; - -val emptytext = {tx = Buffer.empty, nl = 0, pos = 0}; +val empty = + {tx = Buffer.empty, + ind = Buffer.empty, + pos = 0, + nl = 0}; -fun blanks wd {tx, nl, pos} = - {tx = Buffer.add (Symbol.output (spaces wd)) tx, - nl = nl, - pos = pos+wd}; +fun newline {tx, ind, pos, nl} = + {tx = Buffer.add (Symbol.output "\n") tx, + ind = Buffer.empty, + pos = 0, + nl = nl + 1}; -fun newline {tx, nl, pos} = - {tx = Buffer.add (Symbol.output "\n") tx, - nl = nl + 1, - pos = 0}; +fun string (s, len) {tx, ind, pos: int, nl} = + {tx = Buffer.add s tx, + ind = Buffer.add s ind, + pos = pos + len, + nl = nl}; + +fun blanks wd = string (output_spaces wd, wd); -fun string s len {tx, nl, pos:int} = - {tx = Buffer.add s tx, - nl = nl, - pos = pos + len}; +fun indentation (buf, len) {tx, ind, pos, nl} = + let val s = Buffer.content buf in + {tx = Buffer.add (Symbol.indent (s, len)) tx, + ind = Buffer.add s ind, + pos = pos + len, + nl = nl} + end; -(*** Formatting ***) + +(** formatting **) (* margin *) @@ -113,32 +115,50 @@ fun setmargin m = margin_info := make_margin_info m; fun setmp_margin m f = setmp margin_info (make_margin_info m) f; -(*Search for the next break (at this or higher levels) and force it to occur*) + +(* format *) + +(*Add the lengths of the expressions until the next Break; if no Break then + include "after", to account for text following this block.*) +fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after) + | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) + | breakdist (Break _ :: es, after) = 0 + | breakdist ([], after) = after; + +(*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 (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. *) + 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 (! margin_info) - val btext = format(bes, blockin', breakdist(es,after)) text - (*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, len) => format (es,blockin,after) (string s len text) - | 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 <= Int.max(#margin (! margin_info) - breakdist(es,after), - blockin + #breakgain (! margin_info)) - then blanks wd text (*just insert wd blanks*) - else blanks blockin (newline text))); + | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) = + (case e of + Block (bes, indent, wd) => + let + val {emergencypos, ...} = ! margin_info; + val pos' = pos + indent; + val pos'' = pos' mod emergencypos; + val block' = + if pos' < emergencypos then (ind |> add_indent indent, pos') + else (set_indent pos'', pos''); + val btext = format (bes, block', breakdist (es, after)) text; + (*if this block was broken then force the next break*) + val es2 = if nl < #nl btext then forcenext es else es; + in format (es2, block, after) btext end + | String str => format (es, block, after) (string str text) + | Break (force, wd) => + let val {margin, breakgain, ...} = ! margin_info in + (*no break if text to next break fits on this line + or if breaking would add only breakgain to space*) + format (es, block, after) + (if not force andalso + pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain) + then text |> blanks wd (*just insert wd blanks*) + else text |> newline |> indentation block) + end); (*** Exported functions to create formatting expressions ***) @@ -184,7 +204,7 @@ fun chunks prts = blk (0, fbreaks prts); fun indent 0 prt = prt - | indent n prt = blk (0, [str (spaces n), prt]); + | indent n prt = blk (0, [str (Symbol.spaces n), prt]); (*** Pretty printing with depth limitation ***) @@ -199,11 +219,9 @@ else str "..." | pruning dp e = e; -fun prune dp e = if dp>0 then pruning dp e else e; - +fun prune dp e = if dp > 0 then pruning dp e else e; -fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], 0, 0) emptytext)); - +fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty)); val writeln = writeln o string_of; @@ -212,8 +230,8 @@ let fun s_of (Block (prts, _, _)) = implode (map s_of prts) | s_of (String (s, _)) = s - | s_of (Break (false, wd)) = Symbol.output (spaces wd) - | s_of (Break (true, _)) = Symbol.output " "; + | s_of (Break (false, wd)) = output_spaces wd + | s_of (Break (true, _)) = output_spaces 1; in s_of (prune (! depth) prt) end; (*part of the interface to the ML toplevel pretty printers*)