# HG changeset patch # User wenzelm # Date 1458315520 -3600 # Node ID a78ce0c6e191710a0ae27e183b5cd976f307c9b3 # Parent 083c9865c554f9d29b3133cb101dbcf75732822b clarified modules; diff -r 083c9865c554 -r a78ce0c6e191 src/Pure/ML/install_pp_polyml.ML --- 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; diff -r 083c9865c554 -r a78ce0c6e191 src/Pure/ML/ml_pp.ML --- /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; diff -r 083c9865c554 -r a78ce0c6e191 src/Pure/ROOT --- 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" diff -r 083c9865c554 -r a78ce0c6e191 src/Pure/ROOT.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 *)