PrintMode.with_modes;
authorwenzelm
Mon Jul 23 16:45:03 2007 +0200 (2007-07-23)
changeset 239352a4e42ec9a54
parent 23934 79393cb9c0a6
child 23936 66923825628e
PrintMode.with_modes;
src/Pure/Isar/isar_cmd.ML
src/Pure/ProofGeneral/pgml_isabelle.ML
src/Pure/Thy/html.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Jul 23 16:45:02 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Jul 23 16:45:03 2007 +0200
     1.3 @@ -331,15 +331,12 @@
     1.4  
     1.5  (* print state *)
     1.6  
     1.7 -fun with_modes modes e =
     1.8 -  Library.setmp print_mode (modes @ ! print_mode) e ();
     1.9 -
    1.10  fun set_limit _ NONE = ()
    1.11    | set_limit r (SOME n) = r := n;
    1.12  
    1.13  fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
    1.14    (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
    1.15 -    with_modes modes (fn () => Toplevel.print_state true state)));
    1.16 +    PrintMode.with_modes modes (Toplevel.print_state true) state));
    1.17  
    1.18  val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
    1.19  val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
    1.20 @@ -586,8 +583,9 @@
    1.21      val T = ProofContext.read_typ ctxt s;
    1.22    in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
    1.23  
    1.24 -fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () =>
    1.25 -  writeln (string_of (Toplevel.enter_proof_body state) arg)));
    1.26 +fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
    1.27 +  PrintMode.with_modes modes (fn () =>
    1.28 +    writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
    1.29  
    1.30  in
    1.31  
     2.1 --- a/src/Pure/ProofGeneral/pgml_isabelle.ML	Mon Jul 23 16:45:02 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/pgml_isabelle.ML	Mon Jul 23 16:45:03 2007 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  (** print mode **)
     2.5  
     2.6  val pgmlN = "PGML";
     2.7 -fun pgml_mode f x = setmp print_mode (pgmlN :: ! print_mode) f x;
     2.8 +fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x;
     2.9  
    2.10  val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", ""));
    2.11  
     3.1 --- a/src/Pure/Thy/html.ML	Mon Jul 23 16:45:02 2007 +0200
     3.2 +++ b/src/Pure/Thy/html.ML	Mon Jul 23 16:45:03 2007 +0200
     3.3 @@ -51,7 +51,7 @@
     3.4  (* mode *)
     3.5  
     3.6  val htmlN = "HTML";
     3.7 -fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;
     3.8 +fun html_mode f x = PrintMode.with_modes [htmlN] f x;
     3.9  
    3.10  
    3.11  (* symbol output *)
     4.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jul 23 16:45:02 2007 +0200
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jul 23 16:45:03 2007 +0200
     4.3 @@ -146,7 +146,7 @@
     4.4        | expand (Antiquote.Antiq x) =
     4.5            let val (opts, src) = Antiquote.scan_arguments lex antiq x in
     4.6              options opts (fn () => command src node) ();  (*preview errors!*)
     4.7 -            Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
     4.8 +            PrintMode.with_modes (! modes @ Latex.modes)
     4.9                (Output.no_warnings (options opts (fn () => command src node))) ()
    4.10            end;
    4.11      val ants = Antiquote.scan_antiquotes (str, pos);
    4.12 @@ -413,7 +413,7 @@
    4.13    ("display", Library.setmp display o boolean),
    4.14    ("break", Library.setmp break o boolean),
    4.15    ("quotes", Library.setmp quotes o boolean),
    4.16 -  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
    4.17 +  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
    4.18    ("margin", Pretty.setmp_margin o integer),
    4.19    ("indent", Library.setmp indent o integer),
    4.20    ("source", Library.setmp source o boolean),