src/Pure/ML/install_pp_polyml.ML
changeset 62663 bea354f6ff21
parent 62503 19afb533028e
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
     2     Author:     Makarius
     2     Author:     Makarius
     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
     8   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
     8   (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
     9 
     9 
    10 PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
    10 PolyML.addPrettyPrinter
    11   ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
    11   (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
    12 
    12 
    13 PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
    13 PolyML.addPrettyPrinter
    14   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
    14   (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
    15 
    15 
    16 PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
    16 PolyML.addPrettyPrinter
    17   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
    17   (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    18 
    18 
    19 PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
    19 PolyML.addPrettyPrinter
    20   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
    20   (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
    21 
       
    22 PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
       
    23   ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
       
    24 
       
    25 PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
       
    26   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
       
    27 
       
    28 PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
       
    29   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
       
    30 
       
    31 PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
       
    32   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
       
    33 
       
    34 PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
       
    35   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
       
    36 
       
    37 PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
       
    38   ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
       
    39 
       
    40 PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
       
    41   ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
       
    42 
       
    43 PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
       
    44   ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
       
    45 
       
    46 PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
       
    47   ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
       
    48 
       
    49 PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
       
    50   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
       
    51 
       
    52 PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
       
    53   ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
       
    54 
       
    55 PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
       
    56   ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
       
    57 
       
    58 PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
       
    59   ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
       
    60 
       
    61 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
       
    62   ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
       
    63 
       
    64 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
       
    65   ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
       
    66 
       
    67 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
       
    68   pretty (Synchronized.value var, depth));
       
    69 
       
    70 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
    71   (case Future.peek x of
       
    72     NONE => PolyML.PrettyString "<future>"
       
    73   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
    74   | SOME (Exn.Res y) => pretty (y, depth)));
       
    75 
       
    76 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
    77   (case Lazy.peek x of
       
    78     NONE => PolyML.PrettyString "<lazy>"
       
    79   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
    80   | SOME (Exn.Res y) => pretty (y, depth)));
       
    81 
    21 
    82 
    22 
    83 local
    23 local
    84 
    24 
    85 open PolyML;
    25 open PolyML;