More parts of the lexicon status made functional.

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

diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml
index 7351596fab41eff480a476996d7d30ea62261e4d..93d8a5570fa1d30dc0b7fd0f8f36e680d77fb2d8 100644 (file)
--- a/matita/components/lexicon/cicNotation.ml
+++ b/matita/components/lexicon/cicNotation.ml
@@ -32,6 +32,21 @@ type notation_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
+ end
+
+class status =
+ object (self)
+  inherit Interpretations.status
+  inherit TermContentPres.status
+  method set_notation_status
+   : 'status. #g_status as 'status -> 'self
+      = fun o -> (self#set_interp_status o)#set_content_pres_status o
+ end
+
 let compare_notation_id x y = 
   match x,y with
   | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
@@ -45,7 +60,7 @@ 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 = 
@@ -60,26 +75,27 @@ let process_notation st =
             let id =
               CicNotationParser.extend l1 
                 (fun env loc ->
-                  CicNotationPt.AttributedTerm
+                  NotationPt.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
       in
-      let pp_id =
+      let status,pp_id =
         if dir <> Some `LeftToRight then
-          [ PrettyPrinterId
-              (TermContentPres.add_pretty_printer 
-                l2 l1) ]
+         let status,id = TermContentPres.add_pretty_printer status l2 l1 in
+          status,[ PrettyPrinterId id ]
         else
-          []
+          status,[]
       in
-      !rule_id @ pp_id
+       status,!rule_id @ pp_id
   | Interpretation (loc, dsc, l2, l3) ->
-      let interp_id = Interpretations.add_interpretation dsc l2 l3 in
-       [InterpretationId interp_id]
-  | st -> []
+      let status,interp_id =
+        Interpretations.add_interpretation status dsc l2 l3
+      in
+       status,[InterpretationId interp_id]
+  | st -> status,[]
 
 let remove_notation = function
   | RuleId id ->
@@ -89,26 +105,8 @@ let remove_notation = function
         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
+  | PrettyPrinterId id -> ()
+  | InterpretationId id -> ()
 
 let history = ref [];;
 
@@ -116,14 +114,10 @@ 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 ()
 ;;
 
 let pop () =
- TermContentPres.pop ();
- Interpretations.pop ();
  CicNotationParser.pop ();
  match !history with
  | [] -> assert false