From 0dddfaa74403b043a5374c5f27b5405d7d81cfdd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 May 2000 13:15:59 +0000
Subject: Achèvement nettoyage Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@421 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/edit.mli | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'lib/edit.mli')

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
-- 
cgit v1.2.3