src/Pure/ML/install_pp_polyml.ML
author wenzelm
Tue, 23 Feb 2016 16:20:12 +0100
changeset 62387 ad3eb2889f9a
parent 62356 e307a410f46c
child 62503 19afb533028e
permissions -rw-r--r--
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47980
c81801f881b3 simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents: 43791
diff changeset
     1
(*  Title:      Pure/ML/install_pp_polyml.ML
38327
d6afb77b0f6d more precise and more maintainable dependencies;
wenzelm
parents: 33767
diff changeset
     2
    Author:     Makarius
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     3
62356
wenzelm
parents: 52426
diff changeset
     4
ML toplevel pretty-printing for Poly/ML.
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     5
*)
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     6
62356
wenzelm
parents: 52426
diff changeset
     7
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
wenzelm
parents: 52426
diff changeset
     8
  ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
wenzelm
parents: 52426
diff changeset
     9
wenzelm
parents: 52426
diff changeset
    10
PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
wenzelm
parents: 52426
diff changeset
    11
  ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
wenzelm
parents: 52426
diff changeset
    12
wenzelm
parents: 52426
diff changeset
    13
PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
wenzelm
parents: 52426
diff changeset
    14
  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
wenzelm
parents: 52426
diff changeset
    15
wenzelm
parents: 52426
diff changeset
    16
PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
wenzelm
parents: 52426
diff changeset
    17
  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
wenzelm
parents: 52426
diff changeset
    18
wenzelm
parents: 52426
diff changeset
    19
PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
wenzelm
parents: 52426
diff changeset
    20
  ml_pretty (Pretty.to_ML (Pretty.position pos)));
wenzelm
parents: 52426
diff changeset
    21
wenzelm
parents: 52426
diff changeset
    22
PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
wenzelm
parents: 52426
diff changeset
    23
  ml_pretty (Pretty.to_ML (Binding.pp binding)));
wenzelm
parents: 52426
diff changeset
    24
wenzelm
parents: 52426
diff changeset
    25
PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
wenzelm
parents: 52426
diff changeset
    26
  ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
wenzelm
parents: 52426
diff changeset
    27
wenzelm
parents: 52426
diff changeset
    28
PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
wenzelm
parents: 52426
diff changeset
    29
  ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
wenzelm
parents: 52426
diff changeset
    30
wenzelm
parents: 52426
diff changeset
    31
PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
wenzelm
parents: 52426
diff changeset
    32
  ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
wenzelm
parents: 52426
diff changeset
    33
wenzelm
parents: 52426
diff changeset
    34
PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
wenzelm
parents: 52426
diff changeset
    35
  ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
wenzelm
parents: 52426
diff changeset
    36
wenzelm
parents: 52426
diff changeset
    37
PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
wenzelm
parents: 52426
diff changeset
    38
  ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
wenzelm
parents: 52426
diff changeset
    39
wenzelm
parents: 52426
diff changeset
    40
PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
wenzelm
parents: 52426
diff changeset
    41
  ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
wenzelm
parents: 52426
diff changeset
    42
wenzelm
parents: 52426
diff changeset
    43
PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
wenzelm
parents: 52426
diff changeset
    44
  ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
wenzelm
parents: 52426
diff changeset
    45
wenzelm
parents: 52426
diff changeset
    46
PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
wenzelm
parents: 52426
diff changeset
    47
  ml_pretty (Pretty.to_ML (Path.pretty path)));
wenzelm
parents: 52426
diff changeset
    48
wenzelm
parents: 52426
diff changeset
    49
PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
wenzelm
parents: 52426
diff changeset
    50
  ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
wenzelm
parents: 52426
diff changeset
    51
wenzelm
parents: 52426
diff changeset
    52
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
wenzelm
parents: 52426
diff changeset
    53
  ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
wenzelm
parents: 52426
diff changeset
    54
wenzelm
parents: 52426
diff changeset
    55
PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
wenzelm
parents: 52426
diff changeset
    56
  ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
wenzelm
parents: 52426
diff changeset
    57
wenzelm
parents: 52426
diff changeset
    58
PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
wenzelm
parents: 52426
diff changeset
    59
  ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
wenzelm
parents: 52426
diff changeset
    60
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
    61
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    62
  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
    63
43791
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    64
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    65
  ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
43791
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    66
33767
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    67
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    68
  pretty (Synchronized.value var, depth));
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    69
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    70
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    71
  (case Future.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    72
    NONE => PolyML.PrettyString "<future>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    73
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 41415
diff changeset
    74
  | SOME (Exn.Res y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    75
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    76
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    77
  (case Lazy.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    78
    NONE => PolyML.PrettyString "<lazy>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    79
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 41415
diff changeset
    80
  | SOME (Exn.Res y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    81
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    82
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    83
local
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    84
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    85
open PolyML;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    86
val from_ML = Pretty.from_ML o pretty_ml;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    87
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    88
fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    89
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    90
fun prt_term parens (dp: FixedInt.int) t =
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    91
  if dp <= 0 then Pretty.str "..."
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    92
  else
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    93
    (case t of
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    94
      _ $ _ =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    95
        op :: (strip_comb t)
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
    96
        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    97
        |> Pretty.separate " $"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    98
        |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
    99
    | Abs (a, T, b) =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   100
        prt_apps "Abs"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   101
         [from_ML (prettyRepresentation (a, dp - 1)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   102
          from_ML (prettyRepresentation (T, dp - 2)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   103
          prt_term false (dp - 3) b]
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   104
    | Const a => prt_app "Const" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   105
    | Free a => prt_app "Free" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   106
    | Var a => prt_app "Var" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   107
    | Bound a => prt_app "Bound" (from_ML (prettyRepresentation (a, dp - 1))));
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   108
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   109
in
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   110
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   111
val _ =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   112
  PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   113
    ml_pretty (Pretty.to_ML (prt_term false depth t)));
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   114
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   115
local
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   116
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   117
fun prt_proof parens dp prf =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   118
  if dp <= 0 then Pretty.str "..."
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   119
  else
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   120
    (case prf of
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   121
      _ % _ => prt_proofs parens dp prf
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   122
    | _ %% _ => prt_proofs parens dp prf
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   123
    | Abst (a, T, b) =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   124
        prt_apps "Abst"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   125
         [from_ML (prettyRepresentation (a, dp - 1)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   126
          from_ML (prettyRepresentation (T, dp - 2)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   127
          prt_proof false (dp - 3) b]
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   128
    | AbsP (a, t, b) =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   129
        prt_apps "AbsP"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   130
         [from_ML (prettyRepresentation (a, dp - 1)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   131
          from_ML (prettyRepresentation (t, dp - 2)),
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   132
          prt_proof false (dp - 3) b]
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   133
    | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   134
    | MinProof => Pretty.str "MinProof"
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   135
    | PBound a => prt_app "PBound" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   136
    | PAxm a => prt_app "PAxm" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   137
    | OfClass a => prt_app "OfClass" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   138
    | Oracle a => prt_app "Oracle" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   139
    | Promise a => prt_app "Promise" (from_ML (prettyRepresentation (a, dp - 1)))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   140
    | PThm a => prt_app "PThm" (from_ML (prettyRepresentation (a, dp - 1))))
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   141
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   142
and prt_proofs parens dp prf =
33545
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
   143
  let
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   144
    val (head, args) = strip_proof prf [];
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
   145
    val prts =
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62356
diff changeset
   146
      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   147
  in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   148
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   149
and strip_proof (p % t) res =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   150
      strip_proof p
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   151
        ((fn d => [Pretty.str " %", Pretty.brk 1, from_ML (prettyRepresentation (t, d))]) :: res)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   152
  | strip_proof (p %% q) res =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   153
      strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   154
  | strip_proof p res = (fn d => prt_proof true d p, res);
33545
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
   155
52426
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   156
in
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   157
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   158
val _ =
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   159
  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   160
    ml_pretty (Pretty.to_ML (prt_proof false depth prf)));
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   161
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   162
end;
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   163
81e27230a8b7 ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);
wenzelm
parents: 52425
diff changeset
   164
end;