support for "isabelle update -u mixfix_cartouches";
authorwenzelm
Thu Jan 03 21:06:39 2019 +0100 (8 months ago)
changeset 695869171d1ce5a35
parent 69585 0484086194ce
child 69587 53982d5ec0bb
support for "isabelle update -u mixfix_cartouches";
NEWS
etc/options
src/Pure/Syntax/mixfix.ML
     1.1 --- a/NEWS	Thu Jan 03 21:04:16 2019 +0100
     1.2 +++ b/NEWS	Thu Jan 03 21:06:39 2019 +0100
     1.3 @@ -32,7 +32,9 @@
     1.4  without additional spaces, eg "(*)" instead of "( * )".
     1.5  
     1.6  * Mixfix annotations may use cartouches instead of old-style double
     1.7 -quotes, e.g. (infixl \<open>+\<close> 60).
     1.8 +quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
     1.9 +mixfix_cartouches" allows to update existing theory sources
    1.10 +automatically.
    1.11  
    1.12  * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
    1.13  need to provide a closed expression -- without trailing semicolon. Minor
     2.1 --- a/etc/options	Thu Jan 03 21:04:16 2019 +0100
     2.2 +++ b/etc/options	Thu Jan 03 21:06:39 2019 +0100
     2.3 @@ -277,6 +277,12 @@
     2.4  option export_theory : bool = false
     2.5  
     2.6  
     2.7 +section "Theory update"
     2.8 +
     2.9 +option update_mixfix_cartouches : bool = false
    2.10 +  -- "update mixfix templates to use cartouches instead of double quotes"
    2.11 +
    2.12 +
    2.13  section "Build Database"
    2.14  
    2.15  option build_database_server : bool = false
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Jan 03 21:04:16 2019 +0100
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Thu Jan 03 21:06:39 2019 +0100
     3.3 @@ -132,6 +132,23 @@
     3.4    | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT;
     3.5  
     3.6  
     3.7 +(* mixfix template *)
     3.8 +
     3.9 +fun mixfix_template (Mixfix (sy, _, _, _)) = SOME sy
    3.10 +  | mixfix_template (Infix (sy, _, _)) = SOME sy
    3.11 +  | mixfix_template (Infixl (sy, _, _)) = SOME sy
    3.12 +  | mixfix_template (Infixr (sy, _, _)) = SOME sy
    3.13 +  | mixfix_template (Binder (sy, _, _, _)) = SOME sy
    3.14 +  | mixfix_template _ = NONE;
    3.15 +
    3.16 +fun mixfix_template_reports mx =
    3.17 +  if Options.default_bool "update_mixfix_cartouches" then
    3.18 +    (case mixfix_template mx of
    3.19 +      SOME sy => [((Input.pos_of sy, Markup.update), cartouche (#1 (Input.source_content sy)))]
    3.20 +    | NONE => [])
    3.21 +  else [];
    3.22 +
    3.23 +
    3.24  (* syn_ext_types *)
    3.25  
    3.26  val typeT = Type ("type", []);
    3.27 @@ -161,6 +178,8 @@
    3.28                Position.here (pos_of mx))
    3.29        | check_args _ NONE = ();
    3.30  
    3.31 +    val _ = Position.reports_text (maps (mixfix_template_reports o #3) type_decls);
    3.32 +
    3.33      val mfix = map mfix_of type_decls;
    3.34      val _ = map2 check_args type_decls mfix;
    3.35      val consts = map (fn (t, _, _) => (t, "")) type_decls;
    3.36 @@ -206,6 +225,8 @@
    3.37      fun binder (c, _, Binder _) = SOME (binder_name c, c)
    3.38        | binder _ = NONE;
    3.39  
    3.40 +    val _ = Position.reports_text (maps (mixfix_template_reports o #3) const_decls);
    3.41 +
    3.42      val mfix = maps mfix_of const_decls;
    3.43      val binders = map_filter binder const_decls;
    3.44      val binder_trs = binders