more explicit indication of 'guess' as improper Isar (aka "script") element;
authorwenzelm
Mon Sep 02 16:10:26 2013 +0200 (2013-09-02 ago)
changeset 5337147b23c582127
parent 53359 ef65d5ee60cf
child 53372 f5a6313c7fe4
more explicit indication of 'guess' as improper Isar (aka "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	Mon Sep 02 11:03:02 2013 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Mon Sep 02 16:10:26 2013 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4    val prf_decl: T
     1.5    val prf_asm: T
     1.6    val prf_asm_goal: T
     1.7 +  val prf_asm_goal_script: T
     1.8    val prf_script: T
     1.9    val kinds: T list
    1.10    val tag: string -> T -> T
    1.11 @@ -115,13 +116,14 @@
    1.12  val prf_decl = kind "prf_decl";
    1.13  val prf_asm = kind "prf_asm";
    1.14  val prf_asm_goal = kind "prf_asm_goal";
    1.15 +val prf_asm_goal_script = kind "prf_asm_goal_script";
    1.16  val prf_script = kind "prf_script";
    1.17  
    1.18  val kinds =
    1.19    [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    1.20      thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
    1.21      prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    1.22 -    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.23 +    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.24  
    1.25  
    1.26  (* tags *)
    1.27 @@ -242,14 +244,14 @@
    1.28  val is_proof = command_category
    1.29    [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    1.30      prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    1.31 -    prf_asm, prf_asm_goal, prf_script];
    1.32 +    prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.33  
    1.34  val is_proof_body = command_category
    1.35 -  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
    1.36 -    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.37 +  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
    1.38 +    prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.39  
    1.40  val is_theory_goal = command_category [thy_goal];
    1.41 -val is_proof_goal = command_category [prf_goal, prf_asm_goal];
    1.42 +val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
    1.43  val is_qed = command_category [qed, qed_block];
    1.44  val is_qed_global = command_category [qed_global];
    1.45  
     2.1 --- a/src/Pure/Isar/keyword.scala	Mon Sep 02 11:03:02 2013 +0200
     2.2 +++ b/src/Pure/Isar/keyword.scala	Mon Sep 02 16:10:26 2013 +0200
     2.3 @@ -38,6 +38,7 @@
     2.4    val PRF_DECL = "prf_decl"
     2.5    val PRF_ASM = "prf_asm"
     2.6    val PRF_ASM_GOAL = "prf_asm_goal"
     2.7 +  val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
     2.8    val PRF_SCRIPT = "prf_script"
     2.9  
    2.10  
    2.11 @@ -52,11 +53,11 @@
    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,
    2.16 -      PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    2.17 +    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
    2.18 +      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    2.19    val proof1 =
    2.20      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    2.21 -  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    2.22 +  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
    2.23    val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    2.24  }
    2.25  
     3.1 --- a/src/Pure/Pure.thy	Mon Sep 02 11:03:02 2013 +0200
     3.2 +++ b/src/Pure/Pure.thy	Mon Sep 02 16:10:26 2013 +0200
     3.3 @@ -60,7 +60,8 @@
     3.4    and "then" "from" "with" :: prf_chain % "proof"
     3.5    and "note" "using" "unfolding" :: prf_decl % "proof"
     3.6    and "fix" "assume" "presume" "def" :: prf_asm % "proof"
     3.7 -  and "obtain" "guess" :: prf_asm_goal % "proof"
     3.8 +  and "obtain" :: prf_asm_goal % "proof"
     3.9 +  and "guess" :: prf_asm_goal_script % "proof"
    3.10    and "let" "write" :: prf_decl % "proof"
    3.11    and "case" :: prf_asm % "proof"
    3.12    and "{" :: prf_open % "proof"
     4.1 --- a/src/Pure/Tools/keywords.scala	Mon Sep 02 11:03:02 2013 +0200
     4.2 +++ b/src/Pure/Tools/keywords.scala	Mon Sep 02 16:10:26 2013 +0200
     4.3 @@ -38,6 +38,7 @@
     4.4      "prf_decl" -> "proof-decl",
     4.5      "prf_asm" -> "proof-asm",
     4.6      "prf_asm_goal" -> "proof-asm-goal",
     4.7 +    "prf_asm_goal_script" -> "proof-asm-goal",
     4.8      "prf_script" -> "proof-script"
     4.9    ).withDefault((s: String) => s)
    4.10  
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Sep 02 11:03:02 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Sep 02 16:10:26 2013 +0200
     5.3 @@ -77,7 +77,8 @@
     5.4        Keyword.THY_SCRIPT -> LABEL,
     5.5        Keyword.PRF_SCRIPT -> DIGIT,
     5.6        Keyword.PRF_ASM -> KEYWORD3,
     5.7 -      Keyword.PRF_ASM_GOAL -> KEYWORD3
     5.8 +      Keyword.PRF_ASM_GOAL -> KEYWORD3,
     5.9 +      Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
    5.10      ).withDefaultValue(KEYWORD1)
    5.11    }
    5.12