X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fdisambiguate.ml;h=2f02818474b5ccdd1e2f606dd0470817e85c2571;hb=a3ef256812f0397a871fe8e69c125dfd89e62dce;hp=ff794fd5b2d03052bbea92803443159b059dda2e;hpb=92515ddd2fc43f07f4dbb22c6bc98399ef1a2dd7;p=helm.git

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index ff794fd5b..2f0281847 100644
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -34,12 +34,16 @@
 (******************************************************************************)
 
 (* 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 q ; true) ;
+   (function q -> 
+    query := ""; MQueryUtil.text_of_query out q ""; true);
   function result ->
-   !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+   out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
+   !query
 ;;
 
 (** This module provides a functor to disambiguate the input **)