# HG changeset patch
# User wenzelm
# Date 1378131026 -7200
# Node ID 47b23c58212771da82135ed24d7517a40e87d120
# Parent  ef65d5ee60cfd365d298ac2d5a96066d976354ef
more explicit indication of 'guess' as improper Isar (aka "script") element;

diff -r ef65d5ee60cf -r 47b23c582127 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon Sep 02 16:10:26 2013 +0200
@@ -36,6 +36,7 @@
   val prf_decl: T
   val prf_asm: T
   val prf_asm_goal: T
+  val prf_asm_goal_script: T
   val prf_script: T
   val kinds: T list
   val tag: string -> T -> T
@@ -115,13 +116,14 @@
 val prf_decl = kind "prf_decl";
 val prf_asm = kind "prf_asm";
 val prf_asm_goal = kind "prf_asm_goal";
+val prf_asm_goal_script = kind "prf_asm_goal_script";
 val prf_script = kind "prf_script";
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
     prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 
 (* tags *)
@@ -242,14 +244,14 @@
 val is_proof = command_category
   [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
     prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
-    prf_asm, prf_asm_goal, prf_script];
+    prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_proof_body = command_category
-  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
+    prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_theory_goal = command_category [thy_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
 val is_qed = command_category [qed, qed_block];
 val is_qed_global = command_category [qed_global];
 
diff -r ef65d5ee60cf -r 47b23c582127 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Pure/Isar/keyword.scala	Mon Sep 02 16:10:26 2013 +0200
@@ -38,6 +38,7 @@
   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"
 
 
@@ -52,11 +53,11 @@
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
-    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL,
-      PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
+    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
+      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   val proof1 =
     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
-  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
+  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }
 
diff -r ef65d5ee60cf -r 47b23c582127 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Pure/Pure.thy	Mon Sep 02 16:10:26 2013 +0200
@@ -60,7 +60,8 @@
   and "then" "from" "with" :: prf_chain % "proof"
   and "note" "using" "unfolding" :: prf_decl % "proof"
   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
-  and "obtain" "guess" :: prf_asm_goal % "proof"
+  and "obtain" :: prf_asm_goal % "proof"
+  and "guess" :: prf_asm_goal_script % "proof"
   and "let" "write" :: prf_decl % "proof"
   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"
diff -r ef65d5ee60cf -r 47b23c582127 src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Pure/Tools/keywords.scala	Mon Sep 02 16:10:26 2013 +0200
@@ -38,6 +38,7 @@
     "prf_decl" -> "proof-decl",
     "prf_asm" -> "proof-asm",
     "prf_asm_goal" -> "proof-asm-goal",
+    "prf_asm_goal_script" -> "proof-asm-goal",
     "prf_script" -> "proof-script"
   ).withDefault((s: String) => s)
 
diff -r ef65d5ee60cf -r 47b23c582127 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Sep 02 16:10:26 2013 +0200
@@ -77,7 +77,8 @@
       Keyword.THY_SCRIPT -> LABEL,
       Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
-      Keyword.PRF_ASM_GOAL -> KEYWORD3
+      Keyword.PRF_ASM_GOAL -> KEYWORD3,
+      Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
     ).withDefaultValue(KEYWORD1)
   }