added strlen (includes metric information);
removed map_strs;

--- a/src/Pure/Syntax/pretty.ML	Fri Feb 28 16:40:08 1997 +0100
+++ b/src/Pure/Syntax/pretty.ML	Fri Feb 28 16:41:04 1997 +0100
@@ -26,10 +26,11 @@
 signature PRETTY =
   sig
   type T
-  val blk: int * T list -> T
+  val str: string -> T
+  val strlen: string -> int -> T
   val brk: int -> T
   val fbrk: T
-  val str: string -> T
+  val blk: int * T list -> T
   val lst: string * string -> T list -> T
   val quote: T -> T
   val commas: T list -> T list
@@ -45,7 +46,6 @@
   val writeln: T -> unit
   val str_of: T -> string
   val pprint: T -> pprint_args -> unit
-  val map_strs: (string -> string) -> T -> T
   val setdepth: int -> unit
   val setmargin: int -> unit
   end;
@@ -53,15 +53,16 @@
 structure Pretty : PRETTY =
 struct
 
-(*Printing items: compound phrases, strings, and breaks*)
-datatype T = Block of T list * int * int (*indentation, length*)
-           | String of string
-           | Break of bool*int   (*mandatory flag; width if not taken*);
+(*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 :: es, after) = size s + breakdist (es, after)
+  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
   | breakdist (Break _ :: es, after) = 0
   | breakdist ([], after) = after;
 
@@ -87,10 +88,11 @@
      nl  = nl+1,
      pos = 0};
 
-fun string s {tx,nl,pos} =
+fun string s len {tx,nl,pos:int} =
     {tx  = tx ^ s,
      nl  = nl,
-     pos = pos + size(s)};
+     pos = pos + len};
+
 
 (*** Formatting ***)
 
@@ -120,31 +122,34 @@
              (*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)
+     | 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 - breakdist(es,after),
-				     blockin + !breakgain)
+                                     blockin + !breakgain)
                 then blanks wd text  (*just insert wd blanks*)
                 else blanks blockin (newline text)));
 
+
 (*** Exported functions to create formatting expressions ***)
 
-fun length (Block(_,_,len)) = len
-  | length (String s) = size s
-  | length (Break(_,wd)) = wd;
+fun length (Block (_, _, len)) = len
+  | length (String (_, len)) = len
+  | length (Break(_, wd)) = wd;
 
-val str = String
-and fbrk = Break(true,0);
+fun str s = String (s, size s);
+fun strlen s len = String (s, len);
 
-fun brk wd = Break(false,wd);
+fun brk wd = Break (false, wd);
+val fbrk = Break (true, 0);
 
-fun blk (indent,es) =
-  let fun sum([], k) = k
-        | sum(e::es, k) = sum(es, length e + k)
-  in  Block(es,indent, sum(es,0))  end;
+fun blk (indent, es) =
+  let
+    fun sum([], k) = k
+      | 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 =
@@ -194,7 +199,7 @@
 (*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"..."
+              else str "..."
   | pruning dp e = e;
 
 fun prune dp e = if dp>0 then pruning dp e else e;
@@ -209,7 +214,7 @@
 fun str_of prt =
   let
     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
-      | s_of (String s) = s
+      | s_of (String (s, _)) = s
       | s_of (Break (false, wd)) = repstring " " wd
       | s_of (Break (true, _)) = " ";
   in
@@ -220,7 +225,7 @@
 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 ())
-      | pp (String s) = put_str s
+      | pp (String (s, _)) = put_str s
       | pp (Break (false, wd)) = put_brk wd
       | pp (Break (true, _)) = put_fbrk ()
     and pp_lst [] = ()
@@ -229,15 +234,9 @@
     pp (prune (! depth) prt)
   end;
 
-(*Map strings*)
-fun map_strs f (Block (prts, ind, _)) = blk (ind, map (map_strs f) prts)
-  | map_strs f (String s) = String (f s)
-  | map_strs _ brk = brk;
-
 
 (*** Initialization ***)
 
 val () = setmargin 80;
 
 end;
-