# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1615187848 -3600
# Node ID 002e3ecd310866d845efffc30cd1d9fb32520818
# Parent  50f655f2db4f13846adf361abd51e0e6f3bcf420
step 6.10: stop unsuccessful trials with combination of types on Outer_Syntax

note: test in Calculation.thy is outcommented

diff -r 50f655f2db4f -r 002e3ecd3108 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Mar 01 16:03:06 2021 +0100
+++ b/src/Pure/Isar/keyword.ML	Mon Mar 08 08:17:28 2021 +0100
@@ -241,7 +241,7 @@
 
 (* command categories *)
 
-(*                  : Symtab.key list -> keywords -> Symtab.key -> bool*)
+(*WN                : Symtab.key list -> keywords -> Symtab.key -> bool*)
 fun command_category ks =
   let
     val tab = Symtab.make_set ks;
diff -r 50f655f2db4f -r 002e3ecd3108 src/Tools/isac/BridgeJEdit/Calculation.thy
--- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Mon Mar 01 16:03:06 2021 +0100
+++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Mon Mar 08 08:17:28 2021 +0100
@@ -15,9 +15,11 @@
   and "Problem" :: thy_decl (* root-problem + recursively in Solution;
                                "spark_vc" :: thy_goal *)
   and "Specification" "Model" "References" :: diag
+    (*TRIED: diag quasi_command qed_script thy_decl thy_defn thy_goal thy_goal_stmt thy_stmt vvv *)
   and "Solution" :: thy_decl (* structure only *)
   and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term, cp.from "from".."have" *)
-   (* ^^^^^^ :: before_command quasi_command thy_decl thy_defn thy_stmt diag prf_decl *)
+   (* ^^^^^^ :: .. see Pure/Isar/keyword.ML (* command categories *) TRIED COMBINATIONS WITH ^^^:
+      before_command quasi_command thy_decl thy_defn thy_stmt diag prf_decl *)
 (*and "Where" (* only output, preliminarily *)*)
   and "RTheory" :: thy_decl (* await input of string; "R" distingues "Problem".."RProblem" *)
   and "RProblem" "RMethod" :: thy_decl (* await input of string list *)
@@ -247,6 +249,45 @@
   with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
 *)
 
+subsection \<open>try combinations of keyword types\<close>
+subsubsection \<open>"Where" "Given" "Find" "Relate" :: prf_decl\<close>
+text \<open>
+keywords
+  and "Specification" "Model" "References" :: XXX
+  and "Where" "Given" "Find" "Relate" :: prf_decl
+CAUSE THESE ERRORS (EXHAUSTIVE ENUMERATION):
+
+XXX = diag, thy_stmt
+  Bad context for command "Given" -- using reset state
+  Bad context for command "RTheory" -- using reset state
+XXX = thy_decl, thy_defn, thy_goal, thy_goal_stmt
+  Bad context for command "Given" -- using reset state
+  Bad context for command "References" -- using reset state
+XXX = qed_script
+  Bad context for command "Specification" -- using reset state
+  Bad context for command "Model" -- using reset state
+  Bad context for command "Given" -- using reset state
+XXX = quasi_command: SCAN NOT DELIMITED PROPERLY..
+  Outer syntax error: command expected, but keyword Specification was found
+XXX = thy_goal_stmt
+\<close>
+subsubsection \<open>"Where" "Given" "Find" "Relate" :: prf_decl\<close>
+text \<open>
+keywords
+  and "Specification" "Model" "References" :: thy_stmt
+  and "Where" "Given" "Find" "Relate" :: XXX
+CAUSE THESE ERRORS (EXHAUSTIVE ENUMERATION):
+
+XXX = prf_decl ((Where, Find, Relate ARE SCANNED PROPERLY))
+  Bad context for command "Given" -- using reset state
+  Bad context for command "References" -- using reset state
+XXX = thy_stmt ((Where, Find, Relate ARE SCANNED PROPERLY))
+  Bad context for command "Given"
+  Bad context for command "Where"
+  Bad context for command "Find"
+  Bad context for command "Relate"
+\<close>
+
 subsection \<open><Output> BY CLICK ON Problem..Given: Position, command-range?\<close>
 subsubsection \<open>on Problem\<close>
 text \<open>