added keyword category "schematic goal", which prevents any attempt to fork the proof;
authorwenzelm
Fri Apr 23 21:00:28 2010 +0200 (2010-04-23)
changeset 36315e859879079c8
parent 36314 cf1abb4daae6
child 36316 f9b45eac4c60
added keyword category "schematic goal", which prevents any attempt to fork the proof;
src/Pure/Isar/outer_keyword.ML
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/pgip_parser.ML
     1.1 --- a/src/Pure/Isar/outer_keyword.ML	Fri Apr 23 19:36:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/outer_keyword.ML	Fri Apr 23 21:00:28 2010 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val thy_decl: T
     1.5    val thy_script: T
     1.6    val thy_goal: T
     1.7 +  val thy_schematic_goal: T
     1.8    val qed: T
     1.9    val qed_block: T
    1.10    val qed_global: T
    1.11 @@ -55,6 +56,7 @@
    1.12    val is_proof: string -> bool
    1.13    val is_theory_goal: string -> bool
    1.14    val is_proof_goal: string -> bool
    1.15 +  val is_schematic_goal: string -> bool
    1.16    val is_qed: string -> bool
    1.17    val is_qed_global: string -> bool
    1.18  end;
    1.19 @@ -81,6 +83,7 @@
    1.20  val thy_decl = kind "theory-decl";
    1.21  val thy_script = kind "theory-script";
    1.22  val thy_goal = kind "theory-goal";
    1.23 +val thy_schematic_goal = kind "theory-schematic-goal";
    1.24  val qed = kind "qed";
    1.25  val qed_block = kind "qed-block";
    1.26  val qed_global = kind "qed-global";
    1.27 @@ -95,9 +98,11 @@
    1.28  val prf_asm_goal = kind "proof-asm-goal";
    1.29  val prf_script = kind "proof-script";
    1.30  
    1.31 -val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
    1.32 -  thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    1.33 -  prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
    1.34 +val kinds =
    1.35 +  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
    1.36 +    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
    1.37 +    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
    1.38 + |> map kind_of;
    1.39  
    1.40  
    1.41  (* tags *)
    1.42 @@ -191,14 +196,15 @@
    1.43  val is_theory_begin = command_category [thy_begin];
    1.44  
    1.45  val is_theory = command_category
    1.46 -  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal];
    1.47 +  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
    1.48  
    1.49  val is_proof = command_category
    1.50    [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    1.51      prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.52  
    1.53 -val is_theory_goal = command_category [thy_goal];
    1.54 +val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
    1.55  val is_proof_goal = command_category [prf_goal, prf_asm_goal];
    1.56 +val is_schematic_goal = command_category [thy_schematic_goal];
    1.57  val is_qed = command_category [qed, qed_block];
    1.58  val is_qed_global = command_category [qed_global];
    1.59  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Fri Apr 23 19:36:23 2010 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Apr 23 21:00:28 2010 +0200
     2.3 @@ -658,8 +658,11 @@
     2.4  
     2.5  fun proof_result immediate (tr, proof_trs) st =
     2.6    let val st' = command tr st in
     2.7 -    if immediate orelse null proof_trs orelse
     2.8 -      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     2.9 +    if immediate orelse
    2.10 +      null proof_trs orelse
    2.11 +      OuterKeyword.is_schematic_goal (name_of tr) orelse
    2.12 +      not (can proof_of st') orelse
    2.13 +      Proof.is_relevant (proof_of st')
    2.14      then
    2.15        let val (states, st'') = fold_map command_result proof_trs st'
    2.16        in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
     3.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Fri Apr 23 19:36:23 2010 +0200
     3.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Fri Apr 23 21:00:28 2010 +0200
     3.3 @@ -63,6 +63,7 @@
     3.4    |> command K.thy_decl         thy_decl
     3.5    |> command K.thy_script       thy_decl
     3.6    |> command K.thy_goal         goal
     3.7 +  |> command K.thy_schematic_goal goal
     3.8    |> command K.qed              closegoal
     3.9    |> command K.qed_block        closegoal
    3.10    |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])