X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=13543dbb64d081f4afd1a1a7d2f599a956a11179;hb=112afe13b5aef27425d1a0bc9c71a70b491069bf;hp=c49bce0040049595cbcceda5b405559dc4bb713b;hpb=d0991ea0c7c83c100b2d223644cb2f11a8554fa1;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index c49bce004..13543dbb6 100644
--- 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,144 +23,52 @@
  * http://helm.cs.unibo.it/
  *)
 
-open Printf
-
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
-
-exception Failure of string
-let error s = raise (Failure s)
-let warning s = prerr_endline ("MATITA WARNING:\t" ^ s)
-let debug_print s =
-  if BuildTimeConf.debug then prerr_endline ("MATITA DEBUG:\t" ^ s)
+(* $Id$ *)
 
-let explain = function
-  | StatefulProofEngine.Tactic_failure exn ->
-      sprintf "Tactic failed: %s"(Printexc.to_string exn)
-  | StatefulProofEngine.Observer_failures exns ->
-      String.concat "\n"
-        (List.map (fun (_, exn) -> Printexc.to_string exn) exns)
-  | CicTextualParser2.Parse_error (floc, msg) ->
-      let (x, y) = CicAst.loc_of_floc floc in
-      sprintf "parse error at character %d-%d: %s" x y msg
-  | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
-
-exception No_proof
+open Printf
+open GrafiteTypes
 
+  (** user hit the cancel button *)
 exception Cancel
-exception Unbound_identifier of string
-
-(*
-let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
-
-let unopt_uri ?(kind = `Con) = function
-  | Some uri -> uri
-  | None ->
-      (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri)
-*)
-let unopt_uri = function Some uri -> uri | None -> assert false
-
-class type parserr =  (* "parser" is a keyword :-( *)
-  object
-    method parseTerm:     char Stream.t -> DisambiguateTypes.term
-    method parseTactical: char Stream.t -> DisambiguateTypes.tactical
-  end
 
-class type console =
-  object
-    method echo_message   : string -> unit
-    method echo_error     : string -> unit
-    method clear          : unit -> unit
-    method wrap_exn       : 'a. (unit -> 'a) -> 'a option
-  end
-
-class type disambiguator =
-  object
-    method parserr: parserr
-    method setParserr: parserr -> unit
-
-    method env: DisambiguateTypes.environment
-    method setEnv: DisambiguateTypes.environment -> unit
-
-    method disambiguateTerm:
-      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-        char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
-           CicUniv.universe_graph)
-    method disambiguateTermAst:
-      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-        DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term *
-           CicUniv.universe_graph) 
-
-    method disambiguateTermAsts:
-      ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-      DisambiguateTypes.term list ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
-          CicUniv.universe_graph)
-  end
-
-class type proof =
-  object
-    inherit [unit] StatefulProofEngine.status
-
-    method toXml: Xml.token Stream.t * Xml.token Stream.t
-    method toString: string
-  end
-
-class type currentProof =
-  object
-    method onGoing: unit -> bool
-    method proof: proof
-    method start: proof -> unit
-    method abort: unit -> unit
-    method quit: unit -> unit
-  end
-
-type command_outcome = bool * bool
-
-class type interpreter =
-  object
-    method endOffset : int
-    method evalAst : DisambiguateTypes.tactical -> command_outcome
-    method evalPhrase : string -> command_outcome
-(*     method evalStream: char Stream.t -> command_outcome *)
-    method reset : 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 UriManager.uri (* cic object uri *)
+  | `Whelp of string * UriManager.uri 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 -> UriManager.string_of_uri uri
+  | `Whelp (query, _) -> query
+
+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
-    method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
-    method unload: unit -> unit
-    method set_href_callback: (UriManager.uri -> unit) option -> 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 -> UriManager.uri list -> unit
   end
-
-type mml_of_cic_sequent =
-  Cic.metasenv -> Cic.conjecture ->
-    Gdome.document *
-    ((Cic.id, Cic.term) Hashtbl.t *
-    (Cic.id, Cic.id option) Hashtbl.t *
-    (string, Cic.hypothesis) Hashtbl.t)
-
-type mml_of_cic_object =
-  explode_all:bool -> UriManager.uri -> Cic.annobj ->
-  (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
-    Gdome.document
-
-type namer = ProofEngineTypes.mk_fresh_name_type
-
-type choose_uris_callback =
-  selection_mode:[`MULTIPLE|`SINGLE] ->
-  ?title:string -> ?msg:string -> ?nonvars_button:bool ->
-  string list ->
-    string list
-type choose_interp_callback = (string * string) list list -> int list
-
-let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
-  raise (Failure "ambiguous input")
-let mono_interp_callback _ = raise (Failure "ambiguous input")
-