tuned;
authorwenzelm
Wed May 16 15:18:18 2018 +0200 (12 months ago)
changeset 68194796f2585c7ee
parent 68193 14dd78f036ba
child 68195 607957640057
tuned;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Wed May 16 15:18:12 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed May 16 15:18:18 2018 +0200
     1.3 @@ -117,13 +117,14 @@
     1.4        |> maps output_symbols_antiq
     1.5    | (SOME comment, _) => output_comment ctxt (comment, syms));
     1.6  
     1.7 -in
     1.8 -
     1.9  fun output_body ctxt antiq bg en syms =
    1.10    Comment.read_body syms
    1.11    |> maps (output_comment_symbols ctxt {antiq = antiq})
    1.12 -  |> Latex.enclose_body bg en
    1.13 -and output_token ctxt tok =
    1.14 +  |> Latex.enclose_body bg en;
    1.15 +
    1.16 +in
    1.17 +
    1.18 +fun output_token ctxt tok =
    1.19    let
    1.20      fun output antiq bg en =
    1.21        output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));