more explicit indication of 'done' as proof script element;
authorwenzelm
Wed Sep 11 20:16:28 2013 +0200 (2013-09-11 ago)
changeset 53571e58ca0311c0f
parent 53547 e12f16366957
child 53572 e7b77b217491
more explicit indication of 'done' as proof script element;
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Pure.thy
src/Pure/Tools/keywords.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/Isar/keyword.ML	Wed Sep 11 18:52:30 2013 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Wed Sep 11 20:16:28 2013 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val thy_script: T
     1.5    val thy_goal: T
     1.6    val qed: T
     1.7 +  val qed_script: T
     1.8    val qed_block: T
     1.9    val qed_global: T
    1.10    val prf_heading2: T
    1.11 @@ -103,6 +104,7 @@
    1.12  val thy_script = kind "thy_script";
    1.13  val thy_goal = kind "thy_goal";
    1.14  val qed = kind "qed";
    1.15 +val qed_script = kind "qed_script";
    1.16  val qed_block = kind "qed_block";
    1.17  val qed_global = kind "qed_global";
    1.18  val prf_heading2 = kind "prf_heading2";
    1.19 @@ -121,7 +123,7 @@
    1.20  
    1.21  val kinds =
    1.22    [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    1.23 -    thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
    1.24 +    thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
    1.25      prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    1.26      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.27  
    1.28 @@ -242,7 +244,7 @@
    1.29      thy_load, thy_decl, thy_script, thy_goal];
    1.30  
    1.31  val is_proof = command_category
    1.32 -  [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    1.33 +  [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    1.34      prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    1.35      prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.36  
    1.37 @@ -252,7 +254,7 @@
    1.38  
    1.39  val is_theory_goal = command_category [thy_goal];
    1.40  val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
    1.41 -val is_qed = command_category [qed, qed_block];
    1.42 +val is_qed = command_category [qed, qed_script, qed_block];
    1.43  val is_qed_global = command_category [qed_global];
    1.44  
    1.45  end;
     2.1 --- a/src/Pure/Isar/keyword.scala	Wed Sep 11 18:52:30 2013 +0200
     2.2 +++ b/src/Pure/Isar/keyword.scala	Wed Sep 11 20:16:28 2013 +0200
     2.3 @@ -25,6 +25,7 @@
     2.4    val THY_SCRIPT = "thy_script"
     2.5    val THY_GOAL = "thy_goal"
     2.6    val QED = "qed"
     2.7 +  val QED_SCRIPT = "qed_script"
     2.8    val QED_BLOCK = "qed_block"
     2.9    val QED_GLOBAL = "qed_global"
    2.10    val PRF_HEADING2 = "prf_heading2"
    2.11 @@ -53,10 +54,12 @@
    2.12    val theory1 = Set(THY_BEGIN, THY_END)
    2.13    val theory2 = Set(THY_DECL, THY_GOAL)
    2.14    val proof =
    2.15 -    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
    2.16 -      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    2.17 +    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
    2.18 +      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
    2.19 +      PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    2.20    val proof1 =
    2.21 -    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    2.22 +    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
    2.23 +      PRF_CHAIN, PRF_DECL)
    2.24    val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
    2.25    val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    2.26  }
     3.1 --- a/src/Pure/Pure.thy	Wed Sep 11 18:52:30 2013 +0200
     3.2 +++ b/src/Pure/Pure.thy	Wed Sep 11 20:16:28 2013 +0200
     3.3 @@ -68,7 +68,8 @@
     3.4    and "}" :: prf_close % "proof"
     3.5    and "next" :: prf_block % "proof"
     3.6    and "qed" :: qed_block % "proof"
     3.7 -  and "by" ".." "." "done" "sorry" :: "qed" % "proof"
     3.8 +  and "by" ".." "." "sorry" :: "qed" % "proof"
     3.9 +  and "done" :: "qed_script" % "proof"
    3.10    and "oops" :: qed_global % "proof"
    3.11    and "defer" "prefer" "apply" :: prf_script % "proof"
    3.12    and "apply_end" :: prf_script % "proof" == ""
     4.1 --- a/src/Pure/Tools/keywords.scala	Wed Sep 11 18:52:30 2013 +0200
     4.2 +++ b/src/Pure/Tools/keywords.scala	Wed Sep 11 20:16:28 2013 +0200
     4.3 @@ -27,6 +27,7 @@
     4.4      "thy_decl" -> "theory-decl",
     4.5      "thy_script" -> "theory-script",
     4.6      "thy_goal" -> "theory-goal",
     4.7 +    "qed_script" -> "qed",
     4.8      "qed_block" -> "qed-block",
     4.9      "qed_global" -> "qed-global",
    4.10      "prf_heading2" -> "proof-heading",
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Sep 11 18:52:30 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Sep 11 20:16:28 2013 +0200
     5.3 @@ -75,6 +75,7 @@
     5.4      Map[String, Byte](
     5.5        Keyword.THY_END -> KEYWORD2,
     5.6        Keyword.THY_SCRIPT -> LABEL,
     5.7 +      Keyword.QED_SCRIPT -> DIGIT,
     5.8        Keyword.PRF_SCRIPT -> DIGIT,
     5.9        Keyword.PRF_ASM -> KEYWORD3,
    5.10        Keyword.PRF_ASM_GOAL -> KEYWORD3,