]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/disambiguate.ml
fixed references to functions moved from Misc to MQueryMisc
[helm.git] / helm / gTopLevel / disambiguate.ml
index ff794fd5b2d03052bbea92803443159b059dda2e..c0e1818e1d18532c6fe480c6f00d05e81112b463 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 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 **)
@@ -71,7 +75,7 @@ module Make(C:Callbacks) =
     let uris =
      List.map
       (function uri,_ ->
-        Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+        MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
     let html=
      " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
@@ -96,7 +100,7 @@ module Make(C:Callbacks) =
           ~id
           uris
      in
-      List.map Misc.cic_textual_parser_uri_of_string uris'
+      List.map MQueryMisc.cic_textual_parser_uri_of_string uris'
 
 
    exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput