+ let id_to_uris = parse_tokens [] (fun _ -> None) tokens in
+ let id_to_choices =
+ try
+ let choices_raw = req#param "choices" in
+ parse_choices choices_raw
+ with Http_types.Param_not_found _ -> (fun _ -> None)
+ in
+ let module Chat: Disambiguate.Callbacks =
+ struct
+
+ let output_html = prerr_endline
+
+ let interactive_user_uri_choice
+ ~selection_mode ?ok
+ ?enable_button_for_non_vars ~(title: string) ~(msg: string)
+ ~(id: string) (choices: string list)
+ =
+ (match id_to_choices id with
+ | Some choices -> choices
+ | None ->
+ let msg = Pcre.replace ~pat:"\"" ~templ:"\\\"" msg in
+ (match selection_mode with
+ | `SINGLE -> assert false
+ | `EXTENDED ->
+ iter_file
+ (fun line ->
+ let formatted_choices =
+ String.concat ","
+ (List.map (fun uri -> sprintf "\"%s\"" uri) choices)
+ in
+ let processed_line =
+ apply_substs
+ [title_tag_RE, title;
+ choices_tag_RE, formatted_choices;
+ msg_tag_RE, msg;
+ id_to_uris_RE, id_to_uris_raw;
+ id_RE, id]
+ line
+ in
+ output_string outchan processed_line)
+ interactive_user_uri_choice_TPL;
+ raise Chat_unfinished))
+
+ let interactive_interpretation_choice interpretations =
+ let html_interpretations_labels =
+ String.concat ", "
+ (List.map
+ (fun l ->
+ "\"" ^
+ (String.concat "<br />"
+ (List.map
+ (fun (id, value) ->
+ (sprintf "alias %s %s" id value))
+ l)) ^
+ "\"")
+ interpretations)
+ in
+ let html_interpretations =
+ String.concat ", "
+ (List.map
+ (fun l ->
+ "\"" ^
+ (String.concat " "
+ (List.map
+ (fun (id, value) ->
+ (sprintf "alias %s %s"
+ id
+ (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
+ value)))
+ l)) ^
+ "\"")
+ interpretations)
+ in
+ iter_file
+ (fun line ->
+ let processed_line =
+ apply_substs
+ [interpretations_RE, html_interpretations;
+ interpretations_labels_RE, html_interpretations_labels]
+ line
+ in
+ output_string outchan processed_line)
+ interactive_interpretation_choice_TPL;
+ raise Chat_unfinished
+
+ let input_or_locate_uri ~title =
+ UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
+
+ end
+ in
+ let module Disambiguate' = Disambiguate.Make (Chat) in
+ let (id_to_uris', metasenv', term') =
+ Disambiguate'.disambiguate_input
+ context metasenv dom mk_metasenv_and_expr id_to_uris
+ in
+ (match metasenv' with
+ | [] ->
+ let must = MQueryLevels2.get_constraints term' in
+ let must',only = refine_constraints must in
+ let results = MQueryGenerator.searchPattern must' only in
+ debug_print "FASE 3";
+ iter_file
+ (fun line ->
+ let new_aliases =
+ match id_to_uris' with
+ | (domain, f) ->
+ String.concat ", "
+ (List.map
+ (fun name ->
+ sprintf "\"alias %s cic:%s\""
+ name
+ (match f name with
+ | None -> assert false
+ | Some t ->
+ Disambiguate.string_of_cic_textual_parser_uri
+ t))
+ domain)
+ in
+ let processed_line =
+ apply_substs
+ [results_RE, MQueryUtil.text_of_result results "\n";
+ new_aliases_RE, new_aliases]
+ line
+ in
+ output_string outchan processed_line)
+ final_results_TPL
+ | _ -> (* unable to instantiate some implicit variable *)