X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FcicNotation.mli;h=16422729ba259a0340a43ab0286d7afad4003a91;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=9e231e3317a84f502e4e9558e57187dde8227536;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/lexicon/cicNotation.mli b/matita/components/lexicon/cicNotation.mli
index 9e231e331..16422729b 100644
--- a/matita/components/lexicon/cicNotation.mli
+++ b/matita/components/lexicon/cicNotation.mli
@@ -23,22 +23,21 @@
  * http://helm.cs.unibo.it/
  *)
 
-type notation_id
+class type g_status =
+ object ('self)
+  inherit Interpretations.g_status
+  inherit TermContentPres.g_status
+  inherit CicNotationParser.g_status
+ end
 
-val compare_notation_id : notation_id -> notation_id -> int
+class status :
+ object ('self)
+  inherit Interpretations.status
+  inherit TermContentPres.status
+  inherit CicNotationParser.status
+  method set_notation_status: #g_status -> 'self
+ end
 
-val process_notation: LexiconAst.command -> notation_id list
+val process_notation:
+ #status as 'status -> LexiconAst.command -> 'status 
 
-val remove_notation: notation_id -> unit
-
-(** {2 Notation enabling/disabling}
- * Right now, only disabling of notation during pretty printing is supported.
- * If it is useful to disable it also for the input phase is still to be
- * understood ... *)
-
-val get_all_notations: unit -> (notation_id * string) list  (* id, dsc *)
-val get_active_notations: unit -> notation_id list
-val set_active_notations: notation_id list -> unit
-
-val push: unit -> unit
-val pop: unit -> unit