modifications to make matita behave reasonably, removed some useless windows

[helm.git] / components / grafite_engine / grafiteTypes.ml

diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml
index 01fb19c5846b9662e0193ddb371c41851a6850c1..71fd19f94b6d7289d1a7a47336d9ed05dab4914a 100644 (file)
--- a/components/grafite_engine/grafiteTypes.ml
+++ b/components/grafite_engine/grafiteTypes.ml
@@ -44,21 +44,23 @@ type proof_status =
       (* 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. *)
 
+(* REMOVE
 module StringMap = Map.Make (String)
 type option_value =
   | String of string
   | Int of int
-type options = option_value StringMap.t
-let no_options = StringMap.empty
+*)
+(* type options = option_value StringMap.t *)
+(* let no_options = StringMap.empty *)
 
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
   proof_status: proof_status;
-  options: options;
+(*   options: options; *)
   objects: UriManager.uri list;
   coercions: UriManager.uri list;
   universe:Universe.universe;  
-  baseuri: string option;
+  baseuri: string;
 }
 
 let get_current_proof status =
@@ -137,19 +139,14 @@ let add_moo_content cmds status =
     GrafiteAstPp.pp_command content')); *)
   { status with moo_content_rev = content' }
 
+let get_baseuri status = status.baseuri;;
+
+(*
 let get_option status name =
   try
     StringMap.find name status.options
   with Not_found -> raise (Option_error (name, "not found"))
  
-let get_baseuri status =
-  match status.baseuri with
-  | Some b -> b, status
-  | None -> 
-      let _,baseuri,_ = Librarian.baseuri_of_script (Librarian.filename()) in
-      baseuri, {status with baseuri = Some baseuri}
-;;
-
 let set_option status name value =
   let types = [ (* no set options defined! *) ] in
   let ty_and_mangler =
@@ -173,6 +170,7 @@ let get_string_option status name =
   match get_option status name with
   | String s -> s
   | _ -> raise (Option_error (name, "not a string value"))
+*)
 
 let dump_status status = 
   HLog.message "status.aliases:\n";
@@ -184,6 +182,7 @@ let dump_status status =
     | Proof _ -> "proof\n"
     | Intermediate _ -> "Intermediate\n");
   HLog.message "status.options\n";
+(* REMOVEME
   StringMap.iter (fun k v -> 
     let v = 
       match v with
@@ -191,6 +190,7 @@ let dump_status status =
       | Int i -> string_of_int i
     in
     HLog.message (k ^ "::=" ^ v)) status.options;
+*)
   HLog.message "status.coercions\n";
   HLog.message "status.objects:\n";
   List.iter