X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2Finterpretations.mli;h=8ee3fc01f943fcf7cd66c7e526671b74eeb8153c;hb=01b29f47d0d3e6c131fbdcc7a4180d428c8c97b9;hp=222a340f4ea6de8f3c84c7ee0d18d200c2f56f96;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli
index 222a340f4..8ee3fc01f 100644
--- a/matita/components/content/interpretations.mli
+++ b/matita/components/content/interpretations.mli
@@ -24,32 +24,46 @@
  *)
 
 
-  (** {2 Persistant state handling} *)
+  (** {2 State handling} *)
 
-type interpretation_id
+type db
+
+class type g_status =
+  object
+    method interp_db: db
+  end
+
+class status :
+  object ('self)
+    method interp_db: db
+    method set_interp_db: db -> 'self
+    method set_interp_status: #g_status -> 'self
+  end
+
+type cic_id = string
 
 val add_interpretation:
+  #status as 'status ->
   string ->                                       (* id / description *)
   string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
   NotationPt.cic_appl_pattern ->               (* level 3 pattern *)
-    interpretation_id
+    'status
 
-  (** @raise Interpretation_not_found *)
-val lookup_interpretations:
-  ?sorted:bool -> string -> (* symbol *)
-    (string * NotationPt.argument_pattern list *
-      NotationPt.cic_appl_pattern) list
+val set_load_patterns32: 
+ ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit
 
 exception Interpretation_not_found
 
   (** @raise Interpretation_not_found *)
-val remove_interpretation: interpretation_id -> unit
+val lookup_interpretations:
+  #status ->
+   ?sorted:bool -> string -> (* symbol *)
+    (string * NotationPt.argument_pattern list *
+      NotationPt.cic_appl_pattern) list
 
   (** {3 Interpretations toggling} *)
 
-val get_all_interpretations: unit -> (interpretation_id * string) list
-val get_active_interpretations: unit -> interpretation_id list
-val set_active_interpretations: interpretation_id list -> unit
+val toggle_active_interpretations: #status as 'status -> bool -> 'status
 
   (** {2 content -> cic} *)
 
@@ -58,20 +72,11 @@ val set_active_interpretations: interpretation_id list -> unit
 val instantiate_appl_pattern:
   mk_appl:('term list -> 'term) -> 
   mk_implicit:(bool -> 'term) ->
-  term_of_uri : (UriManager.uri -> 'term) ->
   term_of_nref : (NReference.reference -> 'term) ->
   (string * 'term) list -> NotationPt.cic_appl_pattern ->
     'term
 
-val push: unit -> unit
-val pop: unit -> unit
-
-(* for Matita NG *)
 val find_level2_patterns32:
- int ->
-  string * string *
-   NotationPt.argument_pattern list * NotationPt.cic_appl_pattern
-
-val add_load_patterns32: 
- ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit
-val init: unit -> unit
+  #status -> int ->
+   string * string * NotationPt.argument_pattern list *
+    NotationPt.cic_appl_pattern