clarified modules;
authorwenzelm
Fri Mar 18 16:38:40 2016 +0100 (2016-03-18)
changeset 62665a78ce0c6e191
parent 62664 083c9865c554
child 62666 00aff1da05ae
clarified modules;
src/Pure/ML/install_pp_polyml.ML
src/Pure/ML/ml_pp.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/install_pp_polyml.ML	Fri Mar 18 16:38:04 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,104 +0,0 @@
     1.4 -(*  Title:      Pure/ML/install_pp_polyml.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -ML toplevel pretty-printing for Poly/ML.
     1.8 -*)
     1.9 -
    1.10 -PolyML.addPrettyPrinter
    1.11 -  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    1.12 -
    1.13 -PolyML.addPrettyPrinter
    1.14 -  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
    1.15 -
    1.16 -PolyML.addPrettyPrinter
    1.17 -  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
    1.18 -
    1.19 -PolyML.addPrettyPrinter
    1.20 -  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    1.21 -
    1.22 -PolyML.addPrettyPrinter
    1.23 -  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
    1.24 -
    1.25 -
    1.26 -local
    1.27 -
    1.28 -open PolyML;
    1.29 -val from_ML = Pretty.from_ML o ML_Pretty.from_polyml;
    1.30 -fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
    1.31 -fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
    1.32 -
    1.33 -fun prt_term parens (dp: FixedInt.int) t =
    1.34 -  if dp <= 0 then Pretty.str "..."
    1.35 -  else
    1.36 -    (case t of
    1.37 -      _ $ _ =>
    1.38 -        op :: (strip_comb t)
    1.39 -        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
    1.40 -        |> Pretty.separate " $"
    1.41 -        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
    1.42 -    | Abs (a, T, b) =>
    1.43 -        prt_apps "Abs"
    1.44 -         [from_ML (prettyRepresentation (a, dp - 1)),
    1.45 -          from_ML (prettyRepresentation (T, dp - 2)),
    1.46 -          prt_term false (dp - 3) b]
    1.47 -    | Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1)))
    1.48 -    | Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1)))
    1.49 -    | Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1)))
    1.50 -    | Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1))));
    1.51 -
    1.52 -in
    1.53 -
    1.54 -val _ =
    1.55 -  PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
    1.56 -    ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
    1.57 -
    1.58 -local
    1.59 -
    1.60 -fun prt_proof parens dp prf =
    1.61 -  if dp <= 0 then Pretty.str "..."
    1.62 -  else
    1.63 -    (case prf of
    1.64 -      _ % _ => prt_proofs parens dp prf
    1.65 -    | _ %% _ => prt_proofs parens dp prf
    1.66 -    | Abst (a, T, b) =>
    1.67 -        prt_apps "Abst"
    1.68 -         [from_ML (prettyRepresentation (a, dp - 1)),
    1.69 -          from_ML (prettyRepresentation (T, dp - 2)),
    1.70 -          prt_proof false (dp - 3) b]
    1.71 -    | AbsP (a, t, b) =>
    1.72 -        prt_apps "AbsP"
    1.73 -         [from_ML (prettyRepresentation (a, dp - 1)),
    1.74 -          from_ML (prettyRepresentation (t, dp - 2)),
    1.75 -          prt_proof false (dp - 3) b]
    1.76 -    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
    1.77 -    | MinProof => Pretty.str "MinProof"
    1.78 -    | PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1)))
    1.79 -    | PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1)))
    1.80 -    | OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1)))
    1.81 -    | Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1)))
    1.82 -    | Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1)))
    1.83 -    | PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1))))
    1.84 -
    1.85 -and prt_proofs parens dp prf =
    1.86 -  let
    1.87 -    val (head, args) = strip_proof prf [];
    1.88 -    val prts =
    1.89 -      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
    1.90 -  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
    1.91 -
    1.92 -and strip_proof (p % t) res =
    1.93 -      strip_proof p
    1.94 -        ((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res)
    1.95 -  | strip_proof (p %% q) res =
    1.96 -      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
    1.97 -  | strip_proof p res = (fn d => prt_proof true d p, res);
    1.98 -
    1.99 -in
   1.100 -
   1.101 -val _ =
   1.102 -  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
   1.103 -    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
   1.104 -
   1.105 -end;
   1.106 -
   1.107 -end;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML/ml_pp.ML	Fri Mar 18 16:38:40 2016 +0100
     2.3 @@ -0,0 +1,113 @@
     2.4 +(*  Title:      Pure/ML/ml_pp.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +ML toplevel pretty-printing for logical entities.
     2.8 +*)
     2.9 +
    2.10 +structure ML_PP: sig end =
    2.11 +struct
    2.12 +
    2.13 +val _ =
    2.14 +  PolyML.addPrettyPrinter
    2.15 +    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    2.16 +
    2.17 +val _ =
    2.18 +  PolyML.addPrettyPrinter
    2.19 +    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
    2.20 +
    2.21 +val _ =
    2.22 +  PolyML.addPrettyPrinter
    2.23 +    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
    2.24 +
    2.25 +val _ =
    2.26 +  PolyML.addPrettyPrinter
    2.27 +    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    2.28 +
    2.29 +val _ =
    2.30 +  PolyML.addPrettyPrinter
    2.31 +    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
    2.32 +
    2.33 +
    2.34 +local
    2.35 +
    2.36 +fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
    2.37 +fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
    2.38 +
    2.39 +fun prt_term parens (dp: FixedInt.int) t =
    2.40 +  if dp <= 0 then Pretty.str "..."
    2.41 +  else
    2.42 +    (case t of
    2.43 +      _ $ _ =>
    2.44 +        op :: (strip_comb t)
    2.45 +        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
    2.46 +        |> Pretty.separate " $"
    2.47 +        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
    2.48 +    | Abs (a, T, b) =>
    2.49 +        prt_apps "Abs"
    2.50 +         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    2.51 +          Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
    2.52 +          prt_term false (dp - 3) b]
    2.53 +    | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.54 +    | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.55 +    | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.56 +    | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
    2.57 +
    2.58 +in
    2.59 +
    2.60 +val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
    2.61 +
    2.62 +
    2.63 +local
    2.64 +
    2.65 +fun prt_proof parens dp prf =
    2.66 +  if dp <= 0 then Pretty.str "..."
    2.67 +  else
    2.68 +    (case prf of
    2.69 +      _ % _ => prt_proofs parens dp prf
    2.70 +    | _ %% _ => prt_proofs parens dp prf
    2.71 +    | Abst (a, T, b) =>
    2.72 +        prt_apps "Abst"
    2.73 +         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    2.74 +          Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
    2.75 +          prt_proof false (dp - 3) b]
    2.76 +    | AbsP (a, t, b) =>
    2.77 +        prt_apps "AbsP"
    2.78 +         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
    2.79 +          Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)),
    2.80 +          prt_proof false (dp - 3) b]
    2.81 +    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
    2.82 +    | MinProof => Pretty.str "MinProof"
    2.83 +    | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.84 +    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.85 +    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.86 +    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.87 +    | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
    2.88 +    | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
    2.89 +
    2.90 +and prt_proofs parens dp prf =
    2.91 +  let
    2.92 +    val (head, args) = strip_proof prf [];
    2.93 +    val prts =
    2.94 +      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
    2.95 +  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
    2.96 +
    2.97 +and strip_proof (p % t) res =
    2.98 +      strip_proof p
    2.99 +        ((fn d =>
   2.100 +          [Pretty.str " %", Pretty.brk 1,
   2.101 +            Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res)
   2.102 +  | strip_proof (p %% q) res =
   2.103 +      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
   2.104 +  | strip_proof p res = (fn d => prt_proof true d p, res);
   2.105 +
   2.106 +in
   2.107 +
   2.108 +val _ =
   2.109 +  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
   2.110 +    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
   2.111 +
   2.112 +end;
   2.113 +
   2.114 +end;
   2.115 +
   2.116 +end;
     3.1 --- a/src/Pure/ROOT	Fri Mar 18 16:38:04 2016 +0100
     3.2 +++ b/src/Pure/ROOT	Fri Mar 18 16:38:40 2016 +0100
     3.3 @@ -101,7 +101,6 @@
     3.4      "ML/exn_debugger.ML"
     3.5      "ML/exn_properties.ML"
     3.6      "ML/fixed_int_dummy.ML"
     3.7 -    "ML/install_pp_polyml.ML"
     3.8      "ML/ml_antiquotation.ML"
     3.9      "ML/ml_compiler.ML"
    3.10      "ML/ml_compiler0.ML"
    3.11 @@ -113,6 +112,7 @@
    3.12      "ML/ml_lex.ML"
    3.13      "ML/ml_name_space.ML"
    3.14      "ML/ml_options.ML"
    3.15 +    "ML/ml_pp.ML"
    3.16      "ML/ml_pretty.ML"
    3.17      "ML/ml_profiling.ML"
    3.18      "ML/ml_statistics.ML"
     4.1 --- a/src/Pure/ROOT.ML	Fri Mar 18 16:38:04 2016 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Fri Mar 18 16:38:40 2016 +0100
     4.3 @@ -393,8 +393,7 @@
     4.4  
     4.5  structure Output: OUTPUT = Output;  (*seal system channels!*)
     4.6  
     4.7 -
     4.8 -use "ML/install_pp_polyml.ML";
     4.9 +use "ML/ml_pp.ML";
    4.10  
    4.11  
    4.12  (* the Pure theory *)