X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=794b849c4918202171780c1b2c496c0b1b7a7a2e;hb=aa0d60227b785da3355b31519ba11cb4fbd2c925;hp=507837c15cb239e995d174534f83f9e1acf56252;hpb=78cd354ba5225f6431ab0bab6dcaa548bb5a24c3;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 507837c15..794b849c4 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -23,10 +23,13 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf -open MatitaTypes +open GrafiteTypes open MatitaGtkMisc +open MatitaGuiTypes module Stack = Continuationals.Stack @@ -136,8 +139,24 @@ let string_of_dom_node node = text#get_data#to_string with GdomeInit.DOMCastException _ -> "") +let name_of_hypothesis = function + | Some (Cic.Name s, _) -> s + | _ -> assert false + +let id_of_node (node: Gdome.element) = + let xref_attr = + node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds in + try + List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) + with Failure _ -> assert false + +type selected_term = + | SelTerm of Cic.term * string option (* term, parent hypothesis (if any) *) + | SelHyp of string * Cic.context (* hypothesis, context *) + class clickableMathView obj = let text_width = 80 in +let dummy_loc = HExtlib.dummy_floc in object (self) inherit GMathViewAux.multi_selection_math_view obj @@ -161,12 +180,23 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = - (match self#get_selections with - | [] -> () - | node :: _ -> ctxt#return (self#string_of_node node)) + let text = + match ctxt#target with + | "PATTERN" -> self#text_of_selection `Pattern + | "TERM" | _ -> self#text_of_selection `Term + in + match text with + | None -> () + | Some s -> ctxt#return s + + method private text_of_selection fmt = + match self#get_selections with + | [] -> None + | node :: _ -> Some (self#string_of_node ~paste_kind:fmt node) method private selection_clear_cb sel_event = self#remove_selections; + (GData.clipboard Gdk.Atom.clipboard)#clear (); false method private button_press_cb gdk_button = @@ -179,21 +209,59 @@ object (self) self#popup_contextual_menu (GdkEvent.Button.time gdk_button); false + (** @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 + method private popup_contextual_menu time = - match self#string_of_selection with - | None -> () - | Some s -> - let clipboard = GData.clipboard Gdk.Atom.clipboard in - let menu = GMenu.menu () in - let copy_menu_item = - GMenu.image_menu_item - ~label:"_Copy" ~stock:`COPY ~packing:menu#append () - in - connect_menu_item copy_menu_item (fun () -> clipboard#set_text s); - menu#popup ~button:right_button ~time + let menu = GMenu.menu () in + let add_menu_item ?(menu = menu) ?stock ?label () = + GMenu.image_menu_item ?stock ?label ~packing:menu#append () in + let check = add_menu_item ~label:"Check" () in + let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in + menu#append reductions_menu_item; + let reductions = GMenu.menu () in + reductions_menu_item#set_submenu reductions; + let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in + let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in + let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in + let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in + menu#append (GMenu.separator_item ()); + let copy = add_menu_item ~stock:`COPY () in + let gui = get_gui () in + List.iter (fun item -> item#misc#set_sensitive gui#canCopy) + [ copy; check; normalize; reduce; simplify; whd ]; + let reduction_action kind () = + let pat = self#tactic_text_pattern_of_selection in + let statement = + let loc = HExtlib.dummy_floc in + "\n" ^ + GrafiteAstPp.pp_executable ~term_pp:(fun s -> s) + ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) + (GrafiteAst.Tactical (loc, + GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)), + Some (GrafiteAst.Semicolon loc))) in + (MatitaScript.current ())#advance ~statement () in + connect_menu_item copy gui#copy; + connect_menu_item normalize (reduction_action `Normalize); + connect_menu_item reduce (reduction_action `Reduce); + connect_menu_item simplify (reduction_action `Simpl); + connect_menu_item whd (reduction_action `Whd); + menu#popup ~button:right_button ~time method private button_release_cb gdk_button = - let clipboard = GData.clipboard Gdk.Atom.primary in if GdkEvent.Button.button gdk_button = left_button then begin let button_release_x = GdkEvent.Button.x gdk_button in let button_release_y = GdkEvent.Button.y gdk_button in @@ -233,20 +301,17 @@ object (self) List.iter (fun uri -> let menu_item = - GMenu.menu_item ~label:uri ~packing:menu#append () - in + GMenu.menu_item ~label:uri ~packing:menu#append () in connect_menu_item menu_item (fun () -> f uri)) uris; menu#popup ~button ~time) method private choose_selection_cb gdome_elt = - let (gui: MatitaGuiTypes.gui) = get_gui () in - let clipboard = GData.clipboard Gdk.Atom.primary in let set_selection elt = + let misc = self#coerce#misc in self#set_selection (Some elt); - self#coerce#misc#add_selection_target - ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary; - ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) + misc#add_selection_target ~target:"STRING" Gdk.Atom.primary; + ignore (misc#grab_selection Gdk.Atom.primary); in let rec aux elt = if (elt#getAttributeNS ~namespaceURI:helm_ns @@ -270,20 +335,36 @@ object (self) method update_font_size = self#set_font_size !current_font_size + (** find a term by id from stored CIC infos @return either `Hyp if the id + * correspond to an hypothesis or `Term (cic, hyp) if the id correspond to a + * term. In the latter case hyp is either None (if the term is a subterm of + * the sequent conclusion) or Some hyp_name if the term belongs to an + * hypothesis *) method private get_term_by_id cic_info id = - let unsh_item, ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in + let unsh_item, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, _, _ = + cic_info in + let rec find_father_hyp id = + if Hashtbl.mem ids_to_hypotheses id + then Some (name_of_hypothesis (Hashtbl.find ids_to_hypotheses id)) + else + let father_id = + try Hashtbl.find ids_to_father_ids id + with Not_found -> assert false in + match father_id with + | Some id -> find_father_hyp id + | None -> None + in try - `Term (Hashtbl.find ids_to_terms id) + let term = Hashtbl.find ids_to_terms id in + let father_hyp = find_father_hyp id in + SelTerm (term, father_hyp) with Not_found -> try let hyp = Hashtbl.find ids_to_hypotheses id in let _, context, _ = - match unsh_item with - | Some seq -> seq - | None -> assert false - in + match unsh_item with Some seq -> seq | None -> assert false in let context' = MatitaMisc.list_tl_at hyp context in - `Hyp context' + SelHyp (name_of_hypothesis hyp, context') with Not_found -> assert false method private find_obj_conclusion id = @@ -296,78 +377,92 @@ object (self) in (try Hashtbl.find ids_to_terms id with Not_found -> assert false) - method private string_of_node node = + method private string_of_node ~(paste_kind:paste_kind) node = if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds - then self#string_of_id_node node + then + let id = id_of_node node in + self#string_of_cic_sequent (self#sequent_of_id ~paste_kind id) else string_of_dom_node node - method private string_of_id_node node = - let get_id (node: Gdome.element) = - let xref_attr = - node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds - in - List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) - in - let id = get_id node in + method private string_of_cic_sequent cic_sequent = let script = MatitaScript.current () in let metasenv = - if script#onGoingProof () then - script#proofMetasenv - else - [] - in -(* TODO: code for patterns - let conclusion = (MatitaScript.instance ())#proofConclusion in - let conclusion_pattern = - ProofEngineHelpers.pattern_of ~term:conclusion cic_terms - in -*) - let string_of_cic_sequent cic_sequent = - let _, (acic_sequent, _, _, ids_to_inner_sorts, _) = - Cic2acic.asequent_of_sequent metasenv cic_sequent - in - let _, _, _, annterm = acic_sequent in - let ast, ids_to_uris = - CicNotationRew.ast_of_acic ids_to_inner_sorts annterm - in - let pped_ast = CicNotationRew.pp_ast ast in - let markup = CicNotationPres.render ids_to_uris pped_ast in - BoxPp.render_to_string text_width markup - in - let cic_info, unsh_sequent = - match self#cic_info with - | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> - info, unsh_sequent - | Some ((None, _, _, _, _, _) as info) -> - (* building a dummy sequent for obj *) - let t = self#find_obj_conclusion id in - MatitaLog.debug (CicPp.ppterm t); - info, (~-1, [], t) - | None -> assert false - in + 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 + let ast, ids_to_uris = + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in + 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 + + method private pattern_of term context unsh_sequent = + let context_len = List.length context in + let _, unsh_context, conclusion = unsh_sequent in + try + (match + List.nth unsh_context (List.length unsh_context - context_len - 1) + with + | None -> assert false (* can't select a restricted hypothesis *) + | Some (name, Cic.Decl ty) -> + ProofEngineHelpers.pattern_of ~term:ty [term] + | Some (name, Cic.Def (bo, _)) -> + ProofEngineHelpers.pattern_of ~term:bo [term]) + with Failure _ | Invalid_argument _ -> + ProofEngineHelpers.pattern_of ~term:conclusion [term] + + method private get_cic_info id = + match self#cic_info with + | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> info, unsh_sequent + | Some ((None, _, _, _, _, _) as info) -> + let t = self#find_obj_conclusion id in + info, (~-1, [], t) (* dummy sequent for obj *) + | None -> assert false + + method private sequent_of_id ~(paste_kind:paste_kind) id = + let cic_info, unsh_sequent = self#get_cic_info id in let cic_sequent = match self#get_term_by_id cic_info id with - | `Term t -> - let context' = - match ProofEngineHelpers.locate_in_conjecture t unsh_sequent with - [context,_] -> context - | _ -> -(* prerr_endline (sprintf "%d\nt=%s\ncontext=%s" - (List.length l) (CicPp.ppterm t) (CicPp.ppcontext context)); *) - assert false (* since it uses physical equality *) - in - ~-1, context', t - | `Hyp context -> ~-1, context, Cic.Rel 1 - in - string_of_cic_sequent cic_sequent - - method string_of_selections = - List.map self#string_of_node (List.rev self#get_selections) - - method string_of_selection = + | SelTerm (t, _father_hyp) -> + let occurrences = + ProofEngineHelpers.locate_in_conjecture t unsh_sequent in + (match occurrences with + | [ context, _t ] -> + (match paste_kind with + | `Term -> ~-1, context, t + | `Pattern -> ~-1, [], self#pattern_of t context unsh_sequent) + | _ -> + HLog.error (sprintf "found %d occurrences while 1 was expected" + (List.length occurrences)); + assert false) (* since it uses physical equality *) + | SelHyp (_name, context) -> ~-1, context, Cic.Rel 1 in + cic_sequent + + method private string_of_selection ~(paste_kind:paste_kind) = match self#get_selections with | [] -> None - | node :: _ -> Some (self#string_of_node node) + | node :: _ -> Some (self#string_of_node ~paste_kind node) + + method has_selection = self#get_selections <> [] + + (** @return an associative list format -> string with all possible selection + * formats. Rationale: in order to convert the selection to TERM or PATTERN + * format we need the sequent, the metasenv, ... keeping all of them in a + * closure would be more expensive than keeping their already converted + * forms *) + method strings_of_selection = + try + let misc = self#coerce#misc in + List.iter + (fun target -> misc#add_selection_target ~target Gdk.Atom.clipboard) + [ "TERM"; "PATTERN"; "STRING" ]; + ignore (misc#grab_selection Gdk.Atom.clipboard); + List.map + (fun paste_kind -> + paste_kind, HExtlib.unopt (self#string_of_selection ~paste_kind)) + [ `Term; `Pattern ] + with Failure _ -> failwith "no selection" end @@ -397,7 +492,7 @@ object (self) ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in - MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); + HLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement @@ -417,7 +512,7 @@ object (self) self#thaw | _ -> let name = "cic_browser.xml" in - MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); + HLog.debug ("cic_browser: dumping MathML to ./" ^ name); ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); @@ -465,6 +560,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = notebook#append_page logo_with_qed method reset = + cicMathView#remove_selections; (match scrolledWin with | Some w -> (* removing page from the notebook will destroy all contained widget, @@ -487,7 +583,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal ~-1; method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } = - let sequents_no = List.length metasenv in _metasenv <- metasenv; pages <- 0; let win goal_switch = @@ -613,7 +708,7 @@ let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = - [ `Ast of DisambiguateTypes.term + [ `Ast of CicNotationPt.term | `Cic of Cic.term * Cic.metasenv | `String of string ] @@ -621,7 +716,6 @@ type term_source = class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = - let term_RE = Pcre.regexp "^term:(.*)" in let whelp_RE = Pcre.regexp "^\\s*whelp" in let uri_RE = Pcre.regexp @@ -629,8 +723,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in - let trailing_slash_RE = Pcre.regexp "/$" in - let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" 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 @@ -808,7 +900,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadCheck term = failwith "not implemented _loadCheck"; - self#_showMath +(* self#_showMath *) method private egg () = win#mathOrListNotebook#goto_page 2; @@ -816,7 +908,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private home () = self#_showMath; - match self#script#status.proof_status with + match self#script#grafite_status.proof_status with | Proof (uri, metasenv, bo, ty) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in @@ -849,7 +941,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadList l method private setEntry entry = - win#browserUri#entry#set_text (string_of_entry entry); + win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry); current_entry <- entry method private _loadObj obj = @@ -892,10 +984,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt)) | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt) | txt -> - (try - entry_of_string txt + (try + MatitaTypes.entry_of_string txt with Invalid_argument _ -> - command_error (sprintf "unsupported uri: %s" txt)) + raise + (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt))) in self#_load entry; self#_historyAdd entry @@ -968,7 +1061,7 @@ let mathViewer () = end let refresh_all_browsers () = - List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers + List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; @@ -978,20 +1071,34 @@ let get_math_views () = ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView) :: (List.map (fun b -> b#mathView) !cicBrowsers) -let get_selections () = - if (MatitaScript.current ())#onGoingProof () then - let rec aux = - function - | [] -> None - | mv :: tl -> - (match mv#string_of_selections with - | [] -> aux tl - | sels -> Some sels) - in - aux (get_math_views ()) - else - None - -let reset_selections () = - List.iter (fun mv -> mv#remove_selections) (get_math_views ()) +let find_selection_owner () = + let rec aux = + function + | [] -> raise Not_found + | mv :: tl -> + (match mv#get_selections with + | [] -> aux tl + | sel :: _ -> mv) + in + aux (get_math_views ()) + +let has_selection () = + try ignore (find_selection_owner ()); true + with Not_found -> false + +let math_view_clipboard = ref None (* associative list target -> string *) +let has_clipboard () = !math_view_clipboard <> None +let empty_clipboard () = math_view_clipboard := None + +let copy_selection () = + try + math_view_clipboard := + Some ((find_selection_owner ())#strings_of_selection) + with Not_found -> failwith "no selection" + +let paste_clipboard paste_kind = + match !math_view_clipboard with + | None -> failwith "empty clipboard" + | Some cb -> + (try List.assoc paste_kind cb with Not_found -> assert false)