--- a/src/HOL/Import/import_package.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Import/import_package.ML Tue Sep 18 18:05:37 2007 +0200
@@ -25,8 +25,8 @@
val debug = ref false
fun message s = if !debug then writeln s else ()
-val string_of_thm = PrintMode.with_default string_of_thm;
-val string_of_cterm = PrintMode.with_default string_of_cterm;
+val string_of_thm = PrintMode.setmp [] string_of_thm;
+val string_of_cterm = PrintMode.setmp [] string_of_cterm;
fun import_tac (thyname,thmname) =
if ! quick_and_dirty
--- a/src/HOL/Import/proof_kernel.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Sep 18 18:05:37 2007 +0200
@@ -200,7 +200,7 @@
handle TERM _ => ct)
in
quote(
- Library.setmp print_mode [] (
+ PrintMode.setmp [] (
Library.setmp show_brackets false (
Library.setmp show_all_types true (
Library.setmp Syntax.ambiguity_is_error false (
@@ -234,16 +234,15 @@
handle ERROR mesg => F (n+1)
| SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
in
- Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0
+ PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
end
handle ERROR mesg => simple_smart_string_of_cterm ct
val smart_string_of_thm = smart_string_of_cterm o cprop_of
-fun prth th = writeln (Library.setmp print_mode [] string_of_thm th)
-fun prc ct = writeln (Library.setmp print_mode [] string_of_cterm ct)
-fun prin t = writeln
- (Library.setmp print_mode [] (fn () => Sign.string_of_term (the_context ()) t) ());
+fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
+fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct)
+fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
let
(*val _ = writeln "Renaming:"
--- a/src/HOL/Import/shuffler.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Sep 18 18:05:37 2007 +0200
@@ -58,8 +58,8 @@
(*Prints an exception, then fails*)
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-val string_of_thm = Library.setmp print_mode [] string_of_thm;
-val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
+val string_of_thm = PrintMode.setmp [] string_of_thm;
+val string_of_cterm = PrintMode.setmp [] string_of_cterm;
fun mk_meta_eq th =
(case concl_of th of
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 18 18:05:37 2007 +0200
@@ -33,8 +33,7 @@
oracle mc_eindhoven_oracle ("term") =
{*
let
- val eindhoven_term =
- setmp print_mode ["Eindhoven"] o Sign.string_of_term;
+ val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Sign.string_of_term;
fun call_mc s =
let
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 18 18:05:37 2007 +0200
@@ -489,7 +489,7 @@
make_string sign (trm::list) =
Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
in
-(setmp print_mode ["Mucke"] (make_string sign) terms)
+ PrintMode.setmp ["Mucke"] (make_string sign) terms
end;
fun callmc s =
--- a/src/HOL/Tools/res_atp.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Sep 18 18:05:37 2007 +0200
@@ -946,7 +946,7 @@
val ctxt = ProofContext.init (theory_of_thm th)
in isar_atp (ctxt, [], th) end;
-val isar_atp_writeonly = PrintMode.with_default
+val isar_atp_writeonly = PrintMode.setmp []
(fn (ctxt, chain_ths, th) =>
if Thm.no_prems th then ()
else
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Sep 18 18:05:37 2007 +0200
@@ -19,8 +19,8 @@
structure IoaPackage: IOA_PACKAGE =
struct
-val string_of_typ = PrintMode.with_default o Sign.string_of_typ;
-val string_of_term = PrintMode.with_default o Sign.string_of_term;
+val string_of_typ = PrintMode.setmp [] o Sign.string_of_typ;
+val string_of_term = PrintMode.setmp [] o Sign.string_of_term;
exception malformed;
--- a/src/Pure/General/print_mode.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/Pure/General/print_mode.ML Tue Sep 18 18:05:37 2007 +0200
@@ -16,8 +16,8 @@
signature PRINT_MODE =
sig
include BASIC_PRINT_MODE
+ val setmp: string list -> ('a -> 'b) -> 'a -> 'b
val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
- val with_default: ('a -> 'b) -> 'a -> 'b
end;
structure PrintMode: PRINT_MODE =
@@ -28,11 +28,8 @@
fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
fun print_mode_active s = member (op =) (print_mode_value ()) s;
-fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
- setmp print_mode (modes @ ! print_mode) f x);
-
-fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
- setmp print_mode [] f x);
+fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);
+fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => setmp (modes @ ! print_mode) f x);
end;
--- a/src/Pure/Isar/toplevel.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Sep 18 18:05:37 2007 +0200
@@ -661,7 +661,7 @@
|> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
|> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
val _ =
- if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode)
+ if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ())
then print_state false result else ();
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
--- a/src/Pure/codegen.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/Pure/codegen.ML Tue Sep 18 18:05:37 2007 +0200
@@ -827,7 +827,7 @@
end;
fun gen_generate_code prep_term thy modules module =
- PrintMode.with_default (Pretty.setmp_margin (!margin) (fn xs =>
+ PrintMode.setmp [] (Pretty.setmp_margin (!margin) (fn xs =>
let
val _ = (module <> "" orelse
member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
@@ -921,7 +921,7 @@
map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
val (code, gr) = setmp mode ["term_of", "test"]
(generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
- val s = PrintMode.with_default (fn () => "structure TestTerm =\nstruct\n\n" ^
+ val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
space_implode "\n" (map snd code) ^
"\nopen Generated;\n\n" ^ Pretty.string_of
(Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
@@ -1004,7 +1004,7 @@
val eval_result = ref (Bound 0);
-fun eval_term thy = PrintMode.with_default (fn t =>
+fun eval_term thy = PrintMode.setmp [] (fn t =>
let
val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
error "Term to be evaluated contains type variables";
@@ -1051,7 +1051,7 @@
(**** Interface ****)
-val str = PrintMode.with_default Pretty.str;
+val str = PrintMode.setmp [] Pretty.str;
fun parse_mixfix rd s =
(case Scan.finite Symbol.stopper (Scan.repeat
--- a/src/Tools/code/code_target.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/Tools/code/code_target.ML Tue Sep 18 18:05:37 2007 +0200
@@ -56,7 +56,7 @@
infixr 5 @|;
fun x @@ y = [x, y];
fun xs @| y = xs @ [y];
-val str = PrintMode.with_default Pretty.str;
+val str = PrintMode.setmp [] Pretty.str;
val concat = Pretty.block o Pretty.breaks;
val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
fun semicolon ps = Pretty.block [concat ps, str ";"];
@@ -1033,7 +1033,7 @@
let
val output = case file
of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
- | SOME "-" => PrintMode.with_default writeln o code_output
+ | SOME "-" => PrintMode.setmp [] writeln o code_output
| SOME file => File.write (Path.explode file) o code_output;
in
parse_args (Scan.succeed ())
@@ -1044,10 +1044,10 @@
let
val output = case file
of NONE => error "OCaml: no internal compilation"
- | SOME "-" => PrintMode.with_default writeln o code_output
+ | SOME "-" => PrintMode.setmp [] writeln o code_output
| SOME file => File.write (Path.explode file) o code_output;
fun output_file file = File.write (Path.explode file) o code_output;
- val output_diag = PrintMode.with_default writeln o code_output;
+ val output_diag = PrintMode.setmp [] writeln o code_output;
in
parse_args (Scan.succeed ())
#> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
@@ -1381,7 +1381,7 @@
val pathname = Path.append destination filename;
val _ = File.mkdir (Path.dir pathname);
in File.write pathname end
- | write_module NONE _ = PrintMode.with_default writeln;
+ | write_module NONE _ = PrintMode.setmp [] writeln;
fun seri_module (modlname', (imports, (defs, _))) =
let
val imports' =
@@ -1449,7 +1449,7 @@
|> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
|> Pretty.chunks2
|> code_output
- |> PrintMode.with_default writeln
+ |> PrintMode.setmp [] writeln
end;
--- a/src/Tools/nbe.ML Tue Sep 18 18:05:34 2007 +0200
+++ b/src/Tools/nbe.ML Tue Sep 18 18:05:37 2007 +0200
@@ -373,7 +373,7 @@
val ct = Thm.cterm_of thy t;
val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
val ty = Term.type_of t';
- val p = Library.setmp print_mode (modes @ print_mode_value ()) (fn () =>
+ val p = PrintMode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
in Pretty.writeln p end;