src/Pure/Isar/isar_output.ML

 struct
 
 structure T = OuterLex;
 structure P = OuterParse;
 
-
-
 (** global references -- defaults for options **)
 
 val locale = ref "";
 val display = ref false;
 val quotes = ref false;

     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 (! modes @ Latex.modes @ ! print_mode)
-              (options opts (fn () => command src state)) ()
+              (Output.no_warnings (options opts (fn () => command src state))) ()
           end;
     val ants = Antiquote.antiquotes_of (str, pos);
   in
     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
       error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)