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 ->
?enable_button_for_non_vars:bool ->
title:string -> msg:string -> id:string -> string list -> string list
val interactive_interpretation_choice :
- (string * string) list list -> int
- val input_or_locate_uri : title:string -> UriManager.uri
+ (string * string) list list -> int list
+ val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri
end
;;
(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
[] ->
[UriManager.string_of_uri
(C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
| [uri] -> [uri]
| _ ->
C.interactive_user_uri_choice
) 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 *)
CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
Uncertain
- | _ ->
+ | CicRefine.RefineFailure _ ->
prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
Ko
in
exit 1
end
) resolve_ids ;
- let resolve_id',term,metasenv' =
+ let res =
match resolve_ids with
[] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
- | [resolve_id] -> resolve_id
+ | [_] -> resolve_ids
| _ ->
let choices =
List.map
) dom
) resolve_ids
in
- let index = C.interactive_interpretation_choice choices in
- List.nth resolve_ids index
+ let indexes = C.interactive_interpretation_choice choices in
+ List.map (List.nth resolve_ids) indexes
in
- (known_ids @ dom', resolve_id'), metasenv',term
+ List.map
+ (fun (resolve_id',term,metasenv') ->
+ (known_ids @ dom', resolve_id'), metasenv',term
+ ) res
end
;;