# HG changeset patch
# User wenzelm
# Date 1125325087 -7200
# Node ID 797433ca1ab35be6ce99ae66771dfeb69c8c8c9c
# Parent  5140808111d122e5fc1365714336483443e41a8d
delimiter markup for verbatim tokens;

diff -r 5140808111d1 -r 797433ca1ab3 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Aug 29 16:18:06 2005 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Aug 29 16:18:07 2005 +0200
@@ -108,7 +108,8 @@
       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 if T.is_kind T.Verbatim tok then
+      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" (output_syms s)
     else output_syms s
   end;