X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=d7dc383b7757fc5d4da9c6a5b9d34abe99bb95f1;hb=fd372e069bbcaa96dc5b2eef04f341b28850d726;hp=acae4c9dfe2d4d5cbd89da094823fb4c15a81d67;hpb=07dde6f87105c18b28fc784b7d596a5d242e1225;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index acae4c9df..d7dc383b7 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,75 +23,160 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
+open Printf
 
-  (** 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: " ^ s)
+  (** user hit the cancel button *)
+exception Cancel
 
-exception No_proof  (** no current proof is available *)
-exception No_choice (** no choice was made by the user *)
+  (** statement invoked in the wrong context (e.g. tactic with no ongoing proof)
+   *)
+exception Statement_error of string
+let statement_error msg = raise (Statement_error msg)
 
-class type observer =
-  (* "observer" pattern *)
-  object
-    method update: unit -> unit
-  end
+exception Command_error of string
+let command_error msg = raise (Command_error msg)
 
-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
+  (** parameters are: option name, error message *)
+exception Option_error of string * string
 
-class type command =
-  (* "command" pattern *)
-  object
-    method execute: unit -> unit
-    method undo: unit -> unit
-  end
+exception Unbound_identifier of string
 
-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
+type proof_status =
+  | No_proof
+  | Incomplete_proof of ProofEngineTypes.status
+  | Proof of ProofEngineTypes.proof
+  | Intermediate of Cic.metasenv
+      (* Status in which the proof could be while it is being processed by the
+      * engine. No status entering/exiting the engine could be in it. *)
+
+module StringMap = Map.Make (String)
 
-class type disambiguator =
+type option_value =
+  | String of string
+  | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
+
+type status = {
+  aliases: DisambiguateTypes.environment;   (** disambiguation aliases *)
+  proof_status: proof_status;
+  options: options;
+  objects: (UriManager.uri * string) list;
+    (** in-scope objects, with their paths *)
+}
+
+let dump_status status = 
+  MatitaLog.message "status.aliases:\n";
+  MatitaLog.message
+  (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+  MatitaLog.message "status.proof_status:"; 
+  MatitaLog.message
+    (match status.proof_status with
+    | No_proof -> "no proof\n"
+    | Incomplete_proof _ -> "incomplete proof\n"
+    | Proof _ -> "proof\n"
+    | Intermediate _ -> "Intermediate\n");
+  MatitaLog.message "status.options\n";
+  StringMap.iter (fun k v -> 
+    let v = 
+      match v with
+      | String s -> s
+      | Int i -> string_of_int i
+    in
+    MatitaLog.message (k ^ "::=" ^ v)) status.options;
+  MatitaLog.message "status.coercions\n";
+  MatitaLog.message "status.objects:\n";
+  List.iter 
+    (fun (u,_) -> 
+      MatitaLog.message (UriManager.string_of_uri u)) status.objects 
+  
+
+let get_option status name =
+  try
+    StringMap.find name status.options
+  with Not_found -> raise (Option_error (name, "not found"))
+
+let get_string_option status name =
+  match get_option status name with
+  | String s -> s
+  | _ -> raise (Option_error (name, "not a string value"))
+
+let set_option status name value =
+  let mangle_dir s =
+    let s = Str.global_replace (Str.regexp "//+") "/" s in
+    let s = Str.global_replace (Str.regexp "/$") "" s in
+    s
+  in
+  let types =
+    [ "baseuri", (`String, mangle_dir);
+      "basedir", (`String, mangle_dir);
+    ]
+  in
+  let ty_and_mangler =
+    try
+      List.assoc name types
+    with Not_found -> command_error (sprintf "Unknown option \"%s\"" name)
+  in
+  let value =
+    match ty_and_mangler with
+    | `String, f -> String (f value)
+    | `Int, f ->
+        (try
+          Int (int_of_string (f value))
+        with Failure _ ->
+          command_error (sprintf "Not an integer value \"%s\"" value))
+  in
+  { status with options = StringMap.add name value status.options }
+
+  (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
   object
-    method parserr: parserr
-    method setParserr: parserr -> unit
-
-    method disambiguateTerm:
-      context:Cic.context -> metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-        char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list
-    method disambiguateTermAst:
-      context:Cic.context -> metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-        DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list
+    method clear : unit -> unit
+    method echo_error : string -> unit
+    method echo_message : string -> unit
+    method wrap_exn : 'a. (unit -> 'a) -> 'a option
+    method choose_uri : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
-(** {2 shorthands} *)
-
-type namer = ProofEngineTypes.mk_fresh_name_type
+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 string (* cic object uri *)
+  | `Whelp of string * string list (* query and results *)
+  ]
 
-type choose_uris_callback =
-  selection_mode:Gtk.Tags.selection_mode ->
-  ?title:string -> ?msg:string -> ?nonvars_button:bool ->
-  string list ->
-    string list
+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, _) -> query
 
-type choose_interp_callback = (string * string) list list -> int list
+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 -> string list -> unit
+  end
+