# HG changeset patch
# User wenzelm
# Date 1237661925 -3600
# Node ID d53d1a16d5eed8047fe4737dff85bb50e1468e70
# Parent  e755b8b76365ef73447a82bebd92143a416631bc
replaced install_pp/make_pp by more general toplevel_pp based on use_text;

diff -r e755b8b76365 -r d53d1a16d5ee src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/General/secure.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -14,6 +14,7 @@
   val use_file: ML_NameSpace.nameSpace ->
     (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
+  val toplevel_pp: string list -> string -> unit
   val commit: unit -> unit
   val system_out: string -> string * int
   val system: string -> int
@@ -41,6 +42,8 @@
 
 fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
 fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
+fun raw_toplevel_pp x =
+  toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
 
 fun use_text ns pos pr verbose txt =
   (secure_mltext (); raw_use_text ns pos pr verbose txt);
@@ -50,6 +53,8 @@
 
 fun use name = use_file ML_NameSpace.global Output.ml_output true name;
 
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+
 (*commit is dynamically bound!*)
 fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
 
@@ -73,5 +78,6 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+val toplevel_pp = Secure.toplevel_pp;
 val system_out = Secure.system_out;
 val system = Secure.system;
diff -r e755b8b76365 -r d53d1a16d5ee src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -119,10 +119,8 @@
     Meta.printLength := n);
 end;
 
-(*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
-(*the documentation refers to an installPP but I couldn't fine it!*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
+(*dummy implementation*)
+fun toplevel_pp _ _ _ _ _ = ();
 
 (*dummy implementation*)
 fun ml_prompts p1 p2 = ();
diff -r e755b8b76365 -r d53d1a16d5ee src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -74,13 +74,8 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
+(* print depth *)
 
-fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
-  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
-    fn () => brk (99999, 0), en);
-
-(*print depth*)
 local
   val depth = ref 10;
 in
diff -r e755b8b76365 -r d53d1a16d5ee src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/pure_setup.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -27,24 +27,25 @@
 
 (* ML toplevel pretty printing *)
 
-install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
-install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
-install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.position));
-install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o quote o Binding.str_of));
-install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
-install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
-install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
-install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
-install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
-install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
+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"] "Pretty.str o quote o Binding.str_of";
+toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
+toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
+toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Context", "theory"] "Context.pretty_thy";
+toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
+toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context";
+toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
+toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
+toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
 
-if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")) then
-  use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
-else if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
+if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
+then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
+else if String.isPrefix "polyml" ml_system
+then use "ML-Systems/install_pp_polyml.ML"
 else ();