]> matita.cs.unibo.it Git - helm.git/commitdiff
fix queries
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 26 Oct 2010 14:00:32 +0000 (14:00 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 26 Oct 2010 14:00:32 +0000 (14:00 +0000)
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaScript.ml

index 71e7cb55334540bbbf61640ecf5b2f2d4b5fcec7..5b8540875124cf5841b6facce09037c7864d3cc8 100644 (file)
@@ -959,7 +959,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
   let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in
   let whelp_query_RE = Pcre.regexp
-    "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" 
+    "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" 
   in
   let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
@@ -1295,7 +1295,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `NRef nref -> self#_loadNReference nref
           | `Univs uri -> self#_loadUnivs uri
           | `Whelp (query, results) -> 
-              set_whelp_query query;
               self#_loadList (List.map (fun r -> "obj",
                 UriManager.string_of_uri r) results));
           self#setEntry entry
index 1e63cc3d18c9d3e2af250576bf25b20e428e5aab..4738a38f673dd55bd6b6496358b655194007a32f 100644 (file)
@@ -433,7 +433,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
-  let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
+  let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) ->