Use of standard OCaml syntax

[helm.git] / matita / components / content_pres / termContentPres.mli

diff --git a/matita/components/content_pres/termContentPres.mli b/matita/components/content_pres/termContentPres.mli
index 40e8fc02118a550bc47ffea46b634c3bbdf86420..06dfa70e09c9dbe2ca38f126de21e4bb5dfb57e4 100644 (file)
--- a/matita/components/content_pres/termContentPres.mli
+++ b/matita/components/content_pres/termContentPres.mli
@@ -23,30 +23,35 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** {2 Persistant state handling} *)
+  (** {2 state handling} *)
 
-type pretty_printer_id
+type db
 
-val add_pretty_printer:
-  CicNotationPt.term ->             (* level 2 pattern *)
-  CicNotationParser.checked_l1_pattern ->
-    pretty_printer_id
+class type g_status =
+  object
+    method content_pres_db: db
+  end
 
-exception Pretty_printer_not_found
+class virtual status :
+  object ('self)
+    inherit NCic.status
+    method content_pres_db: db
+    method set_content_pres_db: db -> 'self
+    method set_content_pres_status: #g_status -> 'self
+  end
 
-  (** @raise Pretty_printer_not_found *)
-val remove_pretty_printer: pretty_printer_id -> unit
+val add_pretty_printer:
+ (#status as 'status) ->
+  NotationPt.term ->             (* level 2 pattern *)
+  CicNotationParser.checked_l1_pattern ->
+   'status
 
   (** {2 content -> pres} *)
 
-val pp_ast: CicNotationPt.term -> CicNotationPt.term
+val pp_ast: #status -> NotationPt.term -> NotationPt.term
 
   (** {2 pres -> content} *)
 
   (** fills a term pattern instantiating variable magics *)
 val instantiate_level2:
-  CicNotationEnv.t -> CicNotationPt.term ->
-    CicNotationPt.term
-
-val push: unit -> unit
-val pop: unit -> unit
+ #NCic.status -> NotationEnv.t -> NotationPt.term -> NotationPt.term