# HG changeset patch
# User wenzelm
# Date 977608407 -3600
# Node ID ec19f5902ef51245c96c1c03df31c5d24163278a
# Parent  3a610089c43ba91bc3a3ef5a67910362779cf6a9
antiq: preview errors;

diff -r 3a610089c43b -r ec19f5902ef5 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sat Dec 23 22:53:05 2000 +0100
+++ b/src/Pure/Isar/isar_output.ML	Sat Dec 23 22:53:27 2000 +0100
@@ -141,6 +141,7 @@
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
           let val (opts, src) = antiq_args lex x in
+            options opts (fn () => command src state) ();  (*preview errors!*)
             Library.setmp print_mode (Latex.modes @ ! print_mode)
               (options opts (fn () => command src state)) ()
           end;