src/Pure/Thy/latex.ML
changeset 27344 d44490b06190
parent 23703 1b6a2c119151
child 27755 f7cdde18aeb3
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Jun 24 19:43:19 2008 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Jun 24 19:43:20 2008 +0200
     1.3 @@ -91,7 +91,9 @@
     1.4  val output_syms_antiqs =
     1.5    Antiquote.scan_antiquotes #> map
     1.6    (fn Antiquote.Text s => output_syms s
     1.7 -    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
     1.8 +    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     1.9 +    | Antiquote.Open _ => "{\\isaantiqopen}"
    1.10 +    | Antiquote.Close _ => "{\\isaantiqclose}") #>
    1.11    implode;
    1.12  
    1.13  end;