--- a/src/Pure/Thy/thy_output.ML Sun Jan 07 22:18:59 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Jan 08 11:41:16 2018 +0100
@@ -273,11 +273,14 @@
Scan.option (Symbol_Pos.scan_cartouche_content "Document token error: ")
>> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
+val read_symbols_comment =
+ Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment);
+
in
fun output_body state antiq bg en syms =
(if exists (fn (s, _) => s = Symbol.comment) syms then
- (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms of
+ (case read_symbols_comment syms of
SOME res => maps (output_symbols_comment state {antiq = antiq}) res
| NONE => output_symbols syms)
else output_symbols syms) |> Latex.enclose_body bg en