# HG changeset patch
# User wenzelm
# Date 1458314795 -3600
# Node ID bea354f6ff212498e397b085cfb6b1936f30b7fb
# Parent  291cc01f56f5464930528221e687aadc891afba7
clarified modules;
tuned signature;

diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -99,6 +99,13 @@
 fun peek x = Single_Assignment.peek (result_of x);
 fun is_finished x = is_some (peek x);
 
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+    (case peek x of
+      NONE => PolyML.PrettyString "<future>"
+    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+    | SOME (Exn.Res y) => pretty (y, depth)));
+
 
 
 (** scheduling **)
@@ -665,4 +672,3 @@
 end;
 
 type 'a future = 'a Future.future;
-
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -99,7 +99,16 @@
   if is_finished x then Future.value_result (force_result x)
   else (singleton o Future.forks) params (fn () => force x);
 
+
+(* toplevel pretty printing *)
+
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+    (case peek x of
+      NONE => PolyML.PrettyString "<lazy>"
+    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+    | SOME (Exn.Res y) => pretty (y, depth)));
+
 end;
 
 type 'a lazy = 'a Lazy.lazy;
-
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -66,4 +66,9 @@
 
 end;
 
+
+(* toplevel pretty printing *)
+
+val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth));
+
 end;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -394,4 +394,10 @@
         | NONE => ((NONE, deps'), queue)))
   end;
 
+
+(* toplevel pretty printing *)
+
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+
 end;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/General/binding.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -35,7 +35,6 @@
   val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
-  val pp: binding -> Pretty.T
   val bad: binding -> string
   val check: binding -> unit
   val name_spec: scope list -> (string * bool) list -> binding ->
@@ -155,7 +154,7 @@
 
 val print = Pretty.unformatted_string_of o pretty;
 
-val pp = pretty o set_pos Position.none;
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
 
 
 (* check *)
@@ -191,6 +190,7 @@
       andalso error (bad binding);
   in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
+
 end;
 
 type binding = Binding.binding;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/General/path.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -173,6 +173,8 @@
 
 val print = Pretty.unformatted_string_of o pretty;
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+
 
 (* base element *)
 
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/General/pretty.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -74,6 +74,8 @@
   val writeln_chunks2: T list -> unit
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
+  val to_polyml: T -> PolyML.pretty
+  val from_polyml: PolyML.pretty -> T
 end;
 
 structure Pretty: PRETTY =
@@ -372,7 +374,7 @@
 
 
 
-(** ML toplevel pretty printing **)
+(** toplevel pretty printing **)
 
 fun to_ML (Block (m, consistent, indent, prts, _)) =
       ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map to_ML prts)
@@ -386,6 +388,12 @@
       Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
   | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
 
+val to_polyml = to_ML #> ML_Pretty.to_polyml;
+val from_polyml = ML_Pretty.from_polyml #> from_ML;
+
 end;
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn _: T => to_polyml (str "<pretty>"));
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
+
 end;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/General/sha1.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -139,4 +139,6 @@
 
 val fake = Digest;
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
+
 end;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -173,6 +173,10 @@
       (context * thm list list -> state -> state) *
       (context * thm list list -> context -> context)};
 
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
+    Pretty.to_polyml (Pretty.str "<Proof.state>"));
+
 fun make_goal (statement, using, goal, before_qed, after_qed) =
   Goal {statement = statement, using = using, goal = goal,
     before_qed = before_qed, after_qed = after_qed};
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -199,6 +199,8 @@
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
+
 
 
 (** toplevel transitions **)
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -4,80 +4,20 @@
 ML toplevel pretty-printing for Poly/ML.
 *)
 
-PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
 
-PolyML.addPrettyPrinter (fn _ => fn _ => fn 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.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn 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.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
 
-PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
-
-PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
-  ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
 
-PolyML.addPrettyPrinter (fn depth => fn _ => fn 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.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
-  pretty (Synchronized.value var, depth));
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
 
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
-  (case Future.peek x of
-    NONE => PolyML.PrettyString "<future>"
-  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
-  | SOME (Exn.Res y) => pretty (y, depth)));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
-  (case Lazy.peek x of
-    NONE => PolyML.PrettyString "<lazy>"
-  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
-  | SOME (Exn.Res y) => pretty (y, depth)));
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
 
 
 local
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -65,7 +65,7 @@
           let
             val xml =
               ML_Name_Space.displayTypeExpression (types, depth, space)
-              |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
+              |> Pretty.from_polyml |> 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_location loc;
         val txt =
           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
+          Pretty.string_of (Pretty.from_polyml msg);
       in if hard then err txt else warn txt end;
 
 
@@ -205,8 +205,7 @@
       let
         fun display disp x =
           if depth > 0 then
-            (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
-              write "\n")
+            (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
           else ();
 
         fun apply_fix (a, b) =
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -114,8 +114,7 @@
 (* make string *)
 
 local
-  fun pretty_string_of s =
-    "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))";
+  fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
   fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
 in
 
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -123,4 +123,8 @@
       else take (Int.max (max_len, 0)) body @ ["..."];
   in Pretty.str (quote (implode (map print_char body'))) end;
 
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+    Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
+
 end;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/PIDE/xml.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -170,6 +170,9 @@
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
+val _ =
+  PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+
 
 
 (** XML parsing **)
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Syntax/ast.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -66,6 +66,8 @@
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
+
 
 (* strip_positions *)
 
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -66,7 +66,6 @@
   val is_marked: string -> bool
   val dummy_type: term
   val fun_type: term
-  val pp_lexicon: Scan.lexicon -> Pretty.T
 end;
 
 structure Lexicon: LEXICON =
@@ -455,7 +454,8 @@
 
 (* toplevel pretty printing *)
 
-val pp_lexicon =
-  Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ =>
+    Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Tools/debugger.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -189,9 +189,8 @@
     val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
 
     fun print x =
-      Pretty.from_ML
-        (ML_Pretty.from_polyml
-          (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space)));
+      Pretty.from_polyml
+        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
     fun print_all () =
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/context.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -169,6 +169,8 @@
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
+
 fun pretty_abbrev_thy thy =
   let
     val names = display_names thy;
diff -r 291cc01f56f5 -r bea354f6ff21 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/morphism.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -71,6 +71,8 @@
 
 fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
 
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+
 fun binding (Morphism {binding, ...}) = apply binding;
 fun typ (Morphism {typ, ...}) = apply typ;
 fun term (Morphism {term, ...}) = apply term;