(* *)
(******************************************************************************)
+open Printf
+
(** This module provides a functor to disambiguate the input **)
(** given a set of user-interface call-backs **)
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 ->
(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
[] ->
) 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 =