X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fdisambiguate.ml;h=07a03683959ebf43170b07303841f61486d3fea5;hb=6f0bf1e9e4094d452bf318a49979deb5800ac779;hp=efb1c05081d06cd16f1f748e72cfc2be8d21b7f8;hpb=6e2770c280aa9e74604e25324afb680b18d01964;p=helm.git

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index efb1c0508..07a036839 100644
--- 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,7 +46,7 @@ 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 | `MULTIPLE] ->
       ?ok:string ->
@@ -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 "<br>" result;
+     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
          [] ->
@@ -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 =