removed dependency on netclient, use http_client module from ocaml-http

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

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index ce41208dd3ba2833f68b105376f56166a6300ae0..07a03683959ebf43170b07303841f61486d3fea5 100644 (file)
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+open Printf
+
 (** This module provides a functor to disambiguate the input **)
 (** given a set of user-interface call-backs                 **)
 
@@ -44,9 +46,9 @@ module type Callbacks =
     val get_metasenv : unit -> Cic.metasenv
     val set_metasenv : Cic.metasenv -> unit
 
-    val output_html : string -> unit
+    val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
     val interactive_user_uri_choice :
-      selection_mode:[`SINGLE | `EXTENDED] ->
+      selection_mode:[`SINGLE | `MULTIPLE] ->
       ?ok:string ->
       ?enable_button_for_non_vars:bool ->
       title:string -> msg:string -> id:string -> string list -> string list
@@ -72,10 +74,12 @@ module Make(C:Callbacks) =
       (function uri,_ ->
         MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
-     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>";
+     C.output_html (`Msg (`T "Locate query:"));
+     MQueryUtil.text_of_query
+      (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+      "" query; 
+     C.output_html (`Msg (`T "Result:"));
+     MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" result;
      let uris' =
       match uris with
          [] ->
@@ -85,7 +89,7 @@ module Make(C:Callbacks) =
        | [uri] -> [uri]
        | _ ->
          C.interactive_user_uri_choice
-          ~selection_mode:`EXTENDED
+          ~selection_mode:`MULTIPLE
           ~ok:"Try every selection."
           ~enable_button_for_non_vars:true
           ~title:"Ambiguous input."
@@ -142,9 +146,9 @@ module Make(C:Callbacks) =
        ) 1 list_of_uris
      in
       if tests_no > 1 then
-       C.output_html
-        ("<h1>Disambiguation phase started: up to " ^
-          string_of_int tests_no ^ " cases will be tried.") ;
+       C.output_html (`Msg (`T (sprintf
+        "Disambiguation phase started: up to %d cases will be tried"
+        tests_no)));
      (* and now we compute the list of all possible assignments from *)
      (* id to uris that generate well-typed terms                    *)
      let resolve_ids =