discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
authorwenzelm
Mon Feb 25 13:29:19 2013 +0100 (2013-02-25 ago)
changeset 51274cfc83ad52571
parent 51273 d54ee0cad2ab
child 51275 3928173409e4
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
lib/scripts/keywords
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/Pure.thy
     1.1 --- a/lib/scripts/keywords	Mon Feb 25 12:52:27 2013 +0100
     1.2 +++ b/lib/scripts/keywords	Mon Feb 25 13:29:19 2013 +0100
     1.3 @@ -41,7 +41,6 @@
     1.4    "thy_decl" => "theory-decl",
     1.5    "thy_script" => "theory-script",
     1.6    "thy_goal" => "theory-goal",
     1.7 -  "thy_schematic_goal" => "theory-goal",
     1.8    "qed_block" => "qed-block",
     1.9    "qed_global" => "qed-global",
    1.10    "prf_heading2" => "proof-heading",
     2.1 --- a/src/Pure/Isar/keyword.ML	Mon Feb 25 12:52:27 2013 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Mon Feb 25 13:29:19 2013 +0100
     2.3 @@ -22,7 +22,6 @@
     2.4    val thy_load_files: string list -> T
     2.5    val thy_script: T
     2.6    val thy_goal: T
     2.7 -  val thy_schematic_goal: T
     2.8    val qed: T
     2.9    val qed_block: T
    2.10    val qed_global: T
    2.11 @@ -66,7 +65,6 @@
    2.12    val is_proof_body: string -> bool
    2.13    val is_theory_goal: string -> bool
    2.14    val is_proof_goal: string -> bool
    2.15 -  val is_schematic_goal: string -> bool
    2.16    val is_qed: string -> bool
    2.17    val is_qed_global: string -> bool
    2.18  end;
    2.19 @@ -104,7 +102,6 @@
    2.20  fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
    2.21  val thy_script = kind "thy_script";
    2.22  val thy_goal = kind "thy_goal";
    2.23 -val thy_schematic_goal = kind "thy_schematic_goal";
    2.24  val qed = kind "qed";
    2.25  val qed_block = kind "qed_block";
    2.26  val qed_global = kind "qed_global";
    2.27 @@ -123,7 +120,7 @@
    2.28  
    2.29  val kinds =
    2.30    [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    2.31 -    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
    2.32 +    thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
    2.33      prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    2.34      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    2.35  
    2.36 @@ -253,7 +250,7 @@
    2.37  
    2.38  val is_theory = command_category
    2.39    [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    2.40 -    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal];
    2.41 +    thy_load, thy_decl, thy_script, thy_goal];
    2.42  
    2.43  val is_proof = command_category
    2.44    [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    2.45 @@ -264,9 +261,8 @@
    2.46    [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
    2.47      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    2.48  
    2.49 -val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
    2.50 +val is_theory_goal = command_category [thy_goal];
    2.51  val is_proof_goal = command_category [prf_goal, prf_asm_goal];
    2.52 -val is_schematic_goal = command_category [thy_schematic_goal];
    2.53  val is_qed = command_category [qed, qed_block];
    2.54  val is_qed_global = command_category [qed_global];
    2.55  
     3.1 --- a/src/Pure/Isar/keyword.scala	Mon Feb 25 12:52:27 2013 +0100
     3.2 +++ b/src/Pure/Isar/keyword.scala	Mon Feb 25 13:29:19 2013 +0100
     3.3 @@ -24,7 +24,6 @@
     3.4    val THY_LOAD = "thy_load"
     3.5    val THY_SCRIPT = "thy_script"
     3.6    val THY_GOAL = "thy_goal"
     3.7 -  val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
     3.8    val QED = "qed"
     3.9    val QED_BLOCK = "qed_block"
    3.10    val QED_GLOBAL = "qed_global"
    3.11 @@ -49,7 +48,7 @@
    3.12    val diag = Set(DIAG)
    3.13    val theory =
    3.14      Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
    3.15 -      THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    3.16 +      THY_DECL, THY_SCRIPT, THY_GOAL)
    3.17    val theory1 = Set(THY_BEGIN, THY_END)
    3.18    val theory2 = Set(THY_DECL, THY_GOAL)
    3.19    val proof =
     4.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 13:29:19 2013 +0100
     4.3 @@ -720,8 +720,7 @@
     4.4      val st' = command head_tr st;
     4.5    in
     4.6      if not future_enabled orelse is_ignored head_tr orelse
     4.7 -      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
     4.8 -      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     4.9 +      null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    4.10      then
    4.11        let val (results, st'') = fold_map atom_result proof_trs st'
    4.12        in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
     5.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Mon Feb 25 12:52:27 2013 +0100
     5.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Mon Feb 25 13:29:19 2013 +0100
     5.3 @@ -65,7 +65,6 @@
     5.4    |> command Keyword.thy_decl         thy_decl
     5.5    |> command Keyword.thy_script       thy_decl
     5.6    |> command Keyword.thy_goal         goal
     5.7 -  |> command Keyword.thy_schematic_goal goal
     5.8    |> command Keyword.qed              closegoal
     5.9    |> command Keyword.qed_block        closegoal
    5.10    |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
     6.1 --- a/src/Pure/Pure.thy	Mon Feb 25 12:52:27 2013 +0100
     6.2 +++ b/src/Pure/Pure.thy	Mon Feb 25 13:29:19 2013 +0100
     6.3 @@ -50,7 +50,7 @@
     6.4    and "overloading" :: thy_decl
     6.5    and "code_datatype" :: thy_decl
     6.6    and "theorem" "lemma" "corollary" :: thy_goal
     6.7 -  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
     6.8 +  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
     6.9    and "notepad" :: thy_decl
    6.10    and "have" :: prf_goal % "proof"
    6.11    and "hence" :: prf_goal % "proof" == "then have"