From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 9 Mar 2004 16:09:13 +0000 (+0000)
Subject: Partially ported to new disambiguating parser.
X-Git-Tag: v0_0_4~26
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=144b71e5ca75b56c0cc3cc63e2b2045ef9deb6c0;p=helm.git

Partially ported to new disambiguating parser.
Some bugs left (e.g. in aliases)
---

diff --git a/helm/searchEngine/html/index.html b/helm/searchEngine/html/index.html
index e7b73b5d2..fb5c2d45a 100644
--- a/helm/searchEngine/html/index.html
+++ b/helm/searchEngine/html/index.html
@@ -551,13 +551,14 @@ function templateambigpdq2_listainterpretazioni(document,elenco,labels)
 function templateambigpdq2_invia(document,elenco)
 	{
 	stringa=top.topurl+"/"+top.current_query+"?term="+top.terminecic;
-	stringa=stringa+"&aliases=";
-	controllo=stringa.length;
+	stringa=stringa+"&aliases=&interpretation_choices=";
+  var parsa = "";
+	controllo=parsa.length;
 	for (j=0;j<elenco.length;j++)
 		{
 		if (document.disamb.interp[j].checked)
 			{
-			stringa=stringa+escape(elenco[j]);
+			parsa=parsa+escape(elenco[j]);
 
       // TODO da implementare nella terza fase
 			//top.aliasglob[top.aliasglob.length]=document.disamb.interp[j].value;
@@ -567,7 +568,9 @@ function templateambigpdq2_invia(document,elenco)
 			}
 			
 		}
-	if (stringa.length!=controllo) 
+  top.interpretation_choices = parsa;
+  stringa=stringa+parsa;
+	if (parsa.length!=controllo) 
 		{
 		window.open(ask_uwobo(stringa),"cw");
 		}
@@ -598,6 +601,7 @@ function constraints_choice_template_invia(document,aliases,constr_obj_len,const
 	stringa=top.topurl+"/"+top.current_query+"?term="+top.terminecic;
 	stringa=stringa+"&aliases="+escape(aliases);
 	stringa=stringa+"&choices="+escape(top.choices);
+	stringa=stringa+"&interpretation_choices="+escape(top.interpretation_choices);
 	stringa=stringa+"&constraints=";
 	for (j=0;j<constr_obj_len;j++)
 	 {
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"))