--- 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;
-
--- 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;
-
--- 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;
--- 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;
--- 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;
--- 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 *)
--- 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;
--- 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;
--- 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};
--- 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 **)
--- 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
--- 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) =
--- 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
--- 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;
--- 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 **)
--- 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 *)
--- 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;
--- 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)
--- 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;
--- 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;