fixed some macros, added test_abort.ma

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index df10be56336e7b55917180c1e7ad6ae2b47f6cbd..5fe955b3ea5f8124e428b0a7fd28f1815472ee26 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -307,6 +307,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     combo#set_active (aux 0 queries);
     win#queryInputText#set_text input
   in
+  let set_whelp_query txt =
+    let query, arg = 
+      try
+        let q = Pcre.extract ~rex:whelp_query_RE txt in
+        q.(1), q.(2)
+      with Invalid_argument _ -> failwith "Malformed Whelp query"
+    in
+    activate_combo_query arg query
+  in
   let toplevel = win#toplevel in
   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
   let fail msg =
@@ -449,7 +458,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
             | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
             | `Dir dir -> self#_loadDir dir
             | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
-            | `Whelp (query, results) -> self#_loadList results);
+            | `Whelp (query, results) -> 
+                set_whelp_query query;
+                self#_loadList results);
             self#setEntry entry
           end
       with
@@ -556,13 +567,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
       if is_whelp txt then
         begin
-          let q = Pcre.extract ~rex:whelp_query_RE txt in
-          let query, arg = 
-            try
-              q.(1), q.(2)
-            with Invalid_argument _ -> failwith "Malformed Whelp query"
-          in
-          activate_combo_query arg query;
+          set_whelp_query txt;  
+          
+            
           (MatitaScript.instance ())#advance ~statement:(txt^".") ()
         end
       else