src/Pure/Thy/latex.ML
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30642 0c9f9c49d5df
equal deleted inserted replaced
30612:cb6421b6a18f 30613:b22d35d9ef28
   115     else if T.is_kind T.AltString tok then
   115     else if T.is_kind T.AltString tok then
   116       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   116       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
   117     else if T.is_kind T.Verbatim tok then
   117     else if T.is_kind T.Verbatim tok then
   118       let
   118       let
   119         val (txt, pos) = T.source_position_of tok;
   119         val (txt, pos) = T.source_position_of tok;
   120         val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   120         val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   121         val out = implode (map output_syms_antiq ants);
   121         val out = implode (map output_syms_antiq ants);
   122       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   122       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
   123     else output_syms s
   123     else output_syms s
   124   end;
   124   end;
   125 
   125