src/Pure/Thy/latex.ML
changeset 17169 1f12d55060bf
parent 17081 e19963723262
child 17186 797433ca1ab3
     1.1 --- a/src/Pure/Thy/latex.ML	Sun Aug 28 16:04:52 2005 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Aug 28 16:04:53 2005 +0200
     1.3 @@ -104,7 +104,10 @@
     1.4        "\\isacommand{" ^ output_syms s ^ "}"
     1.5      else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
     1.6        "\\isakeyword{" ^ output_syms s ^ "}"
     1.7 -    else if T.is_kind T.String tok then output_syms (Library.quote s)
     1.8 +    else if T.is_kind T.String tok then
     1.9 +      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
    1.10 +    else if T.is_kind T.AltString tok then
    1.11 +      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    1.12      else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
    1.13      else output_syms s
    1.14    end;