1.1 --- a/src/Pure/Isar/keyword.ML Mon Mar 01 16:03:06 2021 +0100
1.2 +++ b/src/Pure/Isar/keyword.ML Mon Mar 08 08:17:28 2021 +0100
1.3 @@ -241,7 +241,7 @@
1.4
1.5 (* command categories *)
1.6
1.7 -(* : Symtab.key list -> keywords -> Symtab.key -> bool*)
1.8 +(*WN : Symtab.key list -> keywords -> Symtab.key -> bool*)
1.9 fun command_category ks =
1.10 let
1.11 val tab = Symtab.make_set ks;
2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Mar 01 16:03:06 2021 +0100
2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Mar 08 08:17:28 2021 +0100
2.3 @@ -15,9 +15,11 @@
2.4 and "Problem" :: thy_decl (* root-problem + recursively in Solution;
2.5 "spark_vc" :: thy_goal *)
2.6 and "Specification" "Model" "References" :: diag
2.7 + (*TRIED: diag quasi_command qed_script thy_decl thy_defn thy_goal thy_goal_stmt thy_stmt vvv *)
2.8 and "Solution" :: thy_decl (* structure only *)
2.9 and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term, cp.from "from".."have" *)
2.10 - (* ^^^^^^ :: before_command quasi_command thy_decl thy_defn thy_stmt diag prf_decl *)
2.11 + (* ^^^^^^ :: .. see Pure/Isar/keyword.ML (* command categories *) TRIED COMBINATIONS WITH ^^^:
2.12 + before_command quasi_command thy_decl thy_defn thy_stmt diag prf_decl *)
2.13 (*and "Where" (* only output, preliminarily *)*)
2.14 and "RTheory" :: thy_decl (* await input of string; "R" distingues "Problem".."RProblem" *)
2.15 and "RProblem" "RMethod" :: thy_decl (* await input of string list *)
2.16 @@ -247,6 +249,45 @@
2.17 with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
2.18 *)
2.19
2.20 +subsection \<open>try combinations of keyword types\<close>
2.21 +subsubsection \<open>"Where" "Given" "Find" "Relate" :: prf_decl\<close>
2.22 +text \<open>
2.23 +keywords
2.24 + and "Specification" "Model" "References" :: XXX
2.25 + and "Where" "Given" "Find" "Relate" :: prf_decl
2.26 +CAUSE THESE ERRORS (EXHAUSTIVE ENUMERATION):
2.27 +
2.28 +XXX = diag, thy_stmt
2.29 + Bad context for command "Given" -- using reset state
2.30 + Bad context for command "RTheory" -- using reset state
2.31 +XXX = thy_decl, thy_defn, thy_goal, thy_goal_stmt
2.32 + Bad context for command "Given" -- using reset state
2.33 + Bad context for command "References" -- using reset state
2.34 +XXX = qed_script
2.35 + Bad context for command "Specification" -- using reset state
2.36 + Bad context for command "Model" -- using reset state
2.37 + Bad context for command "Given" -- using reset state
2.38 +XXX = quasi_command: SCAN NOT DELIMITED PROPERLY..
2.39 + Outer syntax error: command expected, but keyword Specification was found
2.40 +XXX = thy_goal_stmt
2.41 +\<close>
2.42 +subsubsection \<open>"Where" "Given" "Find" "Relate" :: prf_decl\<close>
2.43 +text \<open>
2.44 +keywords
2.45 + and "Specification" "Model" "References" :: thy_stmt
2.46 + and "Where" "Given" "Find" "Relate" :: XXX
2.47 +CAUSE THESE ERRORS (EXHAUSTIVE ENUMERATION):
2.48 +
2.49 +XXX = prf_decl ((Where, Find, Relate ARE SCANNED PROPERLY))
2.50 + Bad context for command "Given" -- using reset state
2.51 + Bad context for command "References" -- using reset state
2.52 +XXX = thy_stmt ((Where, Find, Relate ARE SCANNED PROPERLY))
2.53 + Bad context for command "Given"
2.54 + Bad context for command "Where"
2.55 + Bad context for command "Find"
2.56 + Bad context for command "Relate"
2.57 +\<close>
2.58 +
2.59 subsection \<open><Output> BY CLICK ON Problem..Given: Position, command-range?\<close>
2.60 subsubsection \<open>on Problem\<close>
2.61 text \<open>