Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dans

un plugin.


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

2 files changed, 23 insertions, 0 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c827ab381a..7a1421592c 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -59,6 +59,25 @@ let ttree_find ttree str =
   in 
   proc_rec ttree 0
 
+(* Removes a string from a dictionary: returns an equal dictionary
+   if the word not present. *)
+let ttree_remove ttree str =
+  let rec remove tt i =
+    if i == String.length str then 
+      {node = None; branch = tt.branch}
+    else
+      let c = str.[i] in
+      let br =
+        match try Some (CharMap.find c tt.branch) with Not_found -> None with
+          | Some tt' ->
+              CharMap.add c (remove tt' (i + 1)) (CharMap.remove c tt.branch)
+          | None -> tt.branch
+      in
+      { node = tt.node; branch = br }
+  in 
+  remove ttree 0
+
+
 (* Errors occuring while lexing (explained as "Lexer error: ...") *)
 
 type error =
@@ -171,6 +190,9 @@ let add_keyword str =
   check_keyword str;
   token_tree := ttree_add !token_tree str
 
+let remove_keyword str = 
+  token_tree := ttree_remove !token_tree str
+
 (* Adding a new token (keyword or special token). *)
 let add_token (con, str) = match con with
   | "" -> add_keyword str
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 1a3a10aaae..1b40d7f178 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -21,6 +21,7 @@ type error =
 exception Error of error
 
 val add_token : string * string -> unit
+val remove_keyword : string -> unit
 val is_keyword : string -> bool
 
 val location_function : int -> loc