]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/disambiguate.ml
MathQL query generator: new interface
[helm.git] / helm / gTopLevel / disambiguate.ml
index 1e71be5b254b95738d00daf10000ddc8ae221525..ce41208dd3ba2833f68b105376f56166a6300ae0 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
-(* 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
          [] ->