# HG changeset patch
# User wenzelm
# Date 1515522301 -3600
# Node ID be88c2bc8a455b2544fbe078c9967d80fd2a7e26
# Parent  1256460c063a867ff486e5a0e21899aae7930082
more accurate position for enclosing cartouche;

diff -r 1256460c063a -r be88c2bc8a45 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jan 09 18:30:21 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Jan 09 19:25:01 2018 +0100
@@ -84,16 +84,17 @@
 
 fun output_symbols_comment ctxt {antiq} (is_comment, syms) =
   if is_comment then
-    Latex.enclose_body ("%\n\\isamarkupcmt{") "}"
-      (output_text ctxt {markdown = false}
-        (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms)))
+    let
+      val content = Symbol_Pos.cartouche_content syms;
+      val source = Input.source true (Symbol_Pos.implode content) (Symbol_Pos.range content);
+    in Latex.enclose_body "%\n\\isamarkupcmt{" "}" (output_text ctxt {markdown = false} source) end
   else if antiq then maps output_symbols_antiq (Antiquote.parse (#1 (Symbol_Pos.range syms)) syms)
   else output_symbols syms;
 
 val scan_symbols_comment =
   Scan.many1 (fn (s, _) => s <> Symbol.comment andalso Symbol.not_eof s) >> pair false ||
   (Symbol_Pos.$$ Symbol.comment ::: Scan.many (Symbol.is_blank o Symbol_Pos.symbol)) --
-    Scan.option (Symbol_Pos.scan_cartouche_content "Document token error: ")
+    Scan.option (Symbol_Pos.scan_cartouche "Document token error: ")
       >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
 
 fun read_symbols_comment syms =