X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=9b100ca718c8f3b4ebf82b1322fa3bfddfb46e5b;hb=aac382f935bc72578119fa7ff9f53c3b649dd0dd;hp=48d419341ca4b2fad4aefbf7891c23dc4b1b868a;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 48d419341..9b100ca71 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -145,3 +145,37 @@ class type console =
     method show : ?msg:string -> unit -> unit
   end
 
+type abouts =
+  [ `Blank
+  | `Current_proof
+  | `Us
+  ]
+  
+type mathViewer_entry =
+  [ `About of abouts  (* current proof *)
+  | `Check of string (* term *)
+  | `Cic of Cic.term * Cic.metasenv
+  | `Dir of string (* "directory" in cic uris namespace *)
+  | `Uri of string (* cic object uri *)
+  | `Whelp of string * string list (* query and results *)
+  ]
+
+let string_of_entry = function
+  | `About `Blank -> "about:blank"
+  | `About `Current_proof -> "about:proof"
+  | `About `Us -> "about:us"
+  | `Check _ -> "check:"
+  | `Cic (_, _) -> "term:"
+  | `Dir uri | `Uri uri -> uri
+  | `Whelp (query, _) -> query
+
+class type mathViewer =
+  object
+    (** @param reuse if set reused last opened cic browser otherwise 
+     *  opens a new one. default is false
+     *)
+    method show_entry: ?reuse:bool -> mathViewer_entry -> unit
+    method show_uri_list:
+      ?reuse:bool -> entry:mathViewer_entry -> string list -> unit
+  end
+