more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
authorwenzelm
Sun Nov 05 17:45:17 2017 +0100 (19 months ago)
changeset 67013335a7dce7cb3
parent 67012 671decd2e627
child 67014 e6a695d6a6b2
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
NEWS
src/Doc/Isar_Ref/Spec.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Simps_Case_Conv.thy
src/Pure/Pure.thy
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/NEWS	Sun Nov 05 16:57:03 2017 +0100
     1.2 +++ b/NEWS	Sun Nov 05 17:45:17 2017 +0100
     1.3 @@ -14,6 +14,9 @@
     1.4  INCOMPATIBILITY for old developments that have not been updated to
     1.5  Isabelle2017 yet (using the "isabelle imports" tool).
     1.6  
     1.7 +* Theory header 'abbrevs' specifications need to be separated by 'and'.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Only the most fundamental theory names are global, usually the entry
    1.11  points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
    1.12  FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sun Nov 05 16:57:03 2017 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sun Nov 05 17:45:17 2017 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4      ;
     2.5      keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
     2.6      ;
     2.7 -    abbrevs: @'abbrevs' ((text '=' text) +)
     2.8 +    abbrevs: @'abbrevs' ((text '=' text) + @'and')
     2.9      ;
    2.10      @@{command thy_deps} (thy_bounds thy_bounds?)?
    2.11      ;
     3.1 --- a/src/HOL/Library/FuncSet.thy	Sun Nov 05 16:57:03 2017 +0100
     3.2 +++ b/src/HOL/Library/FuncSet.thy	Sun Nov 05 17:45:17 2017 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  theory FuncSet
     3.5    imports Main
     3.6    abbrevs PiE = "Pi\<^sub>E"
     3.7 -    PIE = "\<Pi>\<^sub>E"
     3.8 +    and PIE = "\<Pi>\<^sub>E"
     3.9  begin
    3.10  
    3.11  definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
     4.1 --- a/src/HOL/Library/Simps_Case_Conv.thy	Sun Nov 05 16:57:03 2017 +0100
     4.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Sun Nov 05 17:45:17 2017 +0100
     4.3 @@ -4,11 +4,9 @@
     4.4  
     4.5  theory Simps_Case_Conv
     4.6  imports Main
     4.7 -keywords
     4.8 -  "simps_of_case" "case_of_simps" :: thy_decl
     4.9 -abbrevs
    4.10 -  "simps_of_case" = ""
    4.11 -  "case_of_simps" = ""
    4.12 +  keywords "simps_of_case" "case_of_simps" :: thy_decl
    4.13 +  abbrevs "simps_of_case" = ""
    4.14 +    and "case_of_simps" = ""
    4.15  begin
    4.16  
    4.17  ML_file "simps_case_conv.ML"
     5.1 --- a/src/Pure/Pure.thy	Sun Nov 05 16:57:03 2017 +0100
     5.2 +++ b/src/Pure/Pure.thy	Sun Nov 05 17:45:17 2017 +0100
     5.3 @@ -92,18 +92,17 @@
     5.4    and "extract_type" "extract" :: thy_decl
     5.5    and "find_theorems" "find_consts" :: diag
     5.6    and "named_theorems" :: thy_decl
     5.7 -abbrevs
     5.8 -  "===>" = "===>"  (*prevent replacement of very long arrows*)
     5.9 -  "--->" = "\<midarrow>\<rightarrow>"
    5.10 -  "default_sort" = ""
    5.11 -  "simproc_setup" = ""
    5.12 -  "hence" = ""
    5.13 -  "hence" = "then have"
    5.14 -  "thus" = ""
    5.15 -  "thus" = "then show"
    5.16 -  "apply_end" = ""
    5.17 -  "realizers" = ""
    5.18 -  "realizability" = ""
    5.19 +abbrevs "===>" = "===>"  (*prevent replacement of very long arrows*)
    5.20 +  and "--->" = "\<midarrow>\<rightarrow>"
    5.21 +  and "default_sort" = ""
    5.22 +  and "simproc_setup" = ""
    5.23 +  and "hence" = ""
    5.24 +  and "hence" = "then have"
    5.25 +  and "thus" = ""
    5.26 +  and "thus" = "then show"
    5.27 +  and "apply_end" = ""
    5.28 +  and "realizers" = ""
    5.29 +  and "realizability" = ""
    5.30  begin
    5.31  
    5.32  section \<open>Isar commands\<close>
     6.1 --- a/src/Pure/Thy/thy_header.ML	Sun Nov 05 16:57:03 2017 +0100
     6.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Nov 05 17:45:17 2017 +0100
     6.3 @@ -141,7 +141,7 @@
     6.4    Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
     6.5    >> (fn (names, spec) => map (rpair spec) names);
     6.6  
     6.7 -val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
     6.8 +val abbrevs = Parse.and_list1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
     6.9  
    6.10  val keyword_decls = Parse.and_list1 keyword_decl >> flat;
    6.11  
     7.1 --- a/src/Pure/Thy/thy_header.scala	Sun Nov 05 16:57:03 2017 +0100
     7.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Nov 05 17:45:17 2017 +0100
     7.3 @@ -127,7 +127,7 @@
     7.4        { case xs ~ yss => (xs :: yss).flatten }
     7.5  
     7.6      val abbrevs =
     7.7 -      rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
     7.8 +      rep1sep(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }, $$$("and"))
     7.9  
    7.10      val args =
    7.11        position(theory_name) ~