# HG changeset patch
# User wenzelm
# Date 1515419990 -3600
# Node ID c0c36348a4fb3d9593c4d2565d425b6bcba1f954
# Parent  5a049cf984380946650a6c90c93d4c7421f7d2ad
tuned;

diff -r 5a049cf98438 -r c0c36348a4fb src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Jan 08 14:28:41 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Jan 08 14:59:50 2018 +0100
@@ -273,17 +273,17 @@
     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);
+fun read_symbols_comment syms =
+  if exists (fn (s, _) => s = Symbol.comment) syms then
+    Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms
+  else NONE;
 
 in
 
 fun output_body state antiq bg en syms =
-  (if exists (fn (s, _) => s = Symbol.comment) syms then
-    (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
+  (case read_symbols_comment syms of
+    SOME res => maps (output_symbols_comment state {antiq = antiq}) res
+  | NONE => output_symbols syms) |> Latex.enclose_body bg en
 and output_token state tok =
   let
     val syms = Input.source_explode (Token.input_of tok);