X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FcicNotation.ml;h=29c4f0e5d79547c562a1c6cefe196b669cd9ed25;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=32cb3f6382cf327b89d01476312d1d7c953f0a6b;hpb=eb9ca860db8cb06083765f7698179f16dee5303e;p=helm.git

diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml
index 32cb3f638..29c4f0e5d 100644
--- a/helm/software/components/lexicon/cicNotation.ml
+++ b/helm/software/components/lexicon/cicNotation.ml
@@ -39,14 +39,18 @@ let compare_notation_id x y =
   | _, RuleId _ -> 1
   | x,y -> Pervasives.compare x y
 
-let parser_ref_counter = RefCounter.create ()
-let rule_ids_to_items = Hashtbl.create 113
+let initial_parser_ref_counter () = RefCounter.create ()
+let initial_rule_ids_to_items ()= Hashtbl.create 113
+
+let parser_ref_counter = ref (initial_parser_ref_counter ());;
+let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
 
 let process_notation st =
   match st with
   | Notation (loc, dir, l1, associativity, precedence, l2) ->
       let l1 = 
-        CicNotationParser.check_l1_pattern l1 precedence associativity
+        CicNotationParser.check_l1_pattern
+         l1 (dir = Some `RightToLeft) precedence associativity
       in
       let item = (l1, precedence, associativity, l2) in
       let rule_id = ref [] in
@@ -59,9 +63,9 @@ let process_notation st =
                   CicNotationPt.AttributedTerm
                    (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
             rule_id := [ RuleId id ];
-            Hashtbl.add rule_ids_to_items id item
+            Hashtbl.add !rule_ids_to_items id item
           in
-          RefCounter.incr ~create_cb parser_ref_counter item
+          RefCounter.incr ~create_cb !parser_ref_counter item
       in
       let pp_id =
         if dir <> Some `LeftToRight then
@@ -77,16 +81,24 @@ let process_notation st =
        [InterpretationId interp_id]
   | st -> []
 
+(* CSC: Matita compiled with recent OCaml triggers the assert false in the
+   code below. The exception FOO trick ignores the failure. It seems to
+   work, but it's the classical patch without understanding what the problem
+   is. *)
+exception FOO;;
+
 let remove_notation = function
+xxx -> try match xxx with
   | RuleId id ->
       let item =
         try
-          Hashtbl.find rule_ids_to_items id
-        with Not_found -> assert false in
+          Hashtbl.find !rule_ids_to_items id
+        with Not_found -> raise FOO (*assert false*) in
       RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
-        parser_ref_counter item
+        !parser_ref_counter item
   | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
   | InterpretationId id -> TermAcicContent.remove_interpretation id
+with FOO -> ();;
 
 let get_all_notations () =
   List.map
@@ -106,7 +118,12 @@ let set_active_notations ids =
   in
   TermAcicContent.set_active_interpretations interp_ids
 
+let history = ref [];;
+
 let push () =
+ history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
+ parser_ref_counter := initial_parser_ref_counter ();
+ rule_ids_to_items := initial_rule_ids_to_items ();
  TermContentPres.push ();
  TermAcicContent.push ();
  CicNotationParser.push ()
@@ -115,5 +132,11 @@ let push () =
 let pop () =
  TermContentPres.pop ();
  TermAcicContent.pop ();
- CicNotationParser.pop ()
+ CicNotationParser.pop ();
+ match !history with
+ | [] -> assert false
+ | (prc,riti) :: tail ->
+     parser_ref_counter := prc;
+     rule_ids_to_items := riti;
+     history := tail;
 ;;