src/Pure/Thy/thy_output.ML
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30635 a7d175c48228
equal deleted inserted replaced
30612:cb6421b6a18f 30613:b22d35d9ef28
   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))) ()
   156           end
   156           end
   157       | expand (Antiquote.Open _) = ""
   157       | expand (Antiquote.Open _) = ""
   158       | expand (Antiquote.Close _) = "";
   158       | expand (Antiquote.Close _) = "";
   159     val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   159     val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   160   in
   160   in
   161     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
   161     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
   162       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
   162       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
   163     else implode (map expand ants)
   163     else implode (map expand ants)
   164   end;
   164   end;