X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=bfff6fd67d5a1a477d9c0101bf805b0d67b3030e;hb=bbff1250ea4a6c74151ef00340983f2547b2e912;hp=4a5c2e1b5df82414056e8dabc71042c0f7988807;hpb=01a159421d87064d2e5397bfc90630a671e7824a;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 4a5c2e1b5..bfff6fd67 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 *)
@@ -347,6 +349,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
+        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
@@ -365,14 +369,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
 
@@ -410,52 +418,45 @@ 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 "<br />"
-                        (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 "<br />"
+                          (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
+                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 =
               UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
@@ -558,7 +559,8 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
                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"))