-(* 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/
*)
-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
+ (** @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")
-
projects / helm.git / blobdiff