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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 3dd457384..6f6b85404 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -37,8 +37,9 @@ open Printf;;
 
 (* DEBUGGING *)
 
-module MQI = MQueryInterpreter
+module MQI  = MQueryInterpreter
 module MQIC = MQIConn
+module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
@@ -384,19 +385,6 @@ let interactive_interpretation_choice interpretations =
 
 (* MISC FUNCTIONS *)
 
-(* 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
-;;
-
 let
  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 =
@@ -957,16 +945,18 @@ let user_uri_choice ~title ~msg uris =
 
 let locate_callback id =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let result = MQueryGenerator.locate mqi_handle id in
+ let out = output_html outputhtml in
+ let query = MQG.locate id in
+ let result = MQI.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
-  output_html outputhtml html ;
+  out "<h1>Locate Query: </h1><pre>";
+  MQueryUtil.text_of_query out query ""; 
+  out "<h1>Result:</h1>";
+  MQueryUtil.text_of_result out result "<br>";
   user_uri_choice ~title:"Ambiguous input."
    ~msg:
      ("Ambiguous input \"" ^ id ^
@@ -1930,7 +1920,8 @@ let completeSearchPattern () =
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = MQueryLevels2.get_constraints expr in
    let must',only = refine_constraints must in
-   let results = MQueryGenerator.searchPattern mqi_handle must' only in 
+   let query = MQG.searchPattern must' only in
+   let results = MQI.execute mqi_handle query in 
     show_query_results results
   with
    e ->