include statement better implemented:

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 859697cd632ecf08c3b2f3d6debd5155f5e3e4eb..bb6033981a82e2a962cc9cc17d021ca2d0573349 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -226,7 +226,24 @@ let compare_rule_id x y =
     aux (x,y)
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
-let owned_keywords = Hashtbl.create 23
+let initial_owned_keywords () = Hashtbl.create 23
+
+let owned_keywords = ref (initial_owned_keywords ())
+
+let history = ref [];;
+
+let push () =
+  history := !owned_keywords :: !history;
+  owned_keywords := (initial_owned_keywords ())
+;;
+
+let pop () =
+  match !history with
+  | [] -> assert false
+  | hd :: old_history ->
+      owned_keywords := hd;
+      history := old_history
+;;
 
 type checked_l1_pattern = CL1P of CicNotationPt.term * int
 
@@ -322,13 +339,13 @@ let extend (CL1P (level1_pattern,precedence)) action =
   let keywords = CicNotationUtil.keywords_of_term level1_pattern in
   let rule_id = p_atoms in
   List.iter CicNotationLexer.add_level2_ast_keyword keywords;
-  Hashtbl.add owned_keywords rule_id keywords;  (* keywords may be [] *)
+  Hashtbl.add !owned_keywords rule_id keywords;  (* keywords may be [] *)
   rule_id
 
 let delete rule_id =
   let atoms = rule_id in
   (try
-    let keywords = Hashtbl.find owned_keywords rule_id in
+    let keywords = Hashtbl.find !owned_keywords rule_id in
     List.iter CicNotationLexer.remove_level2_ast_keyword keywords
   with Not_found -> assert false);
   Grammar.delete_rule term atoms