tuned;
authorwenzelm
Wed Feb 17 23:28:58 2016 +0100 (2016-02-17)
changeset 62356e307a410f46c
parent 62355 00f7618a9f2b
child 62357 ab76bd43c14a
tuned;
src/Pure/General/secure.ML
src/Pure/ML/install_pp_polyml.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/secure.ML	Wed Feb 17 23:15:47 2016 +0100
     1.2 +++ b/src/Pure/General/secure.ML	Wed Feb 17 23:28:58 2016 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    val use_text: use_context ->
     1.5      {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
     1.6    val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
     1.7 -  val toplevel_pp: string list -> string -> unit
     1.8  end;
     1.9  
    1.10  structure Secure: SECURE =
    1.11 @@ -36,11 +35,8 @@
    1.12  
    1.13  val raw_use_text = use_text;
    1.14  val raw_use_file = use_file;
    1.15 -val raw_toplevel_pp = toplevel_pp;
    1.16  
    1.17  fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
    1.18  fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
    1.19  
    1.20 -fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
    1.21 -
    1.22  end;
     2.1 --- a/src/Pure/ML/install_pp_polyml.ML	Wed Feb 17 23:15:47 2016 +0100
     2.2 +++ b/src/Pure/ML/install_pp_polyml.ML	Wed Feb 17 23:28:58 2016 +0100
     2.3 @@ -1,9 +1,63 @@
     2.4  (*  Title:      Pure/ML/install_pp_polyml.ML
     2.5      Author:     Makarius
     2.6  
     2.7 -Extra toplevel pretty-printing for Poly/ML.
     2.8 +ML toplevel pretty-printing for Poly/ML.
     2.9  *)
    2.10  
    2.11 +PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
    2.12 +  ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
    2.13 +
    2.14 +PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
    2.15 +  ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
    2.16 +
    2.17 +PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
    2.18 +  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
    2.19 +
    2.20 +PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
    2.21 +  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
    2.22 +
    2.23 +PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
    2.24 +  ml_pretty (Pretty.to_ML (Pretty.position pos)));
    2.25 +
    2.26 +PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
    2.27 +  ml_pretty (Pretty.to_ML (Binding.pp binding)));
    2.28 +
    2.29 +PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
    2.30 +  ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
    2.31 +
    2.32 +PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
    2.33 +  ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
    2.34 +
    2.35 +PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
    2.36 +  ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
    2.37 +
    2.38 +PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
    2.39 +  ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
    2.40 +
    2.41 +PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
    2.42 +  ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
    2.43 +
    2.44 +PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
    2.45 +  ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
    2.46 +
    2.47 +PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
    2.48 +  ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
    2.49 +
    2.50 +PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
    2.51 +  ml_pretty (Pretty.to_ML (Path.pretty path)));
    2.52 +
    2.53 +PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
    2.54 +  ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
    2.55 +
    2.56 +PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
    2.57 +  ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
    2.58 +
    2.59 +PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
    2.60 +  ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
    2.61 +
    2.62 +PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
    2.63 +  ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
    2.64 +
    2.65  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
    2.66    ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
    2.67  
    2.68 @@ -107,4 +161,3 @@
    2.69  end;
    2.70  
    2.71  end;
    2.72 -
     3.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:15:47 2016 +0100
     3.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:28:58 2016 +0100
     3.3 @@ -189,10 +189,6 @@
     3.4  if ML_System.name = "polyml-5.6"
     3.5  then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
     3.6  
     3.7 -fun toplevel_pp context (_: string list) pp =
     3.8 -  use_text context {line = 1, file = "pp", verbose = false, debug = false}
     3.9 -    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
    3.10 -
    3.11  fun ml_make_string struct_name =
    3.12    "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
    3.13      struct_name ^ ".ML_print_depth ())))))";
     4.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 23:15:47 2016 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Wed Feb 17 23:28:58 2016 +0100
     4.3 @@ -47,8 +47,6 @@
     4.4        Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
     4.5          handle ERROR msg => (writeln msg; error "ML error")) ();
     4.6  
     4.7 -val toplevel_pp = Secure.toplevel_pp;
     4.8 -
     4.9  
    4.10  
    4.11  (** bootstrap phase 1: towards ML within Isar context *)
    4.12 @@ -333,27 +331,6 @@
    4.13  structure Output: OUTPUT = Output;  (*seal system channels!*)
    4.14  
    4.15  
    4.16 -(* ML toplevel pretty printing *)
    4.17 -
    4.18 -toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
    4.19 -toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
    4.20 -toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    4.21 -toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
    4.22 -toplevel_pp ["Position", "T"] "Pretty.position";
    4.23 -toplevel_pp ["Binding", "binding"] "Binding.pp";
    4.24 -toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
    4.25 -toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
    4.26 -toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
    4.27 -toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
    4.28 -toplevel_pp ["Context", "theory"] "Context.pretty_thy";
    4.29 -toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    4.30 -toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
    4.31 -toplevel_pp ["Path", "T"] "Path.pretty";
    4.32 -toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
    4.33 -toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
    4.34 -toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    4.35 -toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
    4.36 -
    4.37  use "ML/install_pp_polyml.ML";
    4.38  
    4.39