Achèvement nettoyage Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@421 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 23 insertions, 13 deletions

diff --git a/lib/edit.ml b/lib/edit.ml
index ae54d71da..8d0b0aa27 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 6d5744259..5926456f0 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