diff options
| -rw-r--r-- | lib/edit.ml | 28 | ||||
| -rw-r--r-- | lib/edit.mli | 8 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 28 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 39 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
5 files changed, 77 insertions, 42 deletions
diff --git a/lib/edit.ml b/lib/edit.ml index ae54d71da5..8d0b0aa276 100644 --- a/lib/edit.ml +++ b/lib/edit.ml @@ -15,24 +15,32 @@ let empty () = { buf = Hashtbl.create 17 } let focus e nd = - begin match nd with - | None -> () - | Some f -> if not (Hashtbl.mem e.buf f) then invalid_arg "Edit.focus" - end; + if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus"; begin match e.focus with - | None -> if nd = None then warning "There is already no focused proof" - | Some foc -> - if e.focus <> nd then - e.last_focused_stk <- foc::(list_except foc e.last_focused_stk) + | Some foc when foc <> nd -> + e.last_focused_stk <- foc::(list_except foc e.last_focused_stk); + | _ -> () end; - e.focus <- nd + e.focus <- Some nd + +let unfocus e = + match e.focus with + | None -> invalid_arg "Edit.unfocus" + | Some foc -> + begin + e.last_focused_stk <- foc::(list_except foc e.last_focused_stk); + e.focus <- None + end let last_focused e = match e.last_focused_stk with | [] -> None | f::_ -> Some f -let restore_last_focus e = focus e (last_focused e) +let restore_last_focus e = + match e.last_focused_stk with + | [] -> () + | f::_ -> focus e f let focusedp e = match e.focus with diff --git a/lib/edit.mli b/lib/edit.mli index 6d5744259d..5926456f0a 100644 --- a/lib/edit.mli +++ b/lib/edit.mli @@ -13,9 +13,11 @@ type ('a,'b,'c) t val empty : unit -> ('a,'b,'c) t -(* sets the focus to the specified domain element, or if [None], - * unsets the focus *) -val focus : ('a,'b,'c) t -> 'a option -> unit +(* sets the focus to the specified domain element *) +val focus : ('a,'b,'c) t -> 'a -> unit + +(* unsets the focus which must not already be unfocused *) +val unfocus : ('a,'b,'c) t -> unit (* gives the last focused element or [None] if none *) val last_focused : ('a,'b,'c) t -> 'a option diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 44c4fc5fb7..7b1794c154 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -18,6 +18,11 @@ open Proof_type open Lib open Astterm +(*********************************************************************) +(* Managing the proofs state *) +(* Mainly contributed by C. Murthy *) +(*********************************************************************) + type proof_topstate = { top_hyps : env * env; top_goal : goal; @@ -84,12 +89,21 @@ let set_current_proof s = with Invalid_argument "Edit.focus" -> errorlabstrm "Pfedit.set_proof" [< 'sTR"No such proof" ; (msg_proofs false) >] + +let resume_proof = set_current_proof + +let suspend_proof () = + try + Edit.unfocus proof_edits + with Invalid_argument "Edit.unfocus" -> + errorlabstrm "Pfedit.suspend_current_proof" + [< 'sTR"No active proof" ; (msg_proofs true) >] let resume_last_proof () = match (Edit.last_focused proof_edits) with | None -> errorlabstrm "resume_last" [< 'sTR"No proof-editing in progress." >] - | p -> + | Some p -> Edit.focus proof_edits p let get_current_proof_name () = @@ -122,7 +136,7 @@ let start (na,ts) = let pfs = mk_pftreestate ts.top_goal in add_proof(na,pfs,ts) -let restart () = +let restart_proof () = match Edit.read proof_edits with | None -> errorlabstrm "Pfedit.restart" @@ -130,7 +144,7 @@ let restart () = | Some(na,_,ts) -> del_proof na; start (na,ts); - set_current_proof (Some na) + set_current_proof na let proof_term () = extract_pftreestate (get_pftreestate()) @@ -217,11 +231,11 @@ let check_no_pending_proofs () = [< 'sTR"Proof editing in progress" ; (msg_proofs false) ; 'sTR"Use \"Abort All\" first or complete proof(s)." >] -let abort_goal pn = del_proof pn +let abort_proof = del_proof -let abort_current_goal () = del_proof (get_current_proof_name ()) +let abort_current_proof () = del_proof (get_current_proof_name ()) -let abort_goals = init_proofs +let abort_all_proofs = init_proofs (*********************************************************************) (* Modifying the current prooftree *) @@ -235,7 +249,7 @@ let start_proof na str env concl = top_strength = str } in start(na,ts); - set_current_proof (Some na) + set_current_proof na (* let start_proof_constr na str concl = diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 6d5c56439a..7f9954b800 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -12,6 +12,13 @@ open Proof_type open Tacmach (*i*) +(*s Several proofs can be opened simultaneously but at most one is + focused at some time. The following functions work by side-effect + on current set of open proofs. In this module, ``proofs'' means an + open proof (something started by vernacular command [Goal], [Lemma] + or [Theorem], and ``goal'' means a subgoal of the current focused + proof *) + (* [refining ()] tells if there is some proof in progress, even if a not focused one *) @@ -22,19 +29,19 @@ val refining : unit -> bool val check_no_pending_proofs : unit -> unit -(* [abort_goal name] aborts proof of name [name] or failed if no proof +(* [abort_proof name] aborts proof of name [name] or failed if no proof has this name *) -val abort_goal : string -> unit +val abort_proof : string -> unit -(* [abort_current_goal ()] aborts current focused proof or failed if +(* [abort_current_proof ()] aborts current focused proof or failed if no proof is focused *) -val abort_current_goal : unit -> unit +val abort_current_proof : unit -> unit -(* [abort_goals ()] aborts all open proofs if any *) +(* [abort_all_proofs ()] aborts all open proofs if any *) -val abort_goals : unit -> unit +val abort_all_proofs : unit -> unit (* [undo n] undoes the effect of the last [n] tactics applied to the current proof; it fails if no proof is focused or if the ``undo'' @@ -71,25 +78,29 @@ val get_goal_context : int -> evar_declarations * env val get_current_goal_context : unit -> evar_declarations * env -(* [set_current_proof None] unfocuses the current focused proof; [set_proof -(Some name)] focuses on the proof of name [name] or raises a -[UserError] if no proof has name [name] *) +(* [resume_proof name] focuses on the proof of name [name] or + raises [UserError] if no proof has name [name] *) + +val resume_proof : string -> unit + +(* [suspend_proof ()] unfocuses the current focused proof or + failed with [UserError] if no proof is currently focused *) -val set_current_proof : string option -> unit +val suspend_proof : unit -> unit (* [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) val get_current_proof_name : unit -> string -(* [list_proofs ()] returns the list of all pending proof names *) +(* [get_all_proof_names ()] returns the list of all pending proof names *) val get_all_proof_names : unit -> string list -(* [restart ()] restarts the current focused proof from the beginning +(* [restart_proof ()] restarts the current focused proof from the beginning or fails if no proof is focused *) -val restart : unit -> unit +val restart_proof : unit -> unit (* [start_proof s str env t] starts a proof of name [s] and conclusion [t] *) @@ -130,7 +141,7 @@ val by : tactic -> unit val instantiate_nth_evar_com : int -> Coqast.t -> unit -(* To deal with focus *) +(* To deal with subgoal focus *) val make_focus : int -> unit val focus : unit -> int diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f21768913e..f90af433bb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -214,7 +214,7 @@ let _ = (* Managing states *) let abort_refine f x = - if Pfedit.refining() then abort_goals (); + if Pfedit.refining() then abort_all_proofs (); f x (* used to be: error "Must save or abort current goal first" *) @@ -353,9 +353,9 @@ let _ = | [VARG_IDENTIFIER id] -> (fun () -> let s = string_of_id id in - abort_goal s; message ("Goal "^s^" aborted")) + abort_proof s; message ("Goal "^s^" aborted")) | [] -> (fun () -> - abort_current_goal (); + abort_current_proof (); message "Current goal aborted") | _ -> bad_vernac_args "ABORT") @@ -364,7 +364,7 @@ let _ = (function | [] -> (fun () -> if refining() then begin - abort_goals (); + abort_all_proofs (); message "Current goals aborted" end else error "No proof-editing in progress") @@ -374,20 +374,20 @@ let _ = let _ = add "RESTART" (function - | [] -> (fun () -> (restart();show_open_subgoals ())) + | [] -> (fun () -> (restart_proof();show_open_subgoals ())) | _ -> bad_vernac_args "RESTART") let _ = add "SUSPEND" (function - | [] -> (fun () -> set_current_proof None) + | [] -> (fun () -> suspend_proof ()) | _ -> bad_vernac_args "SUSPEND") let _ = add "RESUME" (function | [VARG_IDENTIFIER id] -> - (fun () -> set_current_proof (Some(string_of_id id))) + (fun () -> resume_proof (string_of_id id)) | [] -> (fun () -> resume_last_proof ()) | _ -> bad_vernac_args "RESUME") @@ -719,7 +719,7 @@ let _ = mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ; 'sPC ; 'sTR"failed" ; 'sTR"... converting to Axiom" >]; - abort_goal (string_of_id s); + abort_proof (string_of_id s); parameter_def_var (string_of_id s) com end else errorlabstrm "vernacentries__TheoremProof" |