simplified PrintMode interfaces;
authorwenzelm
Tue Sep 18 18:05:37 2007 +0200 (2007-09-18)
changeset 2463438db11874724
parent 24633 0a3a02066244
child 24635 c63f98b80bdd
simplified PrintMode interfaces;
src/HOL/Import/import_package.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/res_atp.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/Pure/General/print_mode.ML
src/Pure/Isar/toplevel.ML
src/Pure/codegen.ML
src/Tools/code/code_target.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Import/import_package.ML	Tue Sep 18 18:05:34 2007 +0200
     1.2 +++ b/src/HOL/Import/import_package.ML	Tue Sep 18 18:05:37 2007 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4  val debug = ref false
     1.5  fun message s = if !debug then writeln s else ()
     1.6  
     1.7 -val string_of_thm = PrintMode.with_default string_of_thm;
     1.8 -val string_of_cterm = PrintMode.with_default string_of_cterm;
     1.9 +val string_of_thm = PrintMode.setmp [] string_of_thm;
    1.10 +val string_of_cterm = PrintMode.setmp [] string_of_cterm;
    1.11  
    1.12  fun import_tac (thyname,thmname) =
    1.13      if ! quick_and_dirty
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 18 18:05:34 2007 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 18 18:05:37 2007 +0200
     2.3 @@ -200,7 +200,7 @@
     2.4  			   handle TERM _ => ct)
     2.5      in
     2.6  	quote(
     2.7 -	Library.setmp print_mode [] (
     2.8 +	PrintMode.setmp [] (
     2.9  	Library.setmp show_brackets false (
    2.10  	Library.setmp show_all_types true (
    2.11  	Library.setmp Syntax.ambiguity_is_error false (
    2.12 @@ -234,16 +234,15 @@
    2.13  	    handle ERROR mesg => F (n+1)
    2.14  		 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
    2.15      in
    2.16 -      Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    2.17 +      PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    2.18      end
    2.19      handle ERROR mesg => simple_smart_string_of_cterm ct
    2.20   
    2.21  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    2.22  
    2.23 -fun prth th = writeln (Library.setmp print_mode [] string_of_thm th)
    2.24 -fun prc ct = writeln (Library.setmp print_mode [] string_of_cterm ct)
    2.25 -fun prin t = writeln
    2.26 -  (Library.setmp print_mode [] (fn () => Sign.string_of_term (the_context ()) t) ());
    2.27 +fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
    2.28 +fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct)
    2.29 +fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
    2.30  fun pth (HOLThm(ren,thm)) =
    2.31      let
    2.32  	(*val _ = writeln "Renaming:"
     3.1 --- a/src/HOL/Import/shuffler.ML	Tue Sep 18 18:05:34 2007 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Tue Sep 18 18:05:37 2007 +0200
     3.3 @@ -58,8 +58,8 @@
     3.4  (*Prints an exception, then fails*)
     3.5  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     3.6  
     3.7 -val string_of_thm = Library.setmp print_mode [] string_of_thm;
     3.8 -val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
     3.9 +val string_of_thm = PrintMode.setmp [] string_of_thm;
    3.10 +val string_of_cterm = PrintMode.setmp [] string_of_cterm;
    3.11  
    3.12  fun mk_meta_eq th =
    3.13      (case concl_of th of
     4.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Tue Sep 18 18:05:34 2007 +0200
     4.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Tue Sep 18 18:05:37 2007 +0200
     4.3 @@ -33,8 +33,7 @@
     4.4  oracle mc_eindhoven_oracle ("term") =
     4.5  {*
     4.6  let
     4.7 -  val eindhoven_term =
     4.8 -    setmp print_mode ["Eindhoven"] o Sign.string_of_term;
     4.9 +  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Sign.string_of_term;
    4.10  
    4.11    fun call_mc s =
    4.12      let
     5.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Sep 18 18:05:34 2007 +0200
     5.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Sep 18 18:05:37 2007 +0200
     5.3 @@ -489,7 +489,7 @@
     5.4   	make_string sign (trm::list) =
     5.5             Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
     5.6  in
     5.7 -(setmp print_mode ["Mucke"] (make_string sign) terms)
     5.8 +  PrintMode.setmp ["Mucke"] (make_string sign) terms
     5.9  end;
    5.10  
    5.11  fun callmc s =
     6.1 --- a/src/HOL/Tools/res_atp.ML	Tue Sep 18 18:05:34 2007 +0200
     6.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Sep 18 18:05:37 2007 +0200
     6.3 @@ -946,7 +946,7 @@
     6.4        val ctxt = ProofContext.init (theory_of_thm th)
     6.5    in  isar_atp (ctxt, [], th)  end;
     6.6  
     6.7 -val isar_atp_writeonly = PrintMode.with_default
     6.8 +val isar_atp_writeonly = PrintMode.setmp []
     6.9        (fn (ctxt, chain_ths, th) =>
    6.10         if Thm.no_prems th then ()
    6.11         else
     7.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Sep 18 18:05:34 2007 +0200
     7.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Sep 18 18:05:37 2007 +0200
     7.3 @@ -19,8 +19,8 @@
     7.4  structure IoaPackage: IOA_PACKAGE =
     7.5  struct
     7.6  
     7.7 -val string_of_typ = PrintMode.with_default o Sign.string_of_typ;
     7.8 -val string_of_term = PrintMode.with_default o Sign.string_of_term;
     7.9 +val string_of_typ = PrintMode.setmp [] o Sign.string_of_typ;
    7.10 +val string_of_term = PrintMode.setmp [] o Sign.string_of_term;
    7.11  
    7.12  exception malformed;
    7.13  
     8.1 --- a/src/Pure/General/print_mode.ML	Tue Sep 18 18:05:34 2007 +0200
     8.2 +++ b/src/Pure/General/print_mode.ML	Tue Sep 18 18:05:37 2007 +0200
     8.3 @@ -16,8 +16,8 @@
     8.4  signature PRINT_MODE =
     8.5  sig
     8.6    include BASIC_PRINT_MODE
     8.7 +  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
     8.8    val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
     8.9 -  val with_default: ('a -> 'b) -> 'a -> 'b
    8.10  end;
    8.11  
    8.12  structure PrintMode: PRINT_MODE =
    8.13 @@ -28,11 +28,8 @@
    8.14  fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
    8.15  fun print_mode_active s = member (op =) (print_mode_value ()) s;
    8.16  
    8.17 -fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    8.18 -  setmp print_mode (modes @ ! print_mode) f x);
    8.19 -
    8.20 -fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    8.21 -  setmp print_mode [] f x);
    8.22 +fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);
    8.23 +fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => setmp (modes @ ! print_mode) f x);
    8.24  
    8.25  end;
    8.26  
     9.1 --- a/src/Pure/Isar/toplevel.ML	Tue Sep 18 18:05:34 2007 +0200
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Sep 18 18:05:37 2007 +0200
     9.3 @@ -661,7 +661,7 @@
     9.4          |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
     9.5          |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
     9.6      val _ =
     9.7 -      if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode)
     9.8 +      if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ())
     9.9        then print_state false result else ();
    9.10    in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
    9.11  
    10.1 --- a/src/Pure/codegen.ML	Tue Sep 18 18:05:34 2007 +0200
    10.2 +++ b/src/Pure/codegen.ML	Tue Sep 18 18:05:37 2007 +0200
    10.3 @@ -827,7 +827,7 @@
    10.4    end;
    10.5  
    10.6  fun gen_generate_code prep_term thy modules module =
    10.7 -  PrintMode.with_default (Pretty.setmp_margin (!margin) (fn xs =>
    10.8 +  PrintMode.setmp [] (Pretty.setmp_margin (!margin) (fn xs =>
    10.9    let
   10.10      val _ = (module <> "" orelse
   10.11          member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
   10.12 @@ -921,7 +921,7 @@
   10.13        map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
   10.14      val (code, gr) = setmp mode ["term_of", "test"]
   10.15        (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
   10.16 -    val s = PrintMode.with_default (fn () => "structure TestTerm =\nstruct\n\n" ^
   10.17 +    val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
   10.18        space_implode "\n" (map snd code) ^
   10.19        "\nopen Generated;\n\n" ^ Pretty.string_of
   10.20          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
   10.21 @@ -1004,7 +1004,7 @@
   10.22  
   10.23  val eval_result = ref (Bound 0);
   10.24  
   10.25 -fun eval_term thy = PrintMode.with_default (fn t =>
   10.26 +fun eval_term thy = PrintMode.setmp [] (fn t =>
   10.27    let
   10.28      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
   10.29        error "Term to be evaluated contains type variables";
   10.30 @@ -1051,7 +1051,7 @@
   10.31  
   10.32  (**** Interface ****)
   10.33  
   10.34 -val str = PrintMode.with_default Pretty.str;
   10.35 +val str = PrintMode.setmp [] Pretty.str;
   10.36  
   10.37  fun parse_mixfix rd s =
   10.38    (case Scan.finite Symbol.stopper (Scan.repeat
    11.1 --- a/src/Tools/code/code_target.ML	Tue Sep 18 18:05:34 2007 +0200
    11.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 18 18:05:37 2007 +0200
    11.3 @@ -56,7 +56,7 @@
    11.4  infixr 5 @|;
    11.5  fun x @@ y = [x, y];
    11.6  fun xs @| y = xs @ [y];
    11.7 -val str = PrintMode.with_default Pretty.str;
    11.8 +val str = PrintMode.setmp [] Pretty.str;
    11.9  val concat = Pretty.block o Pretty.breaks;
   11.10  val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
   11.11  fun semicolon ps = Pretty.block [concat ps, str ";"];
   11.12 @@ -1033,7 +1033,7 @@
   11.13    let
   11.14      val output = case file
   11.15       of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
   11.16 -      | SOME "-" => PrintMode.with_default writeln o code_output
   11.17 +      | SOME "-" => PrintMode.setmp [] writeln o code_output
   11.18        | SOME file => File.write (Path.explode file) o code_output;
   11.19    in
   11.20      parse_args (Scan.succeed ())
   11.21 @@ -1044,10 +1044,10 @@
   11.22    let
   11.23      val output = case file
   11.24       of NONE => error "OCaml: no internal compilation"
   11.25 -      | SOME "-" => PrintMode.with_default writeln o code_output
   11.26 +      | SOME "-" => PrintMode.setmp [] writeln o code_output
   11.27        | SOME file => File.write (Path.explode file) o code_output;
   11.28      fun output_file file = File.write (Path.explode file) o code_output;
   11.29 -    val output_diag = PrintMode.with_default writeln o code_output;
   11.30 +    val output_diag = PrintMode.setmp [] writeln o code_output;
   11.31    in
   11.32      parse_args (Scan.succeed ())
   11.33      #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
   11.34 @@ -1381,7 +1381,7 @@
   11.35              val pathname = Path.append destination filename;
   11.36              val _ = File.mkdir (Path.dir pathname);
   11.37            in File.write pathname end
   11.38 -      | write_module NONE _ = PrintMode.with_default writeln;
   11.39 +      | write_module NONE _ = PrintMode.setmp [] writeln;
   11.40      fun seri_module (modlname', (imports, (defs, _))) =
   11.41        let
   11.42          val imports' =
   11.43 @@ -1449,7 +1449,7 @@
   11.44      |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
   11.45      |> Pretty.chunks2
   11.46      |> code_output
   11.47 -    |> PrintMode.with_default writeln
   11.48 +    |> PrintMode.setmp [] writeln
   11.49    end;
   11.50  
   11.51  
    12.1 --- a/src/Tools/nbe.ML	Tue Sep 18 18:05:34 2007 +0200
    12.2 +++ b/src/Tools/nbe.ML	Tue Sep 18 18:05:37 2007 +0200
    12.3 @@ -373,7 +373,7 @@
    12.4      val ct = Thm.cterm_of thy t;
    12.5      val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
    12.6      val ty = Term.type_of t';
    12.7 -    val p = Library.setmp print_mode (modes @ print_mode_value ()) (fn () =>
    12.8 +    val p = PrintMode.with_modes modes (fn () =>
    12.9        Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
   12.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
   12.11    in Pretty.writeln p end;