added comments, fixed history, added loadList to browser

[helm.git] / helm / matita / matitaTypes.ml

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 454c17a7f521afc53be9b9fc9460d75ba3a4b564..f5ec78ee00c33c4ee29f94f1038b069d4de442aa 100644 (file)
--- 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, _) -> sprintf "whelp:%s" 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