MathQL query generator: new interface

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

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index afa47790ac3254173e4b2f708e8a2d570ba0d9f9..ce41208dd3ba2833f68b105376f56166a6300ae0 100644 (file)
--- 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                 **)
 
@@ -77,17 +64,18 @@ type domain_and_interpretation =
 module Make(C:Callbacks) =
   struct
 
-   let locate_one_id id =
-    let result = MQueryGenerator.locate id in
+   let locate_one_id mqi_handle id =
+    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
          [] ->
@@ -121,7 +109,7 @@ module Make(C:Callbacks) =
       Uris of CicTextualParser0.uri list
     | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
 
-   let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
+   let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
     let known_ids,resolve_id = id_to_uris in
     let dom' =
      let rec filter =
@@ -136,7 +124,7 @@ module Make(C:Callbacks) =
      let list_of_uris =
       List.map
        (function
-           CicTextualParser0.Id id -> Uris (locate_one_id id)
+           CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
          | CicTextualParser0.Symbol (descr,choices) ->
             (* CSC: Implementare la funzione di filtraggio manuale *)
             (* CSC: corrispondente alla locate_one_id              *)