got rid of a ~status label

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 08e6e539aa7c1eb9922c0562cb66386a4c8fb2a2..988eb7e143e9a86ba563095a7dac0f4294976904 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -48,13 +48,21 @@ module MQGT = MQGTypes
 module MQGU = MQGUtil
 module MQG  = MQueryGenerator
 
-(* GLOBAL CONSTANTS *)
 
-let configuration_file = "triciclo.conf.xml"
+(* first of all let's initialize the Helm_registry *)
+let _ =
+ let configuration_file = "gTopLevel.conf.xml" in
+  if not (Sys.file_exists configuration_file) then begin
+    eprintf "E: Can't find configuration file '%s'\n" configuration_file;
+    exit 2
+  end;
+ Helm_registry.load_from configuration_file
+;;
+
+(* GLOBAL CONSTANTS *)
 
 let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
-let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
+let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -371,7 +379,7 @@ let interactive_interpretation_choice interpretations =
  GtkThread.main ();
  match !chosen with
     None -> raise NoChoice
-  | Some n -> n
+  | Some n -> [n]
 ;;
 
 
@@ -398,14 +406,14 @@ let
    let innertypesuri = UriManager.innertypesuri_of_uri uri in
     Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
     Http_getter.register' innertypesuri
-     (Helm_registry.get "annotations.url" ^
+     (Helm_registry.get "local_library.url" ^
        Str.replace_first (Str.regexp "^cic:") ""
         (UriManager.string_of_uri innertypesuri) ^ ".xml"
      ) ;
     (* constant type / variable / mutual inductive types definition *)
     Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
     Http_getter.register' uri
-     (Helm_registry.get "annotations.url" ^
+     (Helm_registry.get "local_library.url" ^
        Str.replace_first (Str.regexp "^cic:") ""
         (UriManager.string_of_uri uri) ^ ".xml"
      ) ;
@@ -420,7 +428,7 @@ let
         in
          Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
          Http_getter.register' bodyuri
-          (Helm_registry.get "annotations.url" ^
+          (Helm_registry.get "local_library.url" ^
             Str.replace_first (Str.regexp "^cic:") ""
              (UriManager.string_of_uri bodyuri) ^ ".xml"
           )
@@ -433,7 +441,7 @@ exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
 let pathname_of_annuri uristring =
- Helm_registry.get "annotations.dir" ^    
+ Helm_registry.get "local_library.dir" ^    
   Str.replace_first (Str.regexp "^cic:") "" uristring
 ;;
 
@@ -484,8 +492,8 @@ let qed () =
   (** save an unfinished proof on the filesystem *)
 let save_unfinished_proof () =
  let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
- let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
- let proof_file = Helm_registry.get "triciclo.proof_file" in
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
  Xml.pp ~quiet:true xml (Some proof_file_type) ;
  HelmLogger.log
   (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
@@ -650,6 +658,7 @@ module InvokeTacticsCallbacks =
 
   let decompose_uris_choice_callback = decompose_uris_choice_callback
   let mk_fresh_name_callback = mk_fresh_name_callback
+  let mqi_handle = mqi_handle
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
@@ -676,8 +685,8 @@ let load_unfinished_proof () =
       None -> raise NoChoice
     | Some uri0 ->
        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
-       let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
-       let proof_file = Helm_registry.get "triciclo.proof_file" in
+       let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+       let proof_file = Helm_registry.get "gtoplevel.proof_file" in
         match CicParser.obj_of_xml proof_file_type (Some proof_file) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
@@ -2067,7 +2076,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.matchConclusion mqi_handle
-            ~choose_must () ~status:(proof, metano)
+            ~choose_must () (proof, metano)
          in
          let uri' =
           user_uri_choice ~title:"Ambiguous input."
@@ -2364,6 +2373,9 @@ object(self)
    let contradictionb =
     GButton.button ~label:"Contradiction"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+   let autob=
+    GButton.button ~label:"Auto"
+     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
    let hbox4 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let existsb =
@@ -2495,6 +2507,7 @@ object(self)
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
    ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
+   ignore(autob#connect#clicked InvokeTactics'.auto) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
@@ -2585,7 +2598,7 @@ end
 
 let dump_environment () =
   try
-    let oc = open_out (Helm_registry.get "triciclo.environment_file") in
+    let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in
     HelmLogger.log (`Msg (`T "Dumping environment ..."));
     CicEnvironment.dump_to_channel oc;
     HelmLogger.log (`Msg (`T "... done!")) ;
@@ -2597,7 +2610,7 @@ let dump_environment () =
 ;;
 let restore_environment () =
   try
-    let ic = open_in (Helm_registry.get "triciclo.environment_file") in
+    let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in
     HelmLogger.log (`Msg (`T "Restoring environment ... "));
     CicEnvironment.restore_from_channel ic;
     HelmLogger.log (`Msg (`T "... done!"));
@@ -2835,11 +2848,6 @@ end
 (* MAIN *)
 
 let initialize_everything () =
-  if not (Sys.file_exists configuration_file) then begin
-    eprintf "E: Can't find configuration file '%s'\n" configuration_file;
-    exit 2
-  end;
-  Helm_registry.load_from configuration_file;
   let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
   let notebook = new notebook in
   let rendering_window' = new rendering_window output notebook in
@@ -2853,7 +2861,7 @@ let initialize_everything () =
     (Some (print_error_as_html "XSLT Debug Message: "));
   rendering_window'#show () ;
   if restore_environment_on_boot &&
-    Sys.file_exists (Helm_registry.get "triciclo.environment_file")
+    Sys.file_exists (Helm_registry.get "gtoplevel.environment_file")
   then
     restore_environment ();
   GtkThread.main ()