# HG changeset patch
# User wenzelm
# Date 1272049228 -7200
# Node ID e859879079c817af50d9c122cfc1f6c1bf0dac62
# Parent  cf1abb4daae65dcd2c3c44d45a257f7ecc1b7691
added keyword category "schematic goal", which prevents any attempt to fork the proof;

diff -r cf1abb4daae6 -r e859879079c8 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Fri Apr 23 19:36:23 2010 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Fri Apr 23 21:00:28 2010 +0200
@@ -17,6 +17,7 @@
   val thy_decl: T
   val thy_script: T
   val thy_goal: T
+  val thy_schematic_goal: T
   val qed: T
   val qed_block: T
   val qed_global: T
@@ -55,6 +56,7 @@
   val is_proof: string -> bool
   val is_theory_goal: string -> bool
   val is_proof_goal: string -> bool
+  val is_schematic_goal: string -> bool
   val is_qed: string -> bool
   val is_qed_global: string -> bool
 end;
@@ -81,6 +83,7 @@
 val thy_decl = kind "theory-decl";
 val thy_script = kind "theory-script";
 val thy_goal = kind "theory-goal";
+val thy_schematic_goal = kind "theory-schematic-goal";
 val qed = kind "qed";
 val qed_block = kind "qed-block";
 val qed_global = kind "qed-global";
@@ -95,9 +98,11 @@
 val prf_asm_goal = kind "proof-asm-goal";
 val prf_script = kind "proof-script";
 
-val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
-  thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
-  prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
+val kinds =
+  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
+    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
+ |> map kind_of;
 
 
 (* tags *)
@@ -191,14 +196,15 @@
 val is_theory_begin = command_category [thy_begin];
 
 val is_theory = command_category
-  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal];
+  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
 
 val is_proof = command_category
   [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
     prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 
-val is_theory_goal = command_category [thy_goal];
+val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
+val is_schematic_goal = command_category [thy_schematic_goal];
 val is_qed = command_category [qed, qed_block];
 val is_qed_global = command_category [qed_global];
 
diff -r cf1abb4daae6 -r e859879079c8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Apr 23 19:36:23 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Apr 23 21:00:28 2010 +0200
@@ -658,8 +658,11 @@
 
 fun proof_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
-    if immediate orelse null proof_trs orelse
-      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
+    if immediate orelse
+      null proof_trs orelse
+      OuterKeyword.is_schematic_goal (name_of tr) orelse
+      not (can proof_of st') orelse
+      Proof.is_relevant (proof_of st')
     then
       let val (states, st'') = fold_map command_result proof_trs st'
       in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
diff -r cf1abb4daae6 -r e859879079c8 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Fri Apr 23 19:36:23 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Fri Apr 23 21:00:28 2010 +0200
@@ -63,6 +63,7 @@
   |> command K.thy_decl         thy_decl
   |> command K.thy_script       thy_decl
   |> command K.thy_goal         goal
+  |> command K.thy_schematic_goal goal
   |> command K.qed              closegoal
   |> command K.qed_block        closegoal
   |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])