From 351cacd582f87110b1ff710ca44ed649f90fbd32 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 12 Apr 2006 16:22:09 +0000
Subject: [PATCH] whelp locate now accepts * and ?

---
 components/grafite/grafiteAstPp.ml         |  2 +-
 components/grafite_parser/grafiteParser.ml |  2 +-
 matita/matitaMathView.ml                   | 13 ++++++++++---
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 6b618c6ac..de6200e09 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/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/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index aa10bdcf3..8848efad6 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/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/matita/matitaMathView.ml b/matita/matitaMathView.ml
index aa1b16a28..a1eef1067 100644
--- a/matita/matitaMathView.ml
+++ b/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
-- 
2.39.2