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