src/Pure/Thy/latex.ML
changeset 27344 d44490b06190
parent 23703 1b6a2c119151
child 27755 f7cdde18aeb3
equal deleted inserted replaced
27343:4b28b80dd1f8 27344:d44490b06190
    89 val output_syms = output_symbols o Symbol.explode;
    89 val output_syms = output_symbols o Symbol.explode;
    90 
    90 
    91 val output_syms_antiqs =
    91 val output_syms_antiqs =
    92   Antiquote.scan_antiquotes #> map
    92   Antiquote.scan_antiquotes #> map
    93   (fn Antiquote.Text s => output_syms s
    93   (fn Antiquote.Text s => output_syms s
    94     | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
    94     | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
       
    95     | Antiquote.Open _ => "{\\isaantiqopen}"
       
    96     | Antiquote.Close _ => "{\\isaantiqclose}") #>
    95   implode;
    97   implode;
    96 
    98 
    97 end;
    99 end;
    98 
   100 
    99 
   101