- the connections between the intermediate language and the "bag"

[helm.git] / matita / components / lexicon / cicNotation.ml

diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml
index 7351596fab41eff480a476996d7d30ea62261e4d..1934c85266986698b46b800839725da456fb4900 100644 (file)
--- a/matita/components/lexicon/cicNotation.ml
+++ b/matita/components/lexicon/cicNotation.ml
@@ -27,108 +27,47 @@
 
 open LexiconAst
 
-type notation_id =
-  | RuleId of CicNotationParser.rule_id
-  | InterpretationId of Interpretations.interpretation_id
-  | PrettyPrinterId of TermContentPres.pretty_printer_id
+class type g_status =
+ object ('self)
+  inherit Interpretations.g_status
+  inherit TermContentPres.g_status
+  inherit CicNotationParser.g_status
+ end
 
-let compare_notation_id x y = 
-  match x,y with
-  | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
-  | RuleId _, _ -> ~-1
-  | _, RuleId _ -> 1
-  | x,y -> Pervasives.compare x y
+class status =
+ object (self)
+  inherit Interpretations.status
+  inherit TermContentPres.status
+  inherit CicNotationParser.status
+  method set_notation_status
+   : 'status. #g_status as 'status -> 'self
+      = fun o -> ((self#set_interp_status o)#set_content_pres_status o)#set_notation_parser_status o
+ end
 
-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 =
+let process_notation status st =
   match st with
   | Notation (loc, dir, l1, associativity, precedence, l2) ->
       let l1 = 
         CicNotationParser.check_l1_pattern
          l1 (dir = Some `RightToLeft) precedence associativity
       in
-      let item = (l1, precedence, associativity, l2) in
-      let rule_id = ref [] in
-      let _ =
+      let status =
         if dir <> Some `RightToLeft then
-          let create_cb (l1, precedence, associativity, l2) =
-            let id =
-              CicNotationParser.extend l1 
-                (fun env loc ->
-                  CicNotationPt.AttributedTerm
-                   (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
-            rule_id := [ RuleId id ];
-            Hashtbl.add !rule_ids_to_items id item
-          in
-          RefCounter.incr ~create_cb !parser_ref_counter item
+          CicNotationParser.extend status l1 
+            (fun env loc ->
+              NotationPt.AttributedTerm
+               (`Loc loc,TermContentPres.instantiate_level2 env l2)) 
+        else status
       in
-      let pp_id =
+      let status =
         if dir <> Some `LeftToRight then
-          [ PrettyPrinterId
-              (TermContentPres.add_pretty_printer 
-                l2 l1) ]
+         let status = TermContentPres.add_pretty_printer status l2 l1 in
+          status
         else
-          []
+          status
       in
-      !rule_id @ pp_id
-  | Interpretation (loc, dsc, l2, l3) ->
-      let interp_id = Interpretations.add_interpretation dsc l2 l3 in
-       [InterpretationId interp_id]
-  | st -> []
-
-let remove_notation = function
-  | RuleId id ->
-      let item =
-        try
-          Hashtbl.find !rule_ids_to_items id
-        with Not_found -> assert false in
-      RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
-        !parser_ref_counter item
-  | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
-  | InterpretationId id -> Interpretations.remove_interpretation id
-
-let get_all_notations () =
-  List.map
-    (fun (interp_id, dsc) ->
-      InterpretationId interp_id, "interpretation: " ^ dsc)
-    (Interpretations.get_all_interpretations ())
-
-let get_active_notations () =
-  List.map (fun id -> InterpretationId id)
-    (Interpretations.get_active_interpretations ())
-
-let set_active_notations ids =
-  let interp_ids =
-    HExtlib.filter_map
-      (function InterpretationId interp_id -> Some interp_id | _ -> None)
-      ids
-  in
-  Interpretations.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 ();
- Interpretations.push ();
- CicNotationParser.push ()
-;;
+       status
+  | Interpretation (loc, dsc, l2, l3) -> 
+      Interpretations.add_interpretation status dsc l2 l3
+  | st -> status
 
-let pop () =
- TermContentPres.pop ();
- Interpretations.pop ();
- CicNotationParser.pop ();
- match !history with
- | [] -> assert false
- | (prc,riti) :: tail ->
-     parser_ref_counter := prc;
-     rule_ids_to_items := riti;
-     history := tail;
-;;