# HG changeset patch
# User wenzelm
# Date 1176382873 -7200
# Node ID 8c6b4f7548e3cecb8e02c7707410c716f0671ebb
# Parent  d920afb63323a8ff3b41a53e7a5e51985e858832
output_basic: added isaantiq markup (only inside verbatim tokens);

diff -r d920afb63323 -r 8c6b4f7548e3 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Apr 12 15:01:11 2007 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Apr 12 15:01:13 2007 +0200
@@ -88,6 +88,12 @@
 val output_symbols = output_known_symbols (K true, K true);
 val output_syms = output_symbols o Symbol.explode;
 
+val output_syms_antiqs =
+  Antiquote.scan_antiquotes #> map
+  (fn Antiquote.Text s => output_syms s
+    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
+  implode;
+
 end;
 
 
@@ -109,7 +115,8 @@
     else if T.is_kind T.AltString tok then
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if T.is_kind T.Verbatim tok then
-      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" (output_syms s)
+      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
+        (output_syms_antiqs (s, T.position_of tok))
     else output_syms s
   end;