--- a/etc/options Thu Jan 03 21:36:58 2019 +0100
+++ b/etc/options Thu Jan 03 21:48:05 2019 +0100
@@ -279,6 +279,9 @@
section "Theory update"
+option update_inner_syntax_cartouches : bool = false
+ -- "update inner syntax (types, terms, etc.) to use cartouches"
+
option update_mixfix_cartouches : bool = false
-- "update mixfix templates to use cartouches instead of double quotes"
--- a/src/Pure/Syntax/syntax.ML Thu Jan 03 21:36:58 2019 +0100
+++ b/src/Pure/Syntax/syntax.ML Thu Jan 03 21:48:05 2019 +0100
@@ -203,6 +203,11 @@
val syms = Input.source_explode source;
val pos = Input.pos_of source;
val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
+ val _ =
+ if Options.default_bool "update_inner_syntax_cartouches" then
+ Context_Position.report_text ctxt
+ pos Markup.update (cartouche (Symbol_Pos.content syms))
+ else ();
in parse (syms, pos) end;
in
(case YXML.parse_body str handle Fail msg => error msg of