# HG changeset patch
# User wenzelm
# Date 1509900317 -3600
# Node ID 335a7dce7cb3720d19bfc35e3e014b38f67b6c8b
# Parent  671decd2e627e97a7278c434aa0d04ce303687cb
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);

diff -r 671decd2e627 -r 335a7dce7cb3 NEWS
--- a/NEWS	Sun Nov 05 16:57:03 2017 +0100
+++ b/NEWS	Sun Nov 05 17:45:17 2017 +0100
@@ -14,6 +14,9 @@
 INCOMPATIBILITY for old developments that have not been updated to
 Isabelle2017 yet (using the "isabelle imports" tool).
 
+* Theory header 'abbrevs' specifications need to be separated by 'and'.
+INCOMPATIBILITY.
+
 * Only the most fundamental theory names are global, usually the entry
 points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
 FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
diff -r 671decd2e627 -r 335a7dce7cb3 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sun Nov 05 16:57:03 2017 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun Nov 05 17:45:17 2017 +0100
@@ -66,7 +66,7 @@
     ;
     keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
     ;
-    abbrevs: @'abbrevs' ((text '=' text) +)
+    abbrevs: @'abbrevs' ((text '=' text) + @'and')
     ;
     @@{command thy_deps} (thy_bounds thy_bounds?)?
     ;
diff -r 671decd2e627 -r 335a7dce7cb3 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sun Nov 05 16:57:03 2017 +0100
+++ b/src/HOL/Library/FuncSet.thy	Sun Nov 05 17:45:17 2017 +0100
@@ -7,7 +7,7 @@
 theory FuncSet
   imports Main
   abbrevs PiE = "Pi\<^sub>E"
-    PIE = "\<Pi>\<^sub>E"
+    and PIE = "\<Pi>\<^sub>E"
 begin
 
 definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
diff -r 671decd2e627 -r 335a7dce7cb3 src/HOL/Library/Simps_Case_Conv.thy
--- a/src/HOL/Library/Simps_Case_Conv.thy	Sun Nov 05 16:57:03 2017 +0100
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Sun Nov 05 17:45:17 2017 +0100
@@ -4,11 +4,9 @@
 
 theory Simps_Case_Conv
 imports Main
-keywords
-  "simps_of_case" "case_of_simps" :: thy_decl
-abbrevs
-  "simps_of_case" = ""
-  "case_of_simps" = ""
+  keywords "simps_of_case" "case_of_simps" :: thy_decl
+  abbrevs "simps_of_case" = ""
+    and "case_of_simps" = ""
 begin
 
 ML_file "simps_case_conv.ML"
diff -r 671decd2e627 -r 335a7dce7cb3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Nov 05 16:57:03 2017 +0100
+++ b/src/Pure/Pure.thy	Sun Nov 05 17:45:17 2017 +0100
@@ -92,18 +92,17 @@
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
-abbrevs
-  "===>" = "===>"  (*prevent replacement of very long arrows*)
-  "--->" = "\<midarrow>\<rightarrow>"
-  "default_sort" = ""
-  "simproc_setup" = ""
-  "hence" = ""
-  "hence" = "then have"
-  "thus" = ""
-  "thus" = "then show"
-  "apply_end" = ""
-  "realizers" = ""
-  "realizability" = ""
+abbrevs "===>" = "===>"  (*prevent replacement of very long arrows*)
+  and "--->" = "\<midarrow>\<rightarrow>"
+  and "default_sort" = ""
+  and "simproc_setup" = ""
+  and "hence" = ""
+  and "hence" = "then have"
+  and "thus" = ""
+  and "thus" = "then show"
+  and "apply_end" = ""
+  and "realizers" = ""
+  and "realizability" = ""
 begin
 
 section \<open>Isar commands\<close>
diff -r 671decd2e627 -r 335a7dce7cb3 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sun Nov 05 16:57:03 2017 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Nov 05 17:45:17 2017 +0100
@@ -141,7 +141,7 @@
   Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
   >> (fn (names, spec) => map (rpair spec) names);
 
-val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
+val abbrevs = Parse.and_list1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
 
 val keyword_decls = Parse.and_list1 keyword_decl >> flat;
 
diff -r 671decd2e627 -r 335a7dce7cb3 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Nov 05 16:57:03 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 05 17:45:17 2017 +0100
@@ -127,7 +127,7 @@
       { case xs ~ yss => (xs :: yss).flatten }
 
     val abbrevs =
-      rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
+      rep1sep(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }, $$$("and"))
 
     val args =
       position(theory_name) ~