src/Pure/Thy/thy_output.ML
changeset 30589 cbe27c4ef417
parent 30588 05f81bbb2614
child 30590 1d9c9fcf8513
equal deleted inserted replaced
30588:05f81bbb2614 30589:cbe27c4ef417
   145 
   145 
   146 val modes = ref ([]: string list);
   146 val modes = ref ([]: string list);
   147 
   147 
   148 fun eval_antiquote lex state (txt, pos) =
   148 fun eval_antiquote lex state (txt, pos) =
   149   let
   149   let
   150     fun expand (Antiquote.Text s) = s
   150     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
   151       | expand (Antiquote.Antiq x) =
   151       | expand (Antiquote.Antiq x) =
   152           let val (opts, src) = T.read_antiq lex antiq x in
   152           let val (opts, src) = T.read_antiq lex antiq x in
   153             options opts (fn () => command src state) ();  (*preview errors!*)
   153             options opts (fn () => command src state) ();  (*preview errors!*)
   154             PrintMode.with_modes (! modes @ Latex.modes)
   154             PrintMode.with_modes (! modes @ Latex.modes)
   155               (Output.no_warnings (options opts (fn () => command src state))) ()
   155               (Output.no_warnings (options opts (fn () => command src state))) ()