Bug fixed: "paste as pattern" now pastes the full pattern (e.g.

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 1e5cb16a804510402b47d0e3c201f2232783ccf6..5de25e45b13b784bca64eb50c5fafbe7d7341f99 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -246,21 +246,24 @@ object (self)
         | _ -> leave_href ())
     | None -> leave_href ()
 
+
+  method private tactic_text_pattern_of_node node =
+   let id = id_of_node node in
+   let cic_info, unsh_sequent = self#get_cic_info id in
+   match self#get_term_by_id cic_info id with
+   | SelTerm (t, father_hyp) ->
+       let sequent = self#sequent_of_id ~paste_kind:`Pattern id in
+       let text = self#string_of_cic_sequent sequent in
+       (match father_hyp with
+       | None -> None, [], Some text
+       | Some hyp_name -> None, [ hyp_name, text ], None)
+   | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
+
     (** @return a pattern structure which contains pretty printed terms *)
   method private tactic_text_pattern_of_selection =
     match self#get_selections with
     | [] -> assert false (* this method is invoked only if there's a sel. *)
-    | node :: _ ->
-        let id = id_of_node node in
-        let cic_info, unsh_sequent = self#get_cic_info id in
-        match self#get_term_by_id cic_info id with
-        | SelTerm (t, father_hyp) ->
-            let sequent = self#sequent_of_id ~paste_kind:`Pattern id in
-            let text = self#string_of_cic_sequent sequent in
-            (match father_hyp with
-            | None -> None, [], Some text
-            | Some hyp_name -> None, [ hyp_name, text ], None)
-        | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
+    | node :: _ -> self#tactic_text_pattern_of_node node
 
   method private popup_contextual_menu time =
     let menu = GMenu.menu () in
@@ -417,8 +420,10 @@ object (self)
   method private string_of_node ~(paste_kind:paste_kind) node =
     if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
     then
-      let id = id_of_node node in
-      self#string_of_cic_sequent (self#sequent_of_id ~paste_kind id)
+     let tactic_text_pattern =  self#tactic_text_pattern_of_node node in
+      GrafiteAstPp.pp_tactic_pattern
+       ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
+       tactic_text_pattern
     else string_of_dom_node node
 
   method private string_of_cic_sequent cic_sequent =
@@ -772,7 +777,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 +792,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 +835,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);