src/Pure/Thy/thy_output.ML
changeset 37146 f652333bbf8e
parent 37145 01aa36932739
child 37198 3af985b10550
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4        | expand (Antiquote.Antiq (ss, (pos, _))) =
     1.5            let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
     1.6              options opts (fn () => command src state) ();  (*preview errors!*)
     1.7 -            PrintMode.with_modes (! modes @ Latex.modes)
     1.8 +            Print_Mode.with_modes (! modes @ Latex.modes)
     1.9                (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
    1.10            end
    1.11        | expand (Antiquote.Open _) = ""
    1.12 @@ -429,7 +429,7 @@
    1.13    ("display", setmp_CRITICAL display o boolean),
    1.14    ("break", setmp_CRITICAL break o boolean),
    1.15    ("quotes", setmp_CRITICAL quotes o boolean),
    1.16 -  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
    1.17 +  ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
    1.18    ("margin", setmp_CRITICAL Pretty.margin_default o integer),
    1.19    ("indent", setmp_CRITICAL indent o integer),
    1.20    ("source", setmp_CRITICAL source o boolean),