X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=07233700a29f15ae43da3e8f223f3652a18c39b4;hb=f740ba9bd597dad3d2edede01433fd31cbb79bb7;hp=cd3571ff4322aad73318565bc53e20a1de8003c9;hpb=ec5f1771cf795ce6186c5f0376ae248ed098d65a;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index cd3571ff4..07233700a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -27,18 +27,6 @@ open Printf open MatitaTypes -let list_map_fail f = - let rec aux = function - | [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Exit -> - (aux tl) - in - aux - let add_trailing_slash = let rex = Pcre.regexp "/$" in fun s -> @@ -57,6 +45,12 @@ object (self) end let cicBrowsers = ref [] +let gui_instance = ref None +let set_gui gui = gui_instance := Some gui +let get_gui () = + match !gui_instance with + | None -> assert false + | Some gui -> gui let default_font_size () = Helm_registry.get_opt_default Helm_registry.int @@ -66,21 +60,39 @@ let increase_font_size () = incr current_font_size let decrease_font_size () = decr current_font_size let reset_font_size () = current_font_size := default_font_size () + (* is there any lablgtk2 constant corresponding to the left mouse button??? *) +let left_button = 1 + +let near (x1, y1) (x2, y2) = + let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in + (distance < 4.) + +let href_ds = Gdome.domString "href" +let xref_ds = Gdome.domString "xref" + class clickableMathView obj = - let href = Gdome.domString "href" in - let xref = Gdome.domString "xref" in + let text_width = 80 in object (self) inherit GMathViewAux.multi_selection_math_view obj val mutable href_callback: (string -> unit) option = None method set_href_callback f = href_callback <- f + val mutable _cic_info = None + method private set_cic_info info = _cic_info <- info + method private cic_info = + match _cic_info with + | Some info -> info + | None -> assert false + initializer self#set_font_size !current_font_size; ignore (self#connect#selection_changed self#choose_selection); - ignore (self#connect#click (fun (gdome_elt, _, _, _) -> + ignore (self#event#connect#button_press self#button_press); + ignore (self#event#connect#button_release self#button_release); +(* ignore (self#connect#click (fun (gdome_elt, _, _, _) -> match gdome_elt with - | Some elt (* element is an hyperlink, use href_callback on it *) + | Some elt |+ element is an hyperlink, use href_callback on it +| when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> (match href_callback with | None -> () @@ -90,10 +102,72 @@ class clickableMathView obj = in f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) - | None -> ())) + | None -> ())) *) + + val mutable button_press_x = -1. + val mutable button_press_y = -1. + val mutable selection_changed = false + + method private button_press gdk_button = + if GdkEvent.Button.button gdk_button = left_button then begin + button_press_x <- GdkEvent.Button.x gdk_button; + button_press_y <- GdkEvent.Button.y gdk_button; + selection_changed <- false + end; + false + + method private button_release gdk_button = + 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 + (if near (button_press_x, button_press_y) + (button_release_x, button_release_y) + && not selection_changed + then + let x = int_of_float button_press_x in + let y = int_of_float button_press_y in + (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 + self#invoke_href_callback + (elt#getAttributeNS ~namespaceURI ~localName)#to_string + gdk_button + else + ignore (self#action_toggle elt))); + end; + false + + method private invoke_href_callback href_value gdk_button = + let button = GdkEvent.Button.button gdk_button in + if button = left_button then + let time = GdkEvent.Button.time gdk_button in + match href_callback with + | None -> () + | Some f -> + (match MatitaMisc.split href_value with + | [ uri ] -> f uri + | uris -> + let menu = GMenu.menu () in + List.iter + (fun uri -> + let menu_item = + GMenu.menu_item ~label:uri ~packing:menu#append () + in + ignore (menu_item#connect#activate (fun () -> f uri))) + uris; + menu#popup ~button ~time) + method private choose_selection gdome_elt = let rec aux elt = - if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then + 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 self#set_selection (Some elt) else try @@ -103,13 +177,74 @@ class clickableMathView obj = with GdomeInit.DOMCastException _ -> () (* debug_print "trying to select above the document root" *) in - match gdome_elt with + (match gdome_elt with | Some elt -> aux elt - | None -> self#set_selection None + | None -> self#set_selection None); + selection_changed <- true method update_font_size = self#set_font_size !current_font_size + + method private get_term_by_id context id = + let ids_to_terms, ids_to_hypotheses = self#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' = MatitaMisc.list_tl_at hyp context in + `Hyp context' + with Not_found -> assert false + method string_of_selected_terms = + let get_id (node: Gdome.element) = + let xref_attr = + node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + in + xref_attr#to_string + in + let script = MatitaScript.instance () in + let metasenv = script#proofMetasenv in + let context = script#proofContext in + let conclusion = script#proofConclusion in + let cic_terms = + List.map + (fun node -> self#get_term_by_id context (get_id node)) + self#get_selections + in +(* TODO: code for patterns + let conclusion = (MatitaScript.instance ())#proofConclusion in + let conclusion_pattern = + ProofEngineHelpers.pattern_of ~term:conclusion cic_terms + in +*) + let dummy_goal = ~-1 in + let cic_sequent = + match cic_terms with + | [] -> assert false + | `Term t :: _ -> + let context' = + ProofEngineHelpers.locate_in_conjecture t + (dummy_goal, context, conclusion) + in + dummy_goal, context', t + | `Hyp context :: _ -> dummy_goal, context, Cic.Rel 1 + in +(* TODO: code for patterns + (* TODO context shouldn't be empty *) + let cic_sequent = ~-1, [], conclusion_pattern 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 = + 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 + end let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = @@ -121,52 +256,15 @@ let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = [] class sequentViewer obj = - object(self) - - inherit clickableMathView obj +object (self) + inherit clickableMathView obj - val mutable current_infos = None - - method get_selected_terms = - let selections = self#get_selections in - list_map_fail - (fun node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:DomMisc.helm_ns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - | Some (ids_to_terms,_,_) -> - (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit) - | None -> assert false) (* "ERROR: No current term!!!" *) - selections - - method get_selected_hypotheses = - let selections = self#get_selections in - list_map_fail - (fun node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:DomMisc.helm_ns - ~localName:(Gdome.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match current_infos with - | Some (_,_,ids_to_hypotheses) -> - (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit) - | None -> assert false) (* "ERROR: No current term!!!" *) - selections - 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, (_, (ids_to_terms, _, ids_to_hypotheses,_ ))) = ApplyTransformation.mml_of_cic_sequent metasenv sequent in - current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); + self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses)); let name = "sequent_viewer.xml" in prerr_endline ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); @@ -227,7 +325,14 @@ class sequentsViewer ~(notebook:GPack.notebook) scrolledWin <- Some w; match sequentViewer#misc#parent with | None -> w#add sequentViewer#coerce - | Some _ -> sequentViewer#misc#reparent w#coerce + | Some parent -> + let parent = + match sequentViewer#misc#parent with + None -> assert false + | Some p -> GContainer.cast_container p + in + parent#remove sequentViewer#coerce; + w#add sequentViewer#coerce in goal2win <- (metano, reparent) :: goal2win; w#coerce @@ -328,8 +433,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 - let gui = MatitaGui.instance () in - let win = gui#newBrowserWin () in + let gui = get_gui () in + let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in let combo,_ = GEdit.combo_box_text ~strings:queries () in let activate_combo_query input q = @@ -543,12 +648,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * if the widget is not mapped (hidden by the notebook) * the document is not rendered *) let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) - let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, - ids_to_hypotheses,_,_))) = + let (mathml, (_,((ids_to_terms, ids_to_father_ids, ids_to_conjectures, + ids_to_hypotheses, ids_to_inner_sorts, ids_to_inner_types) as info))) + = ApplyTransformation.mml_of_cic_object obj in - current_infos <- Some (ids_to_terms, ids_to_father_ids, - ids_to_conjectures, ids_to_hypotheses); + current_infos <- Some info; (match current_mathml with | Some current_mathml when use_diff -> mathView#freeze; @@ -649,7 +754,7 @@ let default_sequentViewer () = sequentViewer ~show:true () let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer let default_sequentsViewer () = - let gui = MatitaGui.instance () in + let gui = get_gui () in let sequentViewer = sequentViewer_instance () in sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer