# HG changeset patch
# User wenzelm
# Date 1378923388 -7200
# Node ID e58ca0311c0f12834472ac078056060d4831ea08
# Parent  e12f16366957c07b780db7ee2c16764ed2978a1a
more explicit indication of 'done' as proof script element;

diff -r e12f16366957 -r e58ca0311c0f src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Pure/Isar/keyword.ML	Wed Sep 11 20:16:28 2013 +0200
@@ -23,6 +23,7 @@
   val thy_script: T
   val thy_goal: T
   val qed: T
+  val qed_script: T
   val qed_block: T
   val qed_global: T
   val prf_heading2: T
@@ -103,6 +104,7 @@
 val thy_script = kind "thy_script";
 val thy_goal = kind "thy_goal";
 val qed = kind "qed";
+val qed_script = kind "qed_script";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";
 val prf_heading2 = kind "prf_heading2";
@@ -121,7 +123,7 @@
 
 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,
+    thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, 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_asm_goal_script, prf_script];
 
@@ -242,7 +244,7 @@
     thy_load, thy_decl, thy_script, thy_goal];
 
 val is_proof = command_category
-  [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
+  [qed, qed_script, 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_asm_goal_script, prf_script];
 
@@ -252,7 +254,7 @@
 
 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_qed = command_category [qed, qed_block];
+val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
 end;
diff -r e12f16366957 -r e58ca0311c0f src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Pure/Isar/keyword.scala	Wed Sep 11 20:16:28 2013 +0200
@@ -25,6 +25,7 @@
   val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
   val QED = "qed"
+  val QED_SCRIPT = "qed_script"
   val QED_BLOCK = "qed_block"
   val QED_GLOBAL = "qed_global"
   val PRF_HEADING2 = "prf_heading2"
@@ -53,10 +54,12 @@
   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_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+    Set(QED, QED_SCRIPT, 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)
+    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
+      PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }
diff -r e12f16366957 -r e58ca0311c0f src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 11 20:16:28 2013 +0200
@@ -68,7 +68,8 @@
   and "}" :: prf_close % "proof"
   and "next" :: prf_block % "proof"
   and "qed" :: qed_block % "proof"
-  and "by" ".." "." "done" "sorry" :: "qed" % "proof"
+  and "by" ".." "." "sorry" :: "qed" % "proof"
+  and "done" :: "qed_script" % "proof"
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
   and "apply_end" :: prf_script % "proof" == ""
diff -r e12f16366957 -r e58ca0311c0f src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Pure/Tools/keywords.scala	Wed Sep 11 20:16:28 2013 +0200
@@ -27,6 +27,7 @@
     "thy_decl" -> "theory-decl",
     "thy_script" -> "theory-script",
     "thy_goal" -> "theory-goal",
+    "qed_script" -> "qed",
     "qed_block" -> "qed-block",
     "qed_global" -> "qed-global",
     "prf_heading2" -> "proof-heading",
diff -r e12f16366957 -r e58ca0311c0f src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Sep 11 20:16:28 2013 +0200
@@ -75,6 +75,7 @@
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
       Keyword.THY_SCRIPT -> LABEL,
+      Keyword.QED_SCRIPT -> DIGIT,
       Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
       Keyword.PRF_ASM_GOAL -> KEYWORD3,