--- 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;
--- 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