# HG changeset patch
# User wenzelm
# Date 1190131537 -7200
# Node ID 38db1187472464743f0f90b9481976df0a8cf962
# Parent  0a3a020662444113dfe4beded4d5a992838c7db9
simplified PrintMode interfaces;

diff -r 0a3a02066244 -r 38db11874724 src/HOL/Import/import_package.ML
--- 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
diff -r 0a3a02066244 -r 38db11874724 src/HOL/Import/proof_kernel.ML
--- 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:"
diff -r 0a3a02066244 -r 38db11874724 src/HOL/Import/shuffler.ML
--- 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
diff -r 0a3a02066244 -r 38db11874724 src/HOL/Modelcheck/EindhovenSyn.thy
--- 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
diff -r 0a3a02066244 -r 38db11874724 src/HOL/Modelcheck/mucke_oracle.ML
--- 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 =
diff -r 0a3a02066244 -r 38db11874724 src/HOL/Tools/res_atp.ML
--- 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
diff -r 0a3a02066244 -r 38db11874724 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- 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;
 
diff -r 0a3a02066244 -r 38db11874724 src/Pure/General/print_mode.ML
--- 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;
 
diff -r 0a3a02066244 -r 38db11874724 src/Pure/Isar/toplevel.ML
--- 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;
 
diff -r 0a3a02066244 -r 38db11874724 src/Pure/codegen.ML
--- 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
diff -r 0a3a02066244 -r 38db11874724 src/Tools/code/code_target.ML
--- 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;
 
 
diff -r 0a3a02066244 -r 38db11874724 src/Tools/nbe.ML
--- 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;