# HG changeset patch
# User wenzelm
# Date 1546545999 -3600
# Node ID 9171d1ce5a355615d3d32124b4f066d6b3f24fab
# Parent  0484086194ce8fa64d2c7ffab45380e5e3d83f5d
support for "isabelle update -u mixfix_cartouches";

diff -r 0484086194ce -r 9171d1ce5a35 NEWS
--- a/NEWS	Thu Jan 03 21:04:16 2019 +0100
+++ b/NEWS	Thu Jan 03 21:06:39 2019 +0100
@@ -32,7 +32,9 @@
 without additional spaces, eg "(*)" instead of "( * )".
 
 * Mixfix annotations may use cartouches instead of old-style double
-quotes, e.g. (infixl \<open>+\<close> 60).
+quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
+mixfix_cartouches" allows to update existing theory sources
+automatically.
 
 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
 need to provide a closed expression -- without trailing semicolon. Minor
diff -r 0484086194ce -r 9171d1ce5a35 etc/options
--- a/etc/options	Thu Jan 03 21:04:16 2019 +0100
+++ b/etc/options	Thu Jan 03 21:06:39 2019 +0100
@@ -277,6 +277,12 @@
 option export_theory : bool = false
 
 
+section "Theory update"
+
+option update_mixfix_cartouches : bool = false
+  -- "update mixfix templates to use cartouches instead of double quotes"
+
+
 section "Build Database"
 
 option build_database_server : bool = false
diff -r 0484086194ce -r 9171d1ce5a35 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Thu Jan 03 21:04:16 2019 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Thu Jan 03 21:06:39 2019 +0100
@@ -132,6 +132,23 @@
   | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT;
 
 
+(* mixfix template *)
+
+fun mixfix_template (Mixfix (sy, _, _, _)) = SOME sy
+  | mixfix_template (Infix (sy, _, _)) = SOME sy
+  | mixfix_template (Infixl (sy, _, _)) = SOME sy
+  | mixfix_template (Infixr (sy, _, _)) = SOME sy
+  | mixfix_template (Binder (sy, _, _, _)) = SOME sy
+  | mixfix_template _ = NONE;
+
+fun mixfix_template_reports mx =
+  if Options.default_bool "update_mixfix_cartouches" then
+    (case mixfix_template mx of
+      SOME sy => [((Input.pos_of sy, Markup.update), cartouche (#1 (Input.source_content sy)))]
+    | NONE => [])
+  else [];
+
+
 (* syn_ext_types *)
 
 val typeT = Type ("type", []);
@@ -161,6 +178,8 @@
               Position.here (pos_of mx))
       | check_args _ NONE = ();
 
+    val _ = Position.reports_text (maps (mixfix_template_reports o #3) type_decls);
+
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
     val consts = map (fn (t, _, _) => (t, "")) type_decls;
@@ -206,6 +225,8 @@
     fun binder (c, _, Binder _) = SOME (binder_name c, c)
       | binder _ = NONE;
 
+    val _ = Position.reports_text (maps (mixfix_template_reports o #3) const_decls);
+
     val mfix = maps mfix_of const_decls;
     val binders = map_filter binder const_decls;
     val binder_trs = binders