--- a/src/Pure/Concurrent/future.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Concurrent/future.ML Sat Mar 21 20:22:13 2009 +0100
@@ -44,6 +44,7 @@
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
val map: ('a -> 'b) -> 'a future -> 'b future
+ val interruptible_task: ('a -> 'b) -> 'a -> 'b
val interrupt_task: string -> unit
val cancel_group: group -> unit
val cancel: 'a future -> unit
@@ -350,6 +351,15 @@
(* cancellation *)
+fun interruptible_task f x =
+ if Multithreading.available then
+ Multithreading.with_attributes
+ (if is_some (thread_data ())
+ then Multithreading.restricted_interrupts
+ else Multithreading.regular_interrupts)
+ (fn _ => f) x
+ else interruptible f x;
+
(*interrupt: permissive signal, may get ignored*)
fun interrupt_task id = SYNCHRONIZED "interrupt"
(fn () => Task_Queue.interrupt_external (! queue) id);
--- a/src/Pure/General/pretty.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/General/pretty.ML Sat Mar 21 20:22:13 2009 +0100
@@ -19,9 +19,6 @@
a unit for breaking).
*)
-type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
- (unit -> unit) * (unit -> unit);
-
signature PRETTY =
sig
val default_indent: string -> int -> output
@@ -49,6 +46,7 @@
val commas: T list -> T list
val enclose: string -> string -> T list -> T
val enum: string -> string -> string -> T list -> T
+ val position: Position.T -> T
val list: string -> string -> T list -> T
val str_list: string -> string -> string list -> T
val big_list: string -> T list -> T
@@ -57,7 +55,8 @@
val setmargin: int -> unit
val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
val setdepth: int -> unit
- val pprint: T -> pprint_args -> unit
+ val to_ML: T -> ML_Pretty.pretty
+ val from_ML: ML_Pretty.pretty -> T
val symbolicN: string
val output_buffer: T -> Buffer.T
val output: T -> output
@@ -159,6 +158,9 @@
fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
+val position =
+ enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+
val list = enum ",";
fun str_list lpar rpar strs = list lpar rpar (map str strs);
@@ -318,20 +320,16 @@
| fmt (Break (true, _)) = Buffer.add (output_spaces 1);
in fmt (prune prt) Buffer.empty end;
-(*ML toplevel pretty printing*)
-fun pprint prt (put_str0, begin_blk, put_brk, put_fbrk, end_blk) =
- let
- fun put_str "" = ()
- | put_str s = put_str0 s;
- fun pp (Block (m, prts, ind, _)) =
- let val (bg, en) = Markup.output m
- in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end
- | pp (String (s, _)) = put_str s
- | pp (Break (false, wd)) = put_brk wd
- | pp (Break (true, _)) = put_fbrk ()
- and pp_lst [] = ()
- | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
- in pp (prune prt) end;
+
+(* ML toplevel pretty printing *)
+
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+ | to_ML (String s) = ML_Pretty.String s
+ | to_ML (Break b) = ML_Pretty.Break b;
+
+fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+ | from_ML (ML_Pretty.String s) = String s
+ | from_ML (ML_Pretty.Break b) = Break b;
(* output interfaces *)
--- a/src/Pure/General/secure.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/General/secure.ML Sat Mar 21 20:22:13 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;
--- a/src/Pure/IsaMakefile Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/IsaMakefile Sat Mar 21 20:22:13 2009 +0100
@@ -20,17 +20,17 @@
## Pure
BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
- ML-Systems/mosml.ML ML-Systems/multithreading.ML \
- ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
- ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
- ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
- ML-Systems/polyml_old_compiler4.ML \
- ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML \
- ML-Systems/smlnj.ML ML-Systems/system_shell.ML \
- ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML \
- ML-Systems/universal.ML
+ ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
+ ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
+ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
+ ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
+ ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML \
+ ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML \
+ ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \
+ ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
+ ML-Systems/time_limit.ML ML-Systems/universal.ML
RAW: $(OUT)/RAW
--- a/src/Pure/Isar/proof_context.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 21 20:22:13 2009 +0100
@@ -36,7 +36,6 @@
val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
val extern_fact: Proof.context -> string -> xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
- val pretty_thm_legacy: thm -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val pretty_thms: Proof.context -> thm list -> Pretty.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
@@ -296,10 +295,6 @@
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
-fun pretty_thm_legacy th =
- let val thy = Thm.theory_of_thm th
- in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-
fun pretty_thm ctxt th =
let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
--- a/src/Pure/Isar/proof_display.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Isar/proof_display.ML Sat Mar 21 20:22:13 2009 +0100
@@ -6,12 +6,12 @@
signature PROOF_DISPLAY =
sig
- val pprint_context: Proof.context -> pprint_args -> unit
- val pprint_typ: theory -> typ -> pprint_args -> unit
- val pprint_term: theory -> term -> pprint_args -> unit
- val pprint_ctyp: ctyp -> pprint_args -> unit
- val pprint_cterm: cterm -> pprint_args -> unit
- val pprint_thm: thm -> pprint_args -> unit
+ val pp_context: Proof.context -> Pretty.T
+ val pp_thm: thm -> Pretty.T
+ val pp_typ: theory -> typ -> Pretty.T
+ val pp_term: theory -> term -> Pretty.T
+ val pp_ctyp: ctyp -> Pretty.T
+ val pp_cterm: cterm -> Pretty.T
val print_theorems_diff: theory -> theory -> unit
val print_theorems: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T
@@ -26,18 +26,20 @@
(* toplevel pretty printing *)
-fun pprint_context ctxt = Pretty.pprint
+fun pp_context ctxt =
(if ! ProofContext.debug then
Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
else Pretty.str "<context>");
-fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
+fun pp_thm th =
+ let val thy = Thm.theory_of_thm th
+ in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-val pprint_typ = pprint Syntax.pretty_typ;
-val pprint_term = pprint Syntax.pretty_term;
-fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
+val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
+val pp_term = Pretty.quote oo Syntax.pretty_term_global;
+
+fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
(* theorems and theory *)
--- a/src/Pure/Isar/toplevel.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Isar/toplevel.ML Sat Mar 21 20:22:13 2009 +0100
@@ -311,7 +311,7 @@
fun controlled_execution f =
f
|> debugging
- |> interruptible;
+ |> Future.interruptible_task;
fun program f =
(f
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_pretty.ML Sat Mar 21 20:22:13 2009 +0100
@@ -0,0 +1,16 @@
+(* Title: Pure/ML-Systems/ml_pretty.ML
+ Author: Makarius
+
+Raw datatype for ML pretty printing.
+*)
+
+structure ML_Pretty =
+struct
+
+datatype pretty =
+ Block of (string * string) * pretty list * int |
+ String of string * int |
+ Break of bool * int;
+
+end;
+
--- a/src/Pure/ML-Systems/mosml.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/mosml.ML Sat Mar 21 20:22:13 2009 +0100
@@ -45,6 +45,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(*low-level pointer equality*)
@@ -118,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 = ();
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Sat Mar 21 20:22:13 2009 +0100
@@ -8,6 +8,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Sat Mar 21 20:22:13 2009 +0100
@@ -8,6 +8,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML Sat Mar 21 20:22:13 2009 +0100
@@ -7,6 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = Address.wordEq;
--- a/src/Pure/ML-Systems/polyml-5.0.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Sat Mar 21 20:22:13 2009 +0100
@@ -7,6 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-5.1.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Sat Mar 21 20:22:13 2009 +0100
@@ -6,6 +6,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-experimental.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Sat Mar 21 20:22:13 2009 +0100
@@ -12,13 +12,6 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-(* toplevel pretty printers *)
-
-(*dummy version*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-
(* runtime compilation *)
structure ML_NameSpace =
@@ -75,3 +68,16 @@
in use_text tune str_of_pos name_space (1, name) output verbose txt end;
end;
+
+
+(* toplevel pretty printing *)
+
+fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
+ | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+ | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
+ | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/polyml.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml.ML Sat Mar 21 20:22:13 2009 +0100
@@ -68,3 +68,6 @@
in use_text tune str_of_pos name_space (1, name) output verbose txt end;
end;
+
+use "ML-Systems/polyml_pp.ML";
+
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml_common.ML Sat Mar 21 20:22:13 2009 +0100
@@ -10,6 +10,7 @@
use "ML-Systems/time_limit.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(** ML system and platform related **)
@@ -73,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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml_pp.ML Sat Mar 21 20:22:13 2009 +0100
@@ -0,0 +1,20 @@
+(* Title: Pure/ML-Systems/polyml_pp.ML
+
+Toplevel pretty printing for Poly/ML before 5.3.
+*)
+
+fun ml_pprint (print, begin_blk, brk, end_blk) =
+ let
+ fun str "" = ()
+ | str s = print s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
+ | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
+ in pprint end;
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
+
--- a/src/Pure/ML-Systems/smlnj.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Mar 21 20:22:13 2009 +0100
@@ -13,6 +13,7 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
(*low-level pointer equality*)
@@ -97,22 +98,6 @@
fun makestring x = "dummy string for SML New Jersey";
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
-
-fun make_pp path pprint =
- let
- open PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (string pps, openHOVBox pps o Rel o dest_int,
- fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps,
- fn () => closeBox pps);
- in (path, pp) end;
-
-fun install_pp (path, pp) = CompilerPPTable.install_pp path pp;
-
-
(* ML command execution *)
fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
@@ -144,6 +129,26 @@
("structure " ^ name ^ " = struct end");
+(* toplevel pretty printing *)
+
+fun ml_pprint pps =
+ let
+ fun str "" = ()
+ | str s = PrettyPrint.string pps s;
+ fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+ (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
+ List.app pprint prts; PrettyPrint.closeBox pps; str en)
+ | pprint (ML_Pretty.String (s, _)) = str s
+ | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
+ | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
+ in pprint end;
+
+fun toplevel_pp tune str_of_pos output path pp =
+ use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+ ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
+ "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
+
+
(** interrupts **)
--- a/src/Pure/Syntax/ast.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Syntax/ast.ML Sat Mar 21 20:22:13 2009 +0100
@@ -20,7 +20,6 @@
val str_of_ast: ast -> string
val pretty_ast: ast -> Pretty.T
val pretty_rule: ast * ast -> Pretty.T
- val pprint_ast: ast -> pprint_args -> unit
val fold_ast: string -> ast list -> ast
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
@@ -79,8 +78,6 @@
| pretty_ast (Appl asts) =
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
-val pprint_ast = Pretty.pprint o pretty_ast;
-
fun pretty_rule (lhs, rhs) =
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
--- a/src/Pure/context.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/context.ML Sat Mar 21 20:22:13 2009 +0100
@@ -27,8 +27,6 @@
val display_names: theory -> string list
val pretty_thy: theory -> Pretty.T
val string_of_thy: theory -> string
- val pprint_thy: theory -> pprint_args -> unit
- val pprint_thy_ref: theory_ref -> pprint_args -> unit
val pretty_abbrev_thy: theory -> Pretty.T
val str_of_thy: theory -> string
val deref: theory_ref -> theory
@@ -228,7 +226,6 @@
val pretty_thy = Pretty.str_list "{" "}" o display_names;
val string_of_thy = Pretty.string_of o pretty_thy;
-val pprint_thy = Pretty.pprint o pretty_thy;
fun pretty_abbrev_thy thy =
let
@@ -256,8 +253,6 @@
else thy_ref
end;
-val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
-
(* build ids *)
--- a/src/Pure/pure_setup.ML Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/pure_setup.ML Sat Mar 21 20:22:13 2009 +0100
@@ -27,23 +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.enum "," "{" "}" o
- map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
-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 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 ();