# HG changeset patch
# User wenzelm
# Date 1125237893 -7200
# Node ID 1f12d55060bff08028f39aafe5aa9ad91caa47dd
# Parent  e7951b19104872e7a4c16b350a0d29cb84eda01a
output_basic: handle AltString token;

diff -r e7951b191048 -r 1f12d55060bf src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Aug 28 16:04:52 2005 +0200
+++ b/src/Pure/Thy/latex.ML	Sun Aug 28 16:04:53 2005 +0200
@@ -104,7 +104,10 @@
       "\\isacommand{" ^ output_syms s ^ "}"
     else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
       "\\isakeyword{" ^ output_syms s ^ "}"
-    else if T.is_kind T.String tok then output_syms (Library.quote s)
+    else if T.is_kind T.String tok then
+      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
+    else if T.is_kind T.AltString tok then
+      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
     else output_syms s
   end;