X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fdisambiguate.ml;fp=helm%2FgTopLevel%2Fdisambiguate.ml;h=ce41208dd3ba2833f68b105376f56166a6300ae0;hb=fc3a73230e9c3a8359944ecbc5546f8f63acac25;hp=1e71be5b254b95738d00daf10000ddc8ae221525;hpb=ccff14650d0212aeadf0fcf6ef9ed2e792516686;p=helm.git

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index 1e71be5b2..ce41208dd 100644
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -33,19 +33,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
-(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE                   *)
-let get_last_query = 
- let query = ref "" in
-  let out s = query := ! query ^ s in
-  MQueryGenerator.set_confirm_query
-   (function q -> 
-    query := ""; MQueryUtil.text_of_query out q ""; true);
-  function result ->
-   out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
-   !query
-;;
-
 (** This module provides a functor to disambiguate the input **)
 (** given a set of user-interface call-backs                 **)
 
@@ -78,16 +65,17 @@ module Make(C:Callbacks) =
   struct
 
    let locate_one_id mqi_handle id =
-    let result = MQueryGenerator.locate mqi_handle id in
+    let query  =  MQueryGenerator.locate id in
+    let result = MQueryInterpreter.execute mqi_handle query in
     let uris =
      List.map
       (function uri,_ ->
         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
-    let html=
-     " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
-    in
-     C.output_html html ;
+     C.output_html "<h1>Locate Query: </h1><pre>";
+     MQueryUtil.text_of_query C.output_html query ""; 
+     C.output_html "<h1>Result:</h1>";
+     MQueryUtil.text_of_result C.output_html result "<br>";
      let uris' =
       match uris with
          [] ->