# HG changeset patch # User wenzelm # Date 1455748138 -3600 # Node ID e307a410f46c66ac9261cbf4f2211c80f4fc469a # Parent 00f7618a9f2b2c272517aa66cc986d2621dd35f9 tuned; diff -r 00f7618a9f2b -r e307a410f46c src/Pure/General/secure.ML --- a/src/Pure/General/secure.ML Wed Feb 17 23:15:47 2016 +0100 +++ b/src/Pure/General/secure.ML Wed Feb 17 23:28:58 2016 +0100 @@ -13,7 +13,6 @@ val use_text: use_context -> {line: int, file: string, verbose: bool, debug: bool} -> string -> unit val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit - val toplevel_pp: string list -> string -> unit end; structure Secure: SECURE = @@ -36,11 +35,8 @@ val raw_use_text = use_text; val raw_use_file = use_file; -val raw_toplevel_pp = toplevel_pp; fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text); fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file); -fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp); - end; diff -r 00f7618a9f2b -r e307a410f46c src/Pure/ML/install_pp_polyml.ML --- a/src/Pure/ML/install_pp_polyml.ML Wed Feb 17 23:15:47 2016 +0100 +++ b/src/Pure/ML/install_pp_polyml.ML Wed Feb 17 23:28:58 2016 +0100 @@ -1,9 +1,63 @@ (* Title: Pure/ML/install_pp_polyml.ML Author: Makarius -Extra toplevel pretty-printing for Poly/ML. +ML toplevel pretty-printing for Poly/ML. *) +PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T => + ml_pretty (Pretty.to_ML (Pretty.str ""))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon => + ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn task => + ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task)))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn group => + ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group)))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn pos => + ml_pretty (Pretty.to_ML (Pretty.position pos))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn binding => + ml_pretty (Pretty.to_ML (Binding.pp binding))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn th => + ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn ct => + ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn cT => + ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn T => + ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn thy => + ml_pretty (Pretty.to_ML (Context.pretty_thy thy))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt => + ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn ast => + ml_pretty (Pretty.to_ML (Ast.pretty_ast ast))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn path => + ml_pretty (Pretty.to_ML (Path.pretty path))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn digest => + ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest))))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state => + ml_pretty (Pretty.to_ML (Pretty.str ""))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn st => + ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st))); + +PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism => + ml_pretty (Pretty.to_ML (Morphism.pretty morphism))); + PolyML.addPrettyPrinter (fn depth => fn _ => fn str => ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); @@ -107,4 +161,3 @@ end; end; - diff -r 00f7618a9f2b -r e307a410f46c src/Pure/RAW/ROOT_polyml.ML --- a/src/Pure/RAW/ROOT_polyml.ML Wed Feb 17 23:15:47 2016 +0100 +++ b/src/Pure/RAW/ROOT_polyml.ML Wed Feb 17 23:28:58 2016 +0100 @@ -189,10 +189,6 @@ if ML_System.name = "polyml-5.6" then use "RAW/ml_parse_tree_polyml-5.6.ML" else (); -fun toplevel_pp context (_: string list) pp = - use_text context {line = 1, file = "pp", verbose = false, debug = false} - ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); - fun ml_make_string struct_name = "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^ struct_name ^ ".ML_print_depth ())))))"; diff -r 00f7618a9f2b -r e307a410f46c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Feb 17 23:15:47 2016 +0100 +++ b/src/Pure/ROOT.ML Wed Feb 17 23:28:58 2016 +0100 @@ -47,8 +47,6 @@ Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file handle ERROR msg => (writeln msg; error "ML error")) (); -val toplevel_pp = Secure.toplevel_pp; - (** bootstrap phase 1: towards ML within Isar context *) @@ -333,27 +331,6 @@ structure Output: OUTPUT = Output; (*seal system channels!*) -(* ML toplevel pretty printing *) - -toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"\")"; -toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon"; -toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; -toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; -toplevel_pp ["Position", "T"] "Pretty.position"; -toplevel_pp ["Binding", "binding"] "Binding.pp"; -toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory"; -toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory"; -toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory"; -toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory"; -toplevel_pp ["Context", "theory"] "Context.pretty_thy"; -toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; -toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; -toplevel_pp ["Path", "T"] "Path.pretty"; -toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; -toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"\")"; -toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; -toplevel_pp ["Morphism", "morphism"] "Morphism.pretty"; - use "ML/install_pp_polyml.ML";