# HG changeset patch
# User wenzelm
# Date 1546548485 -3600
# Node ID e15f053a42d88c991bfe2eff81dc1a1fe03c80bd
# Parent  2b85a9294b2a8138895b375fedb3ce337fc50d62
support for isabelle update -u inner_syntax_cartouches;

diff -r 2b85a9294b2a -r e15f053a42d8 etc/options
--- 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"
 
diff -r 2b85a9294b2a -r e15f053a42d8 src/Pure/Syntax/syntax.ML
--- 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