WARNING: partial commit (does not compile)

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

diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml
index ebc9463ee6b457ed8ae3395d419f13c3872c7440..e25ca3e5726700d3088ac3ba07d032a105ce9719 100644 (file)
--- a/matita/components/lexicon/cicNotation.ml
+++ b/matita/components/lexicon/cicNotation.ml
@@ -29,7 +29,7 @@ open LexiconAst
 
 type notation_id =
   | RuleId of CicNotationParser.rule_id
-  | InterpretationId of TermAcicContent.interpretation_id
+  | InterpretationId of Interpretations.interpretation_id
   | PrettyPrinterId of TermContentPres.pretty_printer_id
 
 let compare_notation_id x y = 
@@ -45,7 +45,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,7 +60,7 @@ 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
@@ -75,11 +75,13 @@ let process_notation st =
         else
           []
       in
-      !rule_id @ pp_id
+       status,!rule_id @ pp_id
   | Interpretation (loc, dsc, l2, l3) ->
-      let interp_id = TermAcicContent.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 ->
@@ -90,25 +92,7 @@ let remove_notation = function
       RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
         !parser_ref_counter item
   | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
-  | InterpretationId id -> TermAcicContent.remove_interpretation id
-
-let get_all_notations () =
-  List.map
-    (fun (interp_id, dsc) ->
-      InterpretationId interp_id, "interpretation: " ^ dsc)
-    (TermAcicContent.get_all_interpretations ())
-
-let get_active_notations () =
-  List.map (fun id -> InterpretationId id)
-    (TermAcicContent.get_active_interpretations ())
-
-let set_active_notations ids =
-  let interp_ids =
-    HExtlib.filter_map
-      (function InterpretationId interp_id -> Some interp_id | _ -> None)
-      ids
-  in
-  TermAcicContent.set_active_interpretations interp_ids
+  | InterpretationId id -> ()
 
 let history = ref [];;
 
@@ -117,13 +101,11 @@ let push () =
  parser_ref_counter := initial_parser_ref_counter ();
  rule_ids_to_items := initial_rule_ids_to_items ();
  TermContentPres.push ();
- TermAcicContent.push ();
  CicNotationParser.push ()
 ;;
 
 let pop () =
  TermContentPres.pop ();
- TermAcicContent.pop ();
  CicNotationParser.pop ();
  match !history with
  | [] -> assert false