From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 15 Apr 2006 16:57:24 +0000 (+0000)
Subject: Patch to avoid double execution of whelp queries reverted (since it seems
X-Git-Tag: make_still_working~7400
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=641c040c545910279d60b32a1ce482e8e8246470;p=helm.git

Patch to avoid double execution of whelp queries reverted (since it seems
that queries are NOT executed twice without the patch (!?!) and with the
patch the query is sometimes not executed).
---

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 1e5cb16a8..44be731de 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -772,7 +772,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   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
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
@@ -788,7 +787,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       | _::tl -> aux (i+1) tl
     in
     win#queryInputText#set_text input;
-    do_not_execute_whelp_query:=true;
     combo#set_active (aux 0 queries);
   in
   let set_whelp_query txt =
@@ -832,24 +830,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       activate_combo_query "" "locate";
       win#whelpBarComboVbox#add combo#coerce;
       let start_query () = 
-        if !do_not_execute_whelp_query then
-          do_not_execute_whelp_query := false
-        else
-          begin
-          let query = 
-            try
-              String.lowercase (List.nth queries combo#active) 
-            with Not_found -> assert false
-          in
-          let input = win#queryInputText#text in
-          let statement = 
-            if query = "locate" then
-                "whelp " ^ query ^ " \"" ^ input ^ "\"." 
-              else
-                "whelp " ^ query ^ " (" ^ input ^ ")." 
-          in
-          (MatitaScript.current ())#advance ~statement ()
-          end
+       let query = 
+         try
+           String.lowercase (List.nth queries combo#active) 
+         with Not_found -> assert false in
+       let input = win#queryInputText#text in
+       let statement = 
+         if query = "locate" then
+             "whelp " ^ query ^ " \"" ^ input ^ "\"." 
+           else
+             "whelp " ^ query ^ " (" ^ input ^ ")." 
+       in
+        (MatitaScript.current ())#advance ~statement ()
       in
       ignore(win#queryInputText#connect#activate ~callback:start_query);
       ignore(combo#connect#changed ~callback:start_query);