X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=fc0fb9cbee4ec2af67bb77d7f2b12ccfc1f269c2;hb=978a25d9392e5fc1a19fa37c86339c5d0b67ddd6;hp=e5cb733bfe179401ba3a9fe8aa584bec940ef40a;hpb=2d4edf383bab53053da30ab591dc0d3140adec34;p=helm.git
diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index e5cb733bf..fc0fb9cbe 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -59,9 +59,11 @@ let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";;
exception Chat_unfinished
-let javascript_quote =
+let javascript_quote s =
let rex = Pcre.regexp "'" in
+ let rex' = Pcre.regexp "\"" in
Pcre.replace ~rex ~templ:"\\'"
+ (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
;;
(* build a bool from a 1-character-string *)
@@ -271,6 +273,7 @@ let callback mqi_handle (req: Http_types.request) outchan =
try
debug_print (sprintf "Received request: %s" req#path);
(match req#path with
+ | "/help" -> Http_daemon.respond ~body:"HELM Search Engine" outchan
| "/execute" ->
let query_string = req#param "query" in
let lexbuf = Lexing.from_string query_string in
@@ -347,23 +350,8 @@ let callback mqi_handle (req: Http_types.request) outchan =
let term_string = req#param "term" in
let (context, metasenv) = ([], []) in
let id_to_uris_raw = req#param "aliases" in
-(*XXX
- let tokens = Pcre.split ~pat:"\\s" id_to_uris_raw in
- let rec parse_tokens keys lookup = function (* TODO spostarla fuori *)
- | [] -> keys, lookup
- | "alias" :: key :: value :: rest ->
- let key' = CicTextualParser0.Id key in
- parse_tokens
- (key'::keys)
- (fun id ->
- if id = key' then
- Some
- (CicTextualParser0.Uri (MQueryMisc.cic_textual_parser_uri_of_string value))
- else lookup id)
- rest
- | _ -> failwith "Can't parse aliases"
- in
-*)
+ let parse_interpretation_choices choices =
+ List.map int_of_string (Pcre.split ~pat:" " choices) in
let parse_choices choices_raw =
let choices = Pcre.split ~pat:";" choices_raw in
List.fold_left
@@ -382,14 +370,18 @@ let callback mqi_handle (req: Http_types.request) outchan =
in
let id_to_uris =
DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in
-print_endline ("id_to_uris_raw: " ^ id_to_uris_raw) ;
-print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id_to_uris)) ;
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 interpretation_choices =
+ try
+ let choices_raw = req#param "interpretation_choices" in
+ Some (parse_interpretation_choices choices_raw)
+ with Http_types.Param_not_found _ -> None
+ in
let module Chat: DisambiguateTypes.Callbacks =
struct
@@ -427,55 +419,48 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
raise Chat_unfinished))
let interactive_interpretation_choice interpretations =
- let html_interpretations_labels =
- String.concat ", "
- (List.map
- (fun l ->
- "\'" ^
- (String.concat "
"
- (List.map
- (fun (id, value) ->
- let id = javascript_quote id in
- let value = javascript_quote value in
- sprintf "alias id %s = %s" id value)
- l)) ^
- "\'")
- interpretations)
- in
- let html_interpretations =
- String.concat ", "
- (List.map
- (fun l ->
- "\'" ^
- (String.concat " "
- (List.map
- (fun (id, value) ->
- let id = javascript_quote id in
- let value = javascript_quote value in
- sprintf "alias id %s = %s"
- id
- (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
- value))
- l)) ^
- "\'")
+ match interpretation_choices with
+ Some l -> prerr_endline "CARRAMBA" ; l
+ | None ->
+ let html_interpretations_labels =
+ String.concat ", "
+ (List.map
+ (fun l ->
+ "\'" ^
+ (String.concat "
"
+ (List.map
+ (fun (id, value) ->
+ let id = javascript_quote id in
+ let value = javascript_quote value in
+ sprintf "%s = %s" id value)
+ l)) ^
+ "\'")
interpretations)
- in
- Http_daemon.send_basic_headers ~code:200 outchan ;
- Http_daemon.send_CRLF outchan ;
- 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 ^ "\n"))
- interactive_interpretation_choice_TPL;
- raise Chat_unfinished
-
- let input_or_locate_uri ~title =
- UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
+ in
+ let html_interpretations =
+ let rec aux n =
+ function
+ [] -> []
+ | _::tl -> ("'" ^ string_of_int n ^ "'")::(aux (n+1) tl)
+ in
+ String.concat ", " (aux 0 interpretations)
+ in
+ Http_daemon.send_basic_headers ~code:200 outchan ;
+ Http_daemon.send_CRLF outchan ;
+ 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 ^ "\n"))
+ interactive_interpretation_choice_TPL;
+ raise Chat_unfinished
+
+ let input_or_locate_uri ~title ?id () =
+ assert false
end
in
@@ -572,29 +557,11 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
(fun line ->
let new_aliases =
DisambiguatingParser.EnvironmentP3.to_string id_to_uris' in
-(*XXX
- match id_to_uris' with
- | (domain, f) ->
- String.concat ", "
- (List.map
- (fun name ->
- sprintf "\'alias %s cic:%s\'"
- (match name with
- CicTextualParser0.Id name -> name
- | _ -> assert false (*CSC: completare *))
- (match f name with
- | None -> assert false
- | Some (CicTextualParser0.Uri t) ->
- MQueryMisc.string_of_cic_textual_parser_uri
- t
- | _ -> assert false (*CSC: completare *)))
- domain)
- in
-*)
let processed_line =
apply_substs
[results_RE, theory_of_result results ;
- new_aliases_RE, new_aliases]
+ (* CSC: Bug here: this is a string, not an array! *)
+ new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'"]
line
in
output_string outchan (processed_line ^ "\n"))