X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=a1eef10673ca4dc5115994b14bf729976d2cca48;hb=37632a908f126ebe1c927cd5c997434d4cd0bf2c;hp=aa1b16a2871da2dd07959af03b24da61fe19716e;hpb=94409a6e42b8cc0a1a5b2836add266b712f92270;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index aa1b16a28..a1eef1067 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -769,7 +769,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
   in
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
-  let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
+  let whelp_query_RE = Pcre.regexp
+    "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" 
+  in
   let do_not_execute_whelp_query = ref false in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
@@ -793,7 +795,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     let query, arg = 
       try
         let q = Pcre.extract ~rex:whelp_query_RE txt in
-        q.(1), q.(2)
+        q.(1), q.(3)
       with Not_found -> failwith "Malformed Whelp query"
     in
     activate_combo_query arg query;
@@ -839,7 +841,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
             with Not_found -> assert false
           in
           let input = win#queryInputText#text in
-          let statement = "whelp " ^ query ^ " (" ^ input ^ ")." in
+          let statement = 
+            if query = "locate" then
+                "whelp " ^ query ^ " \"" ^ input ^ "\"." 
+              else
+                "whelp " ^ query ^ " (" ^ input ^ ")." 
+          in
           (MatitaScript.current ())#advance ~statement ()
           end
       in