Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML/install_pp_polyml.ML
changeset 62503 19afb533028e
parent 62387 ad3eb2889f9a
child 62663 bea354f6ff21
equal deleted inserted replaced
62502:8857237c3a90 62503:19afb533028e 
     3 
     3 
     4 ML toplevel pretty-printing for Poly/ML.
 
     4 ML toplevel pretty-printing for Poly/ML.
 
     5 *)
 
     5 *)
 
     6 
     6 
     7 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
 
     7 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
 
     8   ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
 
     8   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
 
     9 
     9 
    10 PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
 
    10 PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
 
    11   ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
 
    11   ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
 
    12 
    12 
    13 PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
 
    13 PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
 
    14   ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
 
    14   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
 
    15 
    15 
    16 PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
 
    16 PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
 
    17   ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
 
    17   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
 
    18 
    18 
    19 PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
 
    19 PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
 
    20   ml_pretty (Pretty.to_ML (Pretty.position pos)));
 
    20   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
 
    21 
    21 
    22 PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
 
    22 PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
 
    23   ml_pretty (Pretty.to_ML (Binding.pp binding)));
 
    23   ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
 
    24 
    24 
    25 PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
 
    25 PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
 
    26   ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
 
    26   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
 
    27 
    27 
    28 PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
 
    28 PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
 
    29   ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
 
    29   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
 
    30 
    30 
    31 PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
 
    31 PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
 
    32   ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
 
    32   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
 
    33 
    33 
    34 PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
 
    34 PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
 
    35   ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
 
    35   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
 
    36 
    36 
    37 PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
 
    37 PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
 
    38   ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
 
    38   ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
 
    39 
    39 
    40 PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
 
    40 PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
 
    41   ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
 
    41   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
 
    42 
    42 
    43 PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
 
    43 PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
 
    44   ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
 
    44   ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
 
    45 
    45 
    46 PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
 
    46 PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
 
    47   ml_pretty (Pretty.to_ML (Path.pretty path)));
 
    47   ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
 
    48 
    48 
    49 PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
 
    49 PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
 
    50   ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
 
    50   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
 
    51 
    51 
    52 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
 
    52 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
 
    53   ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
 
    53   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
 
    54 
    54 
    55 PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
 
    55 PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
 
    56   ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
 
    56   ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
 
    57 
    57 
    58 PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
 
    58 PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
 
    59   ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
 
    59   ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
 
    60 
    60 
    61 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
 
    61 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
 
    62   ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
 
    62   ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
 
    63 
    63 
    64 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
 
    64 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
 
    65   ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
 
    65   ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
 
    66 
    66 
    67 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
 
    67 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
 
    68   pretty (Synchronized.value var, depth));
 
    68   pretty (Synchronized.value var, depth));
 
    69 
    69 
    70 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
 
    70 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
 
    81 
    81 
    82 
    82 
    83 local
 
    83 local
 
    84 
    84 
    85 open PolyML;
 
    85 open PolyML;
 
    86 val from_ML = Pretty.from_ML o pretty_ml;
 
    86 val from_ML = Pretty.from_ML o ML_Pretty.from_polyml;
 
    87 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
 
    87 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
 
    88 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
 
    88 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
 
    89 
    89 
    90 fun prt_term parens (dp: FixedInt.int) t =
 
    90 fun prt_term parens (dp: FixedInt.int) t =
 
    91   if dp <= 0 then Pretty.str "..."
 
    91   if dp <= 0 then Pretty.str "..."
 
   108 
   108 
   109 in
 
   109 in
 
   110 
   110 
   111 val _ =
 
   111 val _ =
 
   112   PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
 
   112   PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
 
   113     ml_pretty (Pretty.to_ML (prt_term false depth t)));
 
   113     ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
 
   114 
   114 
   115 local
 
   115 local
 
   116 
   116 
   117 fun prt_proof parens dp prf =
 
   117 fun prt_proof parens dp prf =
 
   118   if dp <= 0 then Pretty.str "..."
 
   118   if dp <= 0 then Pretty.str "..."
 
   155 
   155 
   156 in
 
   156 in
 
   157 
   157 
   158 val _ =
 
   158 val _ =
 
   159   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
 
   159   PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
 
   160     ml_pretty (Pretty.to_ML (prt_proof false depth prf)));
 
   160     ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
 
   161 
   161 
   162 end;
 
   162 end;
 
   163 
   163 
   164 end;
 
   164 end;
isabelle