X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=e949020d93c65b7a3d7f4820859e4fe63fa91981;hb=4f04bf7d4032d301ce723fce357a27f92f003893;hp=1ad4b2cd10a79dd14348b67d157d4b4b7552beab;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1ad4b2cd1..e949020d9 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -25,8 +25,9 @@ open Printf -open MatitaTypes +open GrafiteTypes open MatitaGtkMisc +open MatitaGuiTypes module Stack = Continuationals.Stack @@ -62,9 +63,27 @@ let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in (distance < 4.) +let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" +let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" let href_ds = Gdome.domString "href" let xref_ds = Gdome.domString "xref" +let domImpl = Gdome.domImplementation () + + (** Gdome.element of a MathML document whose rendering should be blank. Used + * by cicBrowser to render "about:blank" document *) +let empty_mathml = lazy ( + domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None) + +let empty_boxml = lazy ( + domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) + ~qualifiedName:(Gdome.domString "box") ~doctype:None) + + (** shown for goals closed by side effects *) +let closed_goal_mathml = lazy ( + domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ()) + (* ids_to_terms should not be passed here, is just for debugging *) let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types = let find_parent id ids = @@ -143,12 +162,20 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = - (match self#get_selections with + match self#get_selections with | [] -> () - | node :: _ -> ctxt#return (self#string_of_node node)) + | node :: _ -> +(* eprintf "getting selection with target %s\n%!" ctxt#target; *) + (match ctxt#target with + | "PATTERN" -> + ctxt#return (self#string_of_node ~paste_kind:`Pattern node) + | "TERM" | _ -> + ctxt#return (self#string_of_node ~paste_kind:`Term node)) method private selection_clear_cb sel_event = +(* eprintf "selection clear\n%!"; *) self#remove_selections; + (GData.clipboard Gdk.Atom.clipboard)#clear (); false method private button_press_cb gdk_button = @@ -162,20 +189,18 @@ object (self) false 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 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 + let gui = get_gui () in + copy_menu_item#misc#set_sensitive gui#canCopy; + connect_menu_item copy_menu_item gui#copy; + 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 @@ -190,11 +215,11 @@ object (self) (match self#get_element_at x y with | None -> () | Some elt -> - let namespaceURI = DomMisc.xlink_ns in let localName = href_ds in - if elt#hasAttributeNS ~namespaceURI ~localName then + if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then self#invoke_href_callback - (elt#getAttributeNS ~namespaceURI ~localName)#to_string + (elt#getAttributeNS ~namespaceURI:xlink_ns + ~localName)#to_string gdk_button else ignore (self#action_toggle elt)); @@ -222,16 +247,14 @@ object (self) 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:DomMisc.helm_ns + if (elt#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds)#to_string <> "" then set_selection elt @@ -243,7 +266,7 @@ object (self) with GdomeInit.DOMCastException _ -> () in (match gdome_elt with - | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns + | Some elt when (elt#getAttributeNS ~namespaceURI:xlink_ns ~localName:href_ds)#to_string <> "" -> set_selection elt | Some elt -> aux elt @@ -252,13 +275,18 @@ object (self) method update_font_size = self#set_font_size !current_font_size - method private get_term_by_id context cic_info id = - let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in + method private get_term_by_id cic_info id = + let unsh_item, ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in try `Term (Hashtbl.find ids_to_terms id) 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 let context' = MatitaMisc.list_tl_at hyp context in `Hyp context' with Not_found -> assert false @@ -266,82 +294,128 @@ object (self) method private find_obj_conclusion id = match self#cic_info with | None - | Some (_, _, _, _, None) -> assert false - | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> + | Some (_, _, _, _, _, None) -> assert false + | Some (_, ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) -> let id = find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types in (try Hashtbl.find ids_to_terms id with Not_found -> assert false) - method private string_of_node node = - if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds - then self#string_of_id_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 ~paste_kind node else string_of_dom_node node - method private string_of_id_node node = + method private string_of_id_node ~(paste_kind:paste_kind) node = let get_id (node: Gdome.element) = let xref_attr = - node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + 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 let script = MatitaScript.current () in - let metasenv = script#proofMetasenv in - let context = script#proofContext in - let metasenv, context, conclusion = + let metasenv = if script#onGoingProof () then - script#proofMetasenv, script#proofContext, script#proofConclusion + script#proofMetasenv else - [], [], - let t = self#find_obj_conclusion id in - MatitaLog.debug (CicPp.ppterm t); - t - 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, _ = + 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 + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in - let pped_ast = CicNotationRew.pp_ast ast 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 in - let cic_info = - match self#cic_info with Some info -> info | None -> assert false + 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 + HLog.debug (CicPp.ppterm t); + info, (~-1, [], t) + | None -> assert false + in + let paste_as_pattern_sequent term unsh_sequent = + match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with + | [context, _] -> + (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 hyp *) + | Some (name, Cic.Decl ty) -> + let pattern = + ProofEngineHelpers.pattern_of ~term:ty [term] + in + HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern); + ~-1, [], pattern + | Some (name, Cic.Def (bo, _)) -> + let pattern = + ProofEngineHelpers.pattern_of ~term:bo [term] + in + HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern); + ~-1, [], pattern) + with Failure _ | Invalid_argument _ -> + let pattern = + ProofEngineHelpers.pattern_of ~term:conclusion [term] + in + HLog.debug ("\\vdash " ^ CicPp.ppterm pattern); + ~-1, [], pattern) + | _ -> assert false (* since it uses physical equality *) + in + let paste_as_term_sequent term unsh_sequent = + let context' = + match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with + | [context,_] -> context + | _ -> assert false (* since it uses physical equality *) + in + ~-1, context', term in let cic_sequent = - match self#get_term_by_id context cic_info id with + match self#get_term_by_id cic_info id with | `Term t -> - let context' = - match - ProofEngineHelpers.locate_in_conjecture t - (~-1, context, conclusion) - with - [context,_] -> context - | _ -> assert false (* since it uses physical equality *) - in - ~-1, context', t + (match paste_kind with + | `Term -> paste_as_term_sequent t unsh_sequent + | `Pattern -> paste_as_pattern_sequent t unsh_sequent) | `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 = + 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 @@ -361,15 +435,18 @@ object (self) method load_sequent metasenv metano = let sequent = CicUtil.lookup_meta metano metasenv in - let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) = + let (mathml, unsh_sequent, + (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) + = ApplyTransformation.mml_of_cic_sequent metasenv sequent in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, + (Some (Some unsh_sequent, + 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); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + HLog.debug ("load_sequent: dumping MathML to ./" ^ name); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement method load_object obj = @@ -380,7 +457,7 @@ object (self) ApplyTransformation.mml_of_cic_object obj in self#set_cic_info - (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); + (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); (match current_mathml with | Some current_mathml when use_diff -> self#freeze; @@ -388,8 +465,8 @@ object (self) self#thaw | _ -> let name = "cic_browser.xml" in - MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + 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); end @@ -436,6 +513,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, @@ -458,7 +536,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 = @@ -519,7 +596,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = let markup = match depth, pos with | 0, _ -> `Current (render_switch sw) - | 1, pos when Stack.head_tag stack = Stack.BranchTag -> + | 1, pos when Stack.head_tag stack = `BranchTag -> `Shift (pos, render_switch sw) | _ -> render_switch sw in @@ -538,7 +615,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = (match goal_switch with | Stack.Open goal -> cicMathView#load_sequent _metasenv goal | Stack.Closed goal -> - let doc = Lazy.force MatitaMisc.closed_goal_mathml in + let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); (try cicMathView#set_selection None; @@ -584,7 +661,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 ] @@ -592,7 +669,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 @@ -600,8 +676,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 @@ -643,7 +717,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) f () with exn -> if not (Helm_registry.get_bool "matita.debug") then - fail (MatitaExcPp.to_string exn) + fail (snd (MatitaExcPp.to_string exn)) else raise exn in let handle_error' f = (fun () -> handle_error (fun () -> f ())) in @@ -775,8 +849,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private blank () = self#_showMath; - mathView#load_root - (Lazy.force MatitaMisc.empty_mathml)#get_documentElement + mathView#load_root (Lazy.force empty_mathml)#get_documentElement method private _loadCheck term = failwith "not implemented _loadCheck"; @@ -821,7 +894,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 = @@ -864,10 +937,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 @@ -940,7 +1014,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; @@ -950,7 +1024,38 @@ let get_math_views () = ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView) :: (List.map (fun b -> b#mathView) !cicBrowsers) -let get_selections () = +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) + +(* let get_selections () = if (MatitaScript.current ())#onGoingProof () then let rec aux = function @@ -965,5 +1070,5 @@ let get_selections () = None let reset_selections () = - List.iter (fun mv -> mv#remove_selections) (get_math_views ()) + List.iter (fun mv -> mv#remove_selections) (get_math_views ()) *)