# HG changeset patch
# User wenzelm
# Date 1517662444 -3600
# Node ID 52e6ffa61e9c7d900dd5101d004380056fd93c43
# Parent  c555f1778dd8f6cda4c0b31bebcbe1cc8c98746a
clarified overall range: include delimiters;

diff -r c555f1778dd8 -r 52e6ffa61e9c src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Fri Feb 02 11:47:13 2018 +0100
+++ b/src/Pure/General/input.ML	Sat Feb 03 13:54:04 2018 +0100
@@ -14,6 +14,7 @@
   val source: bool -> Symbol_Pos.text -> Position.range -> source
   val empty: source
   val string: string -> source
+  val cartouche_content: Symbol_Pos.T list -> source
   val reset_pos: source -> source
   val source_explode: source -> Symbol_Pos.T list
   val source_content: source -> string
@@ -41,6 +42,12 @@
 
 fun string text = source true text Position.no_range;
 
+fun cartouche_content syms =
+  let
+    val range = Symbol_Pos.range syms;
+    val (text, _) = Symbol_Pos.implode_range range (Symbol_Pos.cartouche_content syms);
+  in source true text range end;
+
 fun reset_pos (Source {delimited, text, ...}) = source delimited text Position.no_range;
 
 
diff -r c555f1778dd8 -r 52e6ffa61e9c src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Feb 02 11:47:13 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Feb 03 13:54:04 2018 +0100
@@ -100,8 +100,7 @@
       |> maps output_symbols_antiq
   | (SOME Comment.Comment, _) =>
       let
-        val body = Symbol_Pos.cartouche_content syms;
-        val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
+        val source = Input.cartouche_content syms;
         val ctxt' = ctxt
           |> Config.put Document_Antiquotation.thy_output_display false;
       in