The disambiguation now returns a list of interpretations.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e14c9955bcef09b4b4ad6076f322714374347d19..5df73dc1cacbc71b3fb61443838829c32582888c 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 = "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";;
 
@@ -371,7 +379,7 @@ let interactive_interpretation_choice interpretations =
  GtkThread.main ();
  match !chosen with
     None -> raise NoChoice
-  | Some n -> n
+  | Some n -> [n]
 ;;
 
 
@@ -2835,11 +2843,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