# HG changeset patch # User wenzelm # Date 1237663333 -3600 # Node ID 5bfea958f893965af368c8281f70bc8a722cfac8 # Parent be354d68c4e4e98be1974fb3a3e71e86c92cdd0a# Parent 4078276bcace17e42c59ebf5ca7b5372a1e74e94 merged diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Concurrent/future.ML --- 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); diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/General/pretty.ML --- 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 *) diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/General/secure.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/IsaMakefile --- 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 diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Isar/proof_context.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Isar/proof_display.ML --- 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 ""); -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 *) diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Isar/toplevel.ML --- 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 diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/ml_pretty.ML --- /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; + diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/mosml.ML --- 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 = (); diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-4.1.3.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-4.1.4.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-4.2.0.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-5.0.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-5.1.ML --- 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; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-experimental.ML --- 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 ^ "))"); + diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml.ML --- 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"; + diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml_common.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 diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml_pp.ML --- /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 ^ "))"); + diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/smlnj.ML --- 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 **) diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Syntax/ast.ML --- 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]; diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/context.ML --- 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 *) diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/pure_setup.ML --- 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 ();