X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=0d0b7c4d171afe54dd25b143cbce86194ca8965c;hb=78a92e3cc2deb60d306da93d9dcf987c1cb219ba;hp=e14c9955bcef09b4b4ad6076f322714374347d19;hpb=5aee2f85474686a307f2acda957ffe363a72eff3;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e14c9955b..0d0b7c4d1 100644
--- 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 = "gTopLevel.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";;
 
@@ -188,9 +196,9 @@ let check_window uris =
 
 exception NoChoice;;
 
-let
- interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
-  ?(enable_button_for_non_vars=false) ~title ~msg uris
+let interactive_user_uri_choice
+ ~(selection_mode:[ `SINGLE | `MULTIPLE ])
+ ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris
 =
  let only_constant_choices =
    lazy
@@ -371,7 +379,7 @@ let interactive_interpretation_choice interpretations =
  GtkThread.main ();
  match !chosen with
     None -> raise NoChoice
-  | Some n -> n
+  | Some n -> [n]
 ;;
 
 
@@ -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);;
@@ -1046,7 +1055,7 @@ module DisambiguateCallbacks =
     interactive_user_uri_choice ~selection_mode ?ok
      ?enable_button_for_non_vars ~title ~msg
   let interactive_interpretation_choice = interactive_interpretation_choice
-  let input_or_locate_uri = input_or_locate_uri
+  let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
  end
 ;;
 
@@ -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) ;
@@ -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