module type Callbacks =
sig
- 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 (`Msg (`T "Locate query:"));
+ HelmLogger.log (`Msg (`T "Locate query:"));
MQueryUtil.text_of_query
- (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+ (fun s -> HelmLogger.log ~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;
+ HelmLogger.log (`Msg (`T "Result:"));
+ MQueryUtil.text_of_result (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
let uris' =
match uris with
[] ->
) 1 list_of_uris
in
if tests_no > 1 then
- C.output_html (`Msg (`T (sprintf
+ HelmLogger.log (`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 *)
let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
- let term,_,_,metasenv'' =
+ let term,_,metasenv'' =
CicRefine.type_of_aux' metasenv' context expr
in
Ok (term,metasenv'')
prerr_endline
(Printf.sprintf
"+++++ ASSERTION FAILED: a refine operation should not modify the metasenv. Old metasenv:\n %s\n New metasenv:\n %s\n"
- (CicMetaSubst.ppmetasenv [] metasenv)
- (CicMetaSubst.ppmetasenv [] newmetasenv)) ;
+ (CicMetaSubst.ppmetasenv metasenv [])
+ (CicMetaSubst.ppmetasenv newmetasenv [])) ;
(* an assert would raise an exception that could be caught *)
exit 1
end