From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 12 Apr 2006 16:22:09 +0000 (+0000)
Subject: whelp locate now accepts * and ?
X-Git-Tag: make_still_working~7421
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=37632a908f126ebe1c927cd5c997434d4cd0bf2c;p=helm.git

whelp locate now accepts * and ?
---

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 6b618c6ac..de6200e09 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -168,7 +168,7 @@ let pp_macro ~term_pp =
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
   | WHint (_, t) -> "whelp hint " ^ term_pp t
-  | WLocate (_, s) -> "whelp locate " ^ s
+  | WLocate (_, s) -> "whelp locate \"" ^ s ^ "\""
   | WElim (_, t) -> "whelp elim " ^ term_pp t
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index aa10bdcf3..8848efad6 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -341,7 +341,7 @@ EXTEND
         GrafiteAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
         GrafiteAst.WInstance (loc,t)
-    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
         GrafiteAst.WLocate (loc,id)
     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
         GrafiteAst.WElim (loc, t)
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