# 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