]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
Disambiguation can now return more than one choice.
[helm.git] / helm / searchEngine / searchEngine.ml
index 507dadb63d207546cd9cee1cabe272c315aab669..2d8a7067c5fbe5e4edcd2df82ee1a0c7c7a1b43e 100644 (file)
@@ -472,8 +472,12 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
         in
         let module Disambiguate' = DisambiguatingParser.Make(Chat) in
         let (id_to_uris', metasenv', term') =
+         match
           Disambiguate'.disambiguate_term mqi_handle
             context metasenv term_string id_to_uris
+         with
+            [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term'
+          | _ -> assert false
         in
         (match metasenv' with
         | [] ->
@@ -610,7 +614,7 @@ printf "Current directory is %s\n" (Sys.getcwd ());
 printf "HTML directory is %s\n" pages_dir;
 flush stdout;
 Unix.putenv "http_proxy" "";
-let mqi_handle = C.init debug_print in
+let mqi_handle = C.init ~log:debug_print () in
 Http_daemon.start' ~port (callback mqi_handle);
 C.close mqi_handle;
 printf "%s is terminating, bye!\n" daemon_name