X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaMathView.ml;h=532c3dd975a3a2fe4d1364dca912273a51562fd0;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=b1970857ff4e53d23e71cbd3fc1a873e71a7cd7c;hpb=639131d311fd0f111e09feca7b567b28d21e873f;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index b1970857f..532c3dd97 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -100,10 +100,22 @@ let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types = | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) -> return_father id (mk_ids (ty :: bo :: inner_types)) | Cic.AConstant (_, _, _, None, ty, _, _) - | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids (ty::inner_types)) + | Cic.AVariable (_, _, None, ty, _, _) -> + return_father id (mk_ids (ty::inner_types)) | Cic.AInductiveDefinition _ -> assert false (* TODO *) + (** @return string content of a dom node having a single text child node, e.g. + * bool *) +let string_of_dom_node node = + match node#get_firstChild with + | None -> "" + | Some node -> + (try + let text = new Gdome.text_of_node node in + text#get_data#to_string + with GdomeInit.DOMCastException _ -> "") + class clickableMathView obj = let text_width = 80 in object (self) @@ -129,18 +141,15 @@ object (self) val mutable selection_changed = false method private selection_get_cb ctxt ~info ~time = -(* prerr_endline "selection_get_cb"; *) (match self#get_selections with | [] -> () | node :: _ -> ctxt#return (self#string_of_node node)) method private selection_clear_cb sel_event = -(* prerr_endline "selection_clear_cb"; *) self#remove_selections; false method private button_press_cb gdk_button = -(* prerr_endline "button_press_cb"; *) let button = GdkEvent.Button.button gdk_button in if button = left_button then begin button_press_x <- GdkEvent.Button.x gdk_button; @@ -151,7 +160,6 @@ object (self) false method private popup_contextual_menu time = -(* prerr_endline "popup_contextual_menu"; *) match self#string_of_selection with | None -> () | Some s -> @@ -214,18 +222,18 @@ object (self) 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 = + 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) + in let rec aux elt = if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds)#to_string <> "" -(* if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds - && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns - ~localName:xref_ds)#to_string <> "" *) - then begin - 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) - end else + then + set_selection elt + else try (match elt#get_parentNode with | None -> assert false @@ -233,6 +241,9 @@ object (self) with GdomeInit.DOMCastException _ -> () in (match gdome_elt with + | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns + ~localName:href_ds)#to_string <> "" -> + set_selection elt | Some elt -> aux elt | None -> self#set_selection None); selection_changed <- true @@ -261,6 +272,11 @@ object (self) (try Hashtbl.find ids_to_terms id with Not_found -> assert false) method private string_of_node node = + if node#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href_ds + then string_of_dom_node node + else self#string_of_id_node node + + method private string_of_id_node node = let get_id (node: Gdome.element) = let xref_attr = node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds @@ -387,9 +403,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = val mutable _metasenv = [] val mutable scrolledWin: GBin.scrolled_window option = None (* scrolled window to which the sequentViewer is currently attached *) - val logo = (GMisc.image ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") () :> GObj.widget) + val logo = (GMisc.image + ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") () + :> GObj.widget) - val logo_with_qed = (GMisc.image ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") () :> GObj.widget) + val logo_with_qed = (GMisc.image + ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") () + :> GObj.widget) method load_logo = notebook#set_show_tabs false; @@ -410,19 +430,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = w#remove cicMathView#coerce; scrolledWin <- None | None -> ()); - for i = 0 to pages do notebook#remove_page 0 done; + (match switch_page_callback with + | Some id -> + GtkSignal.disconnect notebook#as_widget id; + switch_page_callback <- None + | None -> ()); + for i = 0 to pages do notebook#remove_page 0 done; notebook#set_show_tabs true; pages <- 0; page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- []; + _metasenv <- []; self#script#setGoal ~-1; - (match switch_page_callback with - | Some id -> - GtkSignal.disconnect notebook#as_widget id; - switch_page_callback <- None - | None -> ()) method load_sequents (status: ProofEngineTypes.status) = let ((_, metasenv, _, _), goal) = status in @@ -432,7 +452,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal goal; let win metano = let w = - GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC + GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS ~shadow_type:`IN ~show:true () in let reparent () =