eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
authorwenzelm
Fri Aug 27 20:09:36 2010 +0200 (2010-08-27)
changeset 38832fc0aa40a1b08
parent 38831 4933a3dfd745
child 38833 9ff5ce3580c1
eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Aug 27 19:43:28 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 27 20:09:36 2010 +0200
     1.3 @@ -178,12 +178,11 @@
     1.4        | expand (Antiquote.Antiq (ss, (pos, _))) =
     1.5            let
     1.6              val (opts, src) = Token.read_antiq lex antiq (ss, pos);
     1.7 -            val opts_ctxt = fold option opts (Toplevel.presentation_context_of state);
     1.8 -            val cmd = wrap opts_ctxt (fn () => command src state opts_ctxt);
     1.9 -            val _ = cmd ();  (*preview errors!*)
    1.10 -          in
    1.11 -            Print_Mode.with_modes (! modes @ Latex.modes) (Output.no_warnings_CRITICAL cmd) ()
    1.12 -          end
    1.13 +            fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
    1.14 +            val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    1.15 +            val print_ctxt = Context_Position.set_visible false preview_ctxt;
    1.16 +            val _ = cmd preview_ctxt;
    1.17 +          in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end
    1.18        | expand (Antiquote.Open _) = ""
    1.19        | expand (Antiquote.Close _) = "";
    1.20      val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);