Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified keyword categories;
authorwenzelm
Wed, 01 Jul 2015 21:48:46 +0200
changeset 60624 5b6552e12421
parent 60623 be39fe6c5620
child 60625 f64658887a05
clarified keyword categories;
src/Pure/Isar/keyword.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/keyword.scala file | annotate | diff | comparison | revisions
src/Pure/Pure.thy file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/keyword.ML	Wed Jul 01 21:29:57 2015 +0200
+++ b/src/Pure/Isar/keyword.ML	Wed Jul 01 21:48:46 2015 +0200
@@ -28,8 +28,9 @@
   val prf_decl: string
   val prf_asm: string
   val prf_asm_goal: string
-  val prf_asm_goal_script: string
   val prf_script: string
+  val prf_script_goal: string
+  val prf_script_asm_goal: string
   type spec = (string * string list) * string list
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
@@ -95,13 +96,15 @@
 val prf_decl = "prf_decl";
 val prf_asm = "prf_asm";
 val prf_asm_goal = "prf_asm_goal";
-val prf_asm_goal_script = "prf_asm_goal_script";
 val prf_script = "prf_script";
+val prf_script_goal = "prf_script_goal";
+val prf_script_asm_goal = "prf_script_asm_goal";
 
 val kinds =
   [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
     thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+    prf_script_asm_goal];
 
 
 (* specifications *)
@@ -239,19 +242,21 @@
 
 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+    prf_script_asm_goal];
 
 val is_proof_body = command_category
   [diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+    prf_script_asm_goal];
 
 val is_theory_goal = command_category [thy_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
 val is_proof_asm = command_category [prf_asm, prf_asm_goal];
-val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script];
+val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
 
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
 
--- a/src/Pure/Isar/keyword.scala	Wed Jul 01 21:29:57 2015 +0200
+++ b/src/Pure/Isar/keyword.scala	Wed Jul 01 21:48:46 2015 +0200
@@ -35,8 +35,9 @@
   val PRF_DECL = "prf_decl"
   val PRF_ASM = "prf_asm"
   val PRF_ASM_GOAL = "prf_asm_goal"
-  val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
   val PRF_SCRIPT = "prf_script"
+  val PRF_SCRIPT_GOAL = "prf_script_goal"
+  val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
 
 
   /* command categories */
@@ -63,14 +64,16 @@
 
   val proof =
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
-      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+      PRF_SCRIPT_ASM_GOAL)
 
   val proof_body =
     Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
-      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+      PRF_SCRIPT_ASM_GOAL)
 
   val theory_goal = Set(THY_GOAL)
-  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
   val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
   val qed_global = Set(QED_GLOBAL)
 
--- a/src/Pure/Pure.thy	Wed Jul 01 21:29:57 2015 +0200
+++ b/src/Pure/Pure.thy	Wed Jul 01 21:48:46 2015 +0200
@@ -57,7 +57,7 @@
   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
   and "consider" :: prf_goal % "proof"
   and "obtain" :: prf_asm_goal % "proof"
-  and "guess" :: prf_asm_goal_script % "proof"
+  and "guess" :: prf_script_asm_goal % "proof"
   and "let" "write" :: prf_decl % "proof"
   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"
@@ -69,7 +69,7 @@
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
   and "apply_end" :: prf_script % "proof" == ""
-  and "subgoal" :: prf_goal % "proof"
+  and "subgoal" :: prf_script_goal % "proof"
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"
   and "finally" "ultimately" :: prf_chain % "proof"
isabelle