output_basic: added isaantiq markup (only inside verbatim tokens);
authorwenzelm
Thu Apr 12 15:01:13 2007 +0200 (2007-04-12)
changeset 226488c6b4f7548e3
parent 22647 d920afb63323
child 22649 6cf96b9f7b9e
output_basic: added isaantiq markup (only inside verbatim tokens);
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Thu Apr 12 15:01:11 2007 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Thu Apr 12 15:01:13 2007 +0200
     1.3 @@ -88,6 +88,12 @@
     1.4  val output_symbols = output_known_symbols (K true, K true);
     1.5  val output_syms = output_symbols o Symbol.explode;
     1.6  
     1.7 +val output_syms_antiqs =
     1.8 +  Antiquote.scan_antiquotes #> map
     1.9 +  (fn Antiquote.Text s => output_syms s
    1.10 +    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
    1.11 +  implode;
    1.12 +
    1.13  end;
    1.14  
    1.15  
    1.16 @@ -109,7 +115,8 @@
    1.17      else if T.is_kind T.AltString tok then
    1.18        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    1.19      else if T.is_kind T.Verbatim tok then
    1.20 -      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" (output_syms s)
    1.21 +      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
    1.22 +        (output_syms_antiqs (s, T.position_of tok))
    1.23      else output_syms s
    1.24    end;
    1.25