X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=5b8540875124cf5841b6facce09037c7864d3cc8;hb=5431da8145e4a84596d312fc02b552881d119100;hp=d674498cf166cc82aa55402de59f23c31c2dff59;hpb=9bbfd535a4d8f11395159728314b25eb5d9984c0;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index d674498cf..5b8540875 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -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 @@ -981,7 +981,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) combo#set_active (aux 0 queries); in let searchText = - GSourceView.source_view ~auto_indent:false ~editable:false () + GSourceView2.source_view ~auto_indent:false ~editable:false () in let _ = win#scrolledwinContent#add (searchText :> GObj.widget); @@ -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