src/Tools/Metis/src/Print.sig

--- a/src/Tools/Metis/src/Print.sig	Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Print.sig	Wed Dec 07 16:03:05 2011 +0100
@@ -13,41 +13,12 @@
 val escapeString : {escape : char list} -> string -> string
 
 (* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size.                              *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int
-
-val mkStringSize : string -> stringSize
-
-(* ------------------------------------------------------------------------- *)
 (* A type of pretty-printers.                                                *)
 (* ------------------------------------------------------------------------- *)
 
-datatype breakStyle = Consistent | Inconsistent
-
-datatype step =
-    BeginBlock of breakStyle * int
-  | EndBlock
-  | AddString of stringSize
-  | AddBreak of int
-  | AddNewline
-
-type ppstream = step Stream.stream
+type ppstream
 
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives.                                                *)
-(* ------------------------------------------------------------------------- *)
-
-val beginBlock : breakStyle -> int -> ppstream
-
-val endBlock : ppstream
-
-val addString : stringSize -> ppstream
-
-val addBreak : int -> ppstream
-
-val addNewline : ppstream
+type 'a pp = 'a -> ppstream
 
 val skip : ppstream
 
@@ -59,28 +30,75 @@
 
 val stream : ppstream Stream.stream -> ppstream
 
-val block : breakStyle -> int -> ppstream -> ppstream
+val ppPpstream : ppstream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks.                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent
 
-val blockProgram : breakStyle -> int -> ppstream list -> ppstream
+datatype block =
+    Block of
+      {style : style,
+       indent : int}
+
+val styleBlock : block -> style
+
+val indentBlock : block -> int
+
+val block : block -> ppstream -> ppstream
+
+val consistentBlock : int -> ppstream list -> ppstream
+
+val inconsistentBlock : int -> ppstream list -> ppstream
 
 (* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines.                              *)
+(* Words are unbreakable strings annotated with their effective size.        *)
 (* ------------------------------------------------------------------------- *)
 
-val execute :
-    {lineLength : int} -> ppstream ->
-    {indent : int, line : string} Stream.stream
+datatype word = Word of {word : string, size : int}
+
+val mkWord : string -> word
+
+val emptyWord : word
+
+val charWord : char -> word
+
+val ppWord : word pp
+
+val space : ppstream
+
+val spaces : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks.                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int}
+
+val mkBreak : int -> break
+
+val ppBreak : break pp
+
+val break : ppstream
+
+val breaks : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+val newline : ppstream
+
+val newlines : int -> ppstream
 
 (* ------------------------------------------------------------------------- *)
 (* Pretty-printer combinators.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-type 'a pp = 'a -> ppstream
-
 val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
 
-val ppString : string pp
-
 val ppBracket : string -> string -> 'a pp -> 'a pp
 
 val ppOp : string -> ppstream
@@ -99,6 +117,8 @@
 
 val ppChar : char pp
 
+val ppString : string pp
+
 val ppEscapeString : {escape : char list} -> string pp
 
 val ppUnit : unit pp
@@ -125,12 +145,6 @@
 
 val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
 
-val ppBreakStyle : breakStyle pp
-
-val ppStep : step pp
-
-val ppPpstream : ppstream pp
-
 val ppException : exn pp
 
 (* ------------------------------------------------------------------------- *)
@@ -160,15 +174,29 @@
     ('a * bool) pp -> ('a * bool) pp
 
 (* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length.                      *)
+(* Pretty-printer rendering.                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val render :
+    {lineLength : int option} -> ppstream ->
+    {indent : int, line : string} Stream.stream
+
+val toStringWithLineLength :
+    {lineLength : int option} -> 'a pp -> 'a -> string
+
+val toStreamWithLineLength :
+    {lineLength : int option} -> 'a pp -> 'a -> string Stream.stream
+
+val toLine : 'a pp -> 'a -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length.                       *)
 (* ------------------------------------------------------------------------- *)
 
 val lineLength : int ref
 
 val toString : 'a pp -> 'a -> string
 
-val toLine : 'a pp -> 'a -> string
-
 val toStream : 'a pp -> 'a -> string Stream.stream
 
 val trace : 'a pp -> string -> 'a -> unit