fix

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index b26c2f677221ba96c3180e5963815f3708b6f0db..d956af009239ed6f4d0fa4defd7d98ca19f6353d 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -23,33 +23,50 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** no current proof is available *)
-exception No_proof
+open Printf
+open GrafiteTypes
 
-class type observer =
-  (* "observer" pattern *)
-  object
-    method update: unit -> unit
-  end
+  (** user hit the cancel button *)
+exception Cancel
 
-class subject =
-  (* "observer" pattern *)
-  object
-    val mutable observers = []
-    method attach (o: observer) = observers <- o :: observers
-    method detach (o: observer) =
-      observers <- List.filter (fun o' -> o' != o) observers
-    method notify () = List.iter (fun o -> o#update ()) observers
-  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 UriManager.uri (* cic object uri *)
+  | `Whelp of string * UriManager.uri list (* query and results *)
+  ]
 
-class type command =
-  (* "command" pattern *)
-  object
-    method execute: unit -> unit
-    method undo: unit -> unit
-  end
-
-(** {2 shorthands} *)
+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 -> UriManager.string_of_uri uri
+  | `Whelp (query, _) -> query
 
-type namer = ProofEngineTypes.mk_fresh_name_type
+let entry_of_string = function
+  | "about:blank" -> `About `Blank
+  | "about:proof" -> `About `Current_proof
+  | "about:us"    -> `About `Us
+  | _ ->  (* only about entries supported ATM *)
+      raise (Invalid_argument "entry_of_string")
 
+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 -> UriManager.uri list -> unit
+  end