X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaMathView.ml;h=5de25e45b13b784bca64eb50c5fafbe7d7341f99;hb=f80a8edd258a2ca7fa27d8fbccafc11625460455;hp=746ef8ffa67c74c7bdc455ca7e23d25e0d976d4e;hpb=5da71ef0e78fd5d7faf26b14e823e33f1e7c9f53;p=helm.git diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 746ef8ffa..5de25e45b 100644 --- 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 @@ -338,7 +341,8 @@ object (self) (fun uri -> let menu_item = GMenu.menu_item ~label:uri ~packing:menu#append () in - connect_menu_item menu_item (fun () -> f uri)) + connect_menu_item menu_item + (fun () -> try f uri with Not_found -> assert false)) uris; menu#popup ~button ~time) @@ -416,14 +420,17 @@ 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 = let script = MatitaScript.current () in let metasenv = if script#onGoingProof () then script#proofMetasenv else [] in + (* let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = Cic2acic.asequent_of_sequent metasenv cic_sequent in let _, _, _, annterm = acic_sequent in @@ -432,6 +439,9 @@ object (self) let pped_ast = TermContentPres.pp_ast ast in let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup + *) + ApplyTransformation.txt_of_cic_sequent_conclusion + text_width metasenv cic_sequent method private pattern_of term context unsh_sequent = let context_len = List.length context in @@ -764,7 +774,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" in let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in - let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in + let whelp_query_RE = Pcre.regexp + "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" + 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 @@ -779,17 +791,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | h::_ when String.lowercase h = q' -> i | _::tl -> aux (i+1) tl in + win#queryInputText#set_text input; 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" + q.(1), q.(3) + with Not_found -> failwith "Malformed Whelp query" in - activate_combo_query arg query + activate_combo_query arg query; in let toplevel = win#toplevel in let mathView = cicMathView ~packing:win#scrolledBrowser#add () in @@ -801,11 +813,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png"); "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ] in + let b = (not (Helm_registry.get_bool "matita.debug")) in let handle_error f = try f () with exn -> - if not (Helm_registry.get_bool "matita.debug") then + if b then fail (snd (MatitaExcPp.to_string exn)) else raise exn in @@ -822,9 +835,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) activate_combo_query "" "locate"; win#whelpBarComboVbox#add combo#coerce; let start_query () = - let query = String.lowercase (List.nth queries combo#active) in - let input = win#queryInputText#text in - let statement = "whelp " ^ query ^ " " ^ input ^ "." in + 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);