# HG changeset patch
# User wenzelm
# Date 1457002743 -3600
# Node ID 19afb533028e7185c4915f4ca62a059e87c9d173
# Parent  8857237c3a90cabcfa32c033dc5753ac4138ad13
clarified modules;

diff -r 8857237c3a90 -r 19afb533028e src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/General/linear_set.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -137,9 +137,11 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
-    ml_pretty
+    ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (ML_Pretty.pair
+          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+          (ML_Pretty.from_polyml o pretty))
         (dest set, depth)));
 
 end;
diff -r 8857237c3a90 -r 19afb533028e src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/General/table.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -412,9 +412,11 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
-    ml_pretty
+    ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+        (ML_Pretty.pair
+          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+          (ML_Pretty.from_polyml o pretty))
         (dest tab, depth)));
 
 
diff -r 8857237c3a90 -r 19afb533028e src/Pure/ML/exn_output.ML
--- a/src/Pure/ML/exn_output.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/exn_output.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -20,7 +20,7 @@
 
 fun pretty (exn: exn) =
   Pretty.from_ML
-    (pretty_ml
+    (ML_Pretty.from_polyml
       (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
 
 end;
diff -r 8857237c3a90 -r 19afb533028e src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -5,64 +5,64 @@
 *)
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
-  ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
-  ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
-  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
-  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
-  ml_pretty (Pretty.to_ML (Pretty.position pos)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
-  ml_pretty (Pretty.to_ML (Binding.pp binding)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
-  ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
-  ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
-  ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
-  ml_pretty (Pretty.to_ML (Path.pretty path)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
-  ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
-  ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
+  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
-  ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
 
 PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
-  ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
+  ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
-  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
+  ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
-  ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
+  ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
 
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   pretty (Synchronized.value var, depth));
@@ -83,7 +83,7 @@
 local
 
 open PolyML;
-val from_ML = Pretty.from_ML o pretty_ml;
+val from_ML = Pretty.from_ML o ML_Pretty.from_polyml;
 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
 
@@ -110,7 +110,7 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
-    ml_pretty (Pretty.to_ML (prt_term false depth t)));
+    ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
 
 local
 
@@ -157,7 +157,7 @@
 
 val _ =
   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
-    ml_pretty (Pretty.to_ML (prt_proof false depth prf)));
+    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
 
 end;
 
diff -r 8857237c3a90 -r 19afb533028e src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -65,7 +65,7 @@
           let
             val xml =
               ML_Name_Space.displayTypeExpression (types, depth, space)
-              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+              |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
               |> Output.output |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;
@@ -193,7 +193,7 @@
         val pos = Exn_Properties.position_of loc;
         val txt =
           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
+          Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
       in if hard then err txt else warn txt end;
 
 
@@ -205,7 +205,8 @@
       let
         fun display disp x =
           if depth > 0 then
-            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+            (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
+              write "\n")
           else ();
 
         fun apply_fix (a, b) =
diff -r 8857237c3a90 -r 19afb533028e src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -92,43 +92,6 @@
 
 val error_depth = PolyML.error_depth;
 
-val pretty_ml =
-  let
-    fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
-      | convert _ (PolyML.PrettyBlock (_, _,
-            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
-          ML_Pretty.Break (true, 1, 0)
-      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
-          let
-            fun property name default =
-              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (PolyML.ContextProperty (_, b)) => b
-              | _ => default);
-            val bg = property "begin" "";
-            val en = property "end" "";
-            val len' = property "length" len;
-          in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
-      | convert len (PolyML.PrettyString s) =
-          ML_Pretty.String
-            (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
-  in convert "" end;
-
-fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
-  | ml_pretty (ML_Pretty.Break (true, _, _)) =
-      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
-        [PolyML.PrettyString " "])
-  | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
-      let val context =
-        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
-        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
-      in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
-  | ml_pretty (ML_Pretty.String (s, len)) =
-      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
-      else
-        PolyML.PrettyBlock
-          (0, false,
-            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
-
 
 (* ML compiler *)
 
@@ -137,7 +100,7 @@
 structure ML_Name_Space =
 struct
   open ML_Name_Space;
-  val display_val = pretty_ml o displayVal;
+  val display_val = ML_Pretty.from_polyml o displayVal;
 end;
 
 use "RAW/ml_positions.ML";
@@ -150,7 +113,7 @@
 PolyML.Compiler.prompt2 := "ML# ";
 
 fun ml_make_string struct_name =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
+  "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
     struct_name ^ ".ML_print_depth ()))))))";
 
 
diff -r 8857237c3a90 -r 19afb533028e src/Pure/RAW/ml_debugger.ML
--- a/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -44,7 +44,7 @@
 val _ =
   PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
     let val s = print_exn_id exn_id
-    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
+    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
 
 
 (* hooks *)
diff -r 8857237c3a90 -r 19afb533028e src/Pure/RAW/ml_pretty.ML
--- a/src/Pure/RAW/ml_pretty.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/RAW/ml_pretty.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -1,10 +1,25 @@
 (*  Title:      Pure/RAW/ml_pretty.ML
     Author:     Makarius
 
-Minimal support for raw ML pretty printing -- for boot-strapping only.
+Minimal support for raw ML pretty printing, notably for toplevel pp.
 *)
 
-structure ML_Pretty =
+signature ML_PRETTY =
+sig
+  datatype pretty =
+    Block of (string * string) * bool * FixedInt.int * pretty list |
+    String of string * FixedInt.int |
+    Break of bool * FixedInt.int * FixedInt.int
+  val block: pretty list -> pretty
+  val str: string -> pretty
+  val brk: FixedInt.int -> pretty
+  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
+  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
+  val to_polyml: pretty -> PolyML.pretty
+  val from_polyml: PolyML.pretty -> pretty
+end;
+
+structure ML_Pretty: ML_PRETTY =
 struct
 
 datatype pretty =
@@ -27,4 +42,43 @@
       | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
   in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
 
+
+(* convert *)
+
+fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
+  | to_polyml (Break (true, _, _)) =
+      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+        [PolyML.PrettyString " "])
+  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
+      let val context =
+        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
+  | to_polyml (String (s, len)) =
+      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
+      else
+        PolyML.PrettyBlock
+          (0, false,
+            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
+
+val from_polyml =
+  let
+    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
+      | convert _ (PolyML.PrettyBlock (_, _,
+            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
+          Break (true, 1, 0)
+      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
+          let
+            fun property name default =
+              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (PolyML.ContextProperty (_, b)) => b
+              | _ => default);
+            val bg = property "begin" "";
+            val en = property "end" "";
+            val len' = property "length" len;
+          in Block ((bg, en), consistent, ind, map (convert len') prts) end
+      | convert len (PolyML.PrettyString s) =
+          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
+  in convert "" end;
+
 end;