--- a/src/Pure/ML/install_pp_polyml.ML Fri Mar 18 16:38:04 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-(* Title: Pure/ML/install_pp_polyml.ML
- Author: Makarius
-
-ML toplevel pretty-printing for Poly/ML.
-*)
-
-PolyML.addPrettyPrinter
- (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
-
-PolyML.addPrettyPrinter
- (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
-
-PolyML.addPrettyPrinter
- (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
-
-PolyML.addPrettyPrinter
- (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
-
-PolyML.addPrettyPrinter
- (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
-
-
-local
-
-open PolyML;
-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 ^ " (") ")";
-
-fun prt_term parens (dp: FixedInt.int) t =
- if dp <= 0 then Pretty.str "..."
- else
- (case t of
- _ $ _ =>
- op :: (strip_comb t)
- |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
- |> Pretty.separate " $"
- |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
- | Abs (a, T, b) =>
- prt_apps "Abs"
- [from_ML (prettyRepresentation (a, dp - 1)),
- from_ML (prettyRepresentation (T, dp - 2)),
- prt_term false (dp - 3) b]
- | Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1)))
- | Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1)))
- | Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1)))
- | Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1))));
-
-in
-
-val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
- ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
-
-local
-
-fun prt_proof parens dp prf =
- if dp <= 0 then Pretty.str "..."
- else
- (case prf of
- _ % _ => prt_proofs parens dp prf
- | _ %% _ => prt_proofs parens dp prf
- | Abst (a, T, b) =>
- prt_apps "Abst"
- [from_ML (prettyRepresentation (a, dp - 1)),
- from_ML (prettyRepresentation (T, dp - 2)),
- prt_proof false (dp - 3) b]
- | AbsP (a, t, b) =>
- prt_apps "AbsP"
- [from_ML (prettyRepresentation (a, dp - 1)),
- from_ML (prettyRepresentation (t, dp - 2)),
- prt_proof false (dp - 3) b]
- | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
- | MinProof => Pretty.str "MinProof"
- | PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1)))
- | PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1)))
- | OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1)))
- | Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1)))
- | Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1)))
- | PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1))))
-
-and prt_proofs parens dp prf =
- let
- val (head, args) = strip_proof prf [];
- val prts =
- head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
- in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
-
-and strip_proof (p % t) res =
- strip_proof p
- ((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res)
- | strip_proof (p %% q) res =
- strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
- | strip_proof p res = (fn d => prt_proof true d p, res);
-
-in
-
-val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
- ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
-
-end;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pp.ML Fri Mar 18 16:38:40 2016 +0100
@@ -0,0 +1,113 @@
+(* Title: Pure/ML/ml_pp.ML
+ Author: Makarius
+
+ML toplevel pretty-printing for logical entities.
+*)
+
+structure ML_PP: sig end =
+struct
+
+val _ =
+ PolyML.addPrettyPrinter
+ (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
+
+val _ =
+ PolyML.addPrettyPrinter
+ (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
+
+val _ =
+ PolyML.addPrettyPrinter
+ (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
+
+val _ =
+ PolyML.addPrettyPrinter
+ (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
+
+val _ =
+ PolyML.addPrettyPrinter
+ (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
+
+
+local
+
+fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
+fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
+
+fun prt_term parens (dp: FixedInt.int) t =
+ if dp <= 0 then Pretty.str "..."
+ else
+ (case t of
+ _ $ _ =>
+ op :: (strip_comb t)
+ |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
+ |> Pretty.separate " $"
+ |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
+ | Abs (a, T, b) =>
+ prt_apps "Abs"
+ [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
+ Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
+ prt_term false (dp - 3) b]
+ | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
+
+in
+
+val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
+
+
+local
+
+fun prt_proof parens dp prf =
+ if dp <= 0 then Pretty.str "..."
+ else
+ (case prf of
+ _ % _ => prt_proofs parens dp prf
+ | _ %% _ => prt_proofs parens dp prf
+ | Abst (a, T, b) =>
+ prt_apps "Abst"
+ [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
+ Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
+ prt_proof false (dp - 3) b]
+ | AbsP (a, t, b) =>
+ prt_apps "AbsP"
+ [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
+ Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)),
+ prt_proof false (dp - 3) b]
+ | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
+ | MinProof => Pretty.str "MinProof"
+ | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
+ | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
+
+and prt_proofs parens dp prf =
+ let
+ val (head, args) = strip_proof prf [];
+ val prts =
+ head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
+ in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
+
+and strip_proof (p % t) res =
+ strip_proof p
+ ((fn d =>
+ [Pretty.str " %", Pretty.brk 1,
+ Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res)
+ | strip_proof (p %% q) res =
+ strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
+ | strip_proof p res = (fn d => prt_proof true d p, res);
+
+in
+
+val _ =
+ PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
+ ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
+
+end;
+
+end;
+
+end;
--- a/src/Pure/ROOT Fri Mar 18 16:38:04 2016 +0100
+++ b/src/Pure/ROOT Fri Mar 18 16:38:40 2016 +0100
@@ -101,7 +101,6 @@
"ML/exn_debugger.ML"
"ML/exn_properties.ML"
"ML/fixed_int_dummy.ML"
- "ML/install_pp_polyml.ML"
"ML/ml_antiquotation.ML"
"ML/ml_compiler.ML"
"ML/ml_compiler0.ML"
@@ -113,6 +112,7 @@
"ML/ml_lex.ML"
"ML/ml_name_space.ML"
"ML/ml_options.ML"
+ "ML/ml_pp.ML"
"ML/ml_pretty.ML"
"ML/ml_profiling.ML"
"ML/ml_statistics.ML"
--- a/src/Pure/ROOT.ML Fri Mar 18 16:38:04 2016 +0100
+++ b/src/Pure/ROOT.ML Fri Mar 18 16:38:40 2016 +0100
@@ -393,8 +393,7 @@
structure Output: OUTPUT = Output; (*seal system channels!*)
-
-use "ML/install_pp_polyml.ML";
+use "ML/ml_pp.ML";
(* the Pure theory *)