X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaTypes.ml;h=9b100ca718c8f3b4ebf82b1322fa3bfddfb46e5b;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=454c17a7f521afc53be9b9fc9460d75ba3a4b564;hpb=3b5b254f2faa600a14a837e95f94f953dc9959c7;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 454c17a7f..9b100ca71 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -145,14 +145,37 @@ class type console =
     method show : ?msg:string -> unit -> unit
   end
 
-type term_source =
-  [ `Ast of DisambiguateTypes.term
+type abouts =
+  [ `Blank
+  | `Current_proof
+  | `Us
+  ]
+  
+type mathViewer_entry =
+  [ `About of abouts  (* current proof *)
+  | `Check of string (* term *)
   | `Cic of Cic.term * Cic.metasenv
-  | `String of string
+  | `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
-    method show_term: term_source -> unit
+    (** @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