src/Pure/Thy/thy_output.ML
changeset 23935 2a4e42ec9a54
parent 23863 8f3099589cfa
child 23942 079e99db59d7
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Jul 23 16:45:02 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Jul 23 16:45:03 2007 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4        | expand (Antiquote.Antiq x) =
     1.5            let val (opts, src) = Antiquote.scan_arguments lex antiq x in
     1.6              options opts (fn () => command src node) ();  (*preview errors!*)
     1.7 -            Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
     1.8 +            PrintMode.with_modes (! modes @ Latex.modes)
     1.9                (Output.no_warnings (options opts (fn () => command src node))) ()
    1.10            end;
    1.11      val ants = Antiquote.scan_antiquotes (str, pos);
    1.12 @@ -413,7 +413,7 @@
    1.13    ("display", Library.setmp display o boolean),
    1.14    ("break", Library.setmp break o boolean),
    1.15    ("quotes", Library.setmp quotes o boolean),
    1.16 -  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
    1.17 +  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
    1.18    ("margin", Pretty.setmp_margin o integer),
    1.19    ("indent", Library.setmp indent o integer),
    1.20    ("source", Library.setmp source o boolean),