]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix: implemented interactive_user_uri_choice (trivial non-"advanced"
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 26 Oct 2004 12:44:13 +0000 (12:44 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 26 Oct 2004 12:44:13 +0000 (12:44 +0000)
implementation: filter out variables)

helm/searchEngine/searchEngine.ml

index 8bcd141b0fdfe218c15cfc2a90d454cc49395d39..d327c71bf54a80af3be15d10e543ad5f49d90687 100644 (file)
@@ -98,6 +98,10 @@ let javascript_quote s =
 let string_tail s =
   let len = String.length s in
   String.sub s 1 (len-1)
+let nonvar s =
+  let len = String.length s in
+  let suffix = String.sub s (len-4) 4 in
+  not (suffix  = ".var")
 
 let add_param_substs params =
   List.map
@@ -196,19 +200,19 @@ let exec_action dbh (req: Http_types.request) outchan =
     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
-        (fun f x ->
-           match Pcre.split ~pat:"\\s" x with
-             | ""::id::tail
-             | id::tail when id<>"" ->
-                 (fun id' ->
-                    if id = id' then
-                      Some (List.map (fun u -> Netencoding.Url.decode u) tail)
-                    else
-                      f id')
-             | _ -> failwith "Can't parse choices")
-        (fun _ -> None)
-        choices
+    List.fold_left
+      (fun f x ->
+         match Pcre.split ~pat:"\\s" x with
+           | ""::id::tail
+           | id::tail when id<>"" ->
+               (fun id' ->
+                  if id = id' then
+                    Some (List.map (fun u -> Netencoding.Url.decode u) tail)
+                  else
+                    f id')
+           | _ -> failwith "Can't parse choices")
+      (fun _ -> None)
+      choices
   in
   let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
   let id_to_choices =
@@ -231,7 +235,7 @@ let exec_action dbh (req: Http_types.request) outchan =
       =
         match id_to_choices id with
         | Some choices -> choices
-        | None -> assert false
+        | None -> List.filter nonvar choices
 
       let interactive_interpretation_choice interpretations =
         match interpretation_choices with