-(* 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
* http://helm.cs.unibo.it/
*)
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
-
- (** exceptions whose content should be presented to the user *)
-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)
-
-exception No_proof (** no current proof is available *)
-
-let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
-
-class type observer =
- (* "observer" pattern *)
- object
- method update: unit -> unit
- end
-
-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
-
-class type command =
- (* "command" pattern *)
+(* $Id$ *)
+
+open Printf
+open GrafiteTypes
+
+ (** user hit the cancel button *)
+exception Cancel
+
+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 execute: unit -> unit
- method undo: unit -> 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
-
-class type parserr = (* "parser" is a keyword :-( *)
- object
- method parseTerm: char Stream.t -> DisambiguateTypes.term
- method parseTactic: char Stream.t -> DisambiguateTypes.tactic
- method parseTactical: char Stream.t -> DisambiguateTypes.tactical
- method parseCommand: char Stream.t -> DisambiguateTypes.command
- method parseScript: char Stream.t -> DisambiguateTypes.script
- end
-
-class type disambiguator =
- object
- method parserr: parserr
- method setParserr: parserr -> unit
-
- method env: DisambiguateTypes.environment
- method setEnv: DisambiguateTypes.environment -> unit
-
- (* TODO Zack: as long as matita doesn't support MDI inteface,
- * disambiguateTerm will return a single term *)
- (** @param env disambiguation environment. If this parameter is given the
- * disambiguator act statelessly, that is internal disambiguation status
- * want be changed but only returned. If this parameter is not given the
- * internal one will be used and updated with the disambiguation status
- * resulting from the disambiguation *)
- method disambiguateTerm:
- ?context:Cic.context -> ?metasenv:Cic.metasenv ->
- ?env:DisambiguateTypes.environment ->
- char Stream.t ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
- (** @param env @see disambiguateTerm above *)
- method disambiguateTermAst:
- ?context:Cic.context -> ?metasenv:Cic.metasenv ->
- ?env:DisambiguateTypes.environment ->
- DisambiguateTypes.term ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
- end
-
-class type proofStatus =
- object
- inherit subject
-
- (** {3 properties} *)
-
- method proof: ProofEngineTypes.proof
- method setProof: ProofEngineTypes.proof -> unit
-
- method goal: ProofEngineTypes.goal option
- method setGoal: ProofEngineTypes.goal option -> unit
-
- (** @raise MatitaTypes.No_proof *)
- method status: ProofEngineTypes.status (* proof, goal *)
- method setStatus: ProofEngineTypes.status -> unit
-
- (** {3 actions} *)
-
- (** return a pair of "xml" (as defined in Xml module) representing the *
- * current proof type and body, respectively *)
- method toXml: Xml.token Stream.t * Xml.token Stream.t
- method toString: string
- end
-
-class type proof =
- object
- (** {3 status} *)
- method status: proofStatus
- method setStatus: proofStatus -> unit
- end
-
-type proof_handler =
- { get_proof: unit -> proof; (* return current proof or fail *)
- set_proof: proof option -> unit; (* set a proof option as current proof *)
- has_proof: unit -> bool; (* check if a current proof is available or not *)
- new_proof: proof -> unit; (* as a set_proof but takes care also to register
- observers *)
- quit: unit -> unit
- }
-
- (** interpreter for toplevel phrases given via console *)
-class type interpreter =
- object
- method evalPhrase: string -> unit
- end
-
-(** {2 shorthands} *)
-
-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
-
projects / helm.git / blobdiff