From cfd919846d9e9c437a017f67ea1993eff7ea8ee9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 08:38:28 +0000 Subject: [PATCH] proof of concept implementation of cut and paste from gtkMathView to text (still via debug menu item "print selected terms") --- helm/matita/matita.ml | 12 +- helm/matita/matitaMathView.ml | 198 +++++++++++++++++++-------------- helm/matita/matitaMathView.mli | 12 +- 3 files changed, 127 insertions(+), 95 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index aae334abd..9207b1c05 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -44,7 +44,6 @@ let _ = MatitaDb.create_owner_environment (); MatitamakeLib.initialize (); GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) - prerr_endline BuildTimeConf.gtkmathview_conf; GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; ignore (GMain.Main.init ()); CicEnvironment.set_trust (* environment trust *) @@ -113,7 +112,8 @@ let _ = let sequent_viewer = MatitaMathView.sequentViewer_instance () in let sequents_viewer = MatitaMathView.sequentsViewer_instance () in sequent_viewer#set_href_callback - (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri)))); + (Some (fun uri -> (MatitaMathView.cicBrowser ())#load + (`Uri (UriManager.uri_of_string uri)))); let browser_observer _ = MatitaMathView.refresh_all_browsers () in let sequents_observer status = sequents_viewer#reset; @@ -159,12 +159,8 @@ let _ = prerr_endline (UriManager.string_of_uri u)) (CicEnvironment.list_obj ())); addDebugItem "print selected terms" (fun () -> - let i = ref 0 in - List.iter - (fun t -> - incr i; - MatitaLog.debug (sprintf "%d: %s" !i (CicPp.ppterm t))) - (MatitaMathView.sequentViewer_instance ())#get_selected_terms); + let sequentViewer = MatitaMathView.sequentViewer_instance () in + MatitaLog.debug (sequentViewer#string_of_selected_terms)); addDebugItem "dump getter settings" (fun _ -> prerr_endline (Http_getter_env.env_to_string ())); addDebugItem "getter: getalluris" (fun _ -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index ee18823f5..5f0c77df5 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 -> @@ -73,15 +61,25 @@ 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); @@ -103,31 +101,38 @@ class clickableMathView obj = val mutable button_press_x = -1. val mutable button_press_y = -1. + val mutable selection_changed = false method private button_press gdk_button = - button_press_x <- GdkEvent.Button.x gdk_button; - button_press_y <- GdkEvent.Button.y 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 = - 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) - 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 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))); + 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 = @@ -152,7 +157,12 @@ class clickableMathView obj = 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 @@ -162,13 +172,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 = @@ -180,52 +251,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 ()); @@ -608,12 +642,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; diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 045555b80..3816a4b02 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -33,6 +33,8 @@ class type clickableMathView = (** set hyperlink callback. None disable hyperlink handling *) method set_href_callback: (string -> unit) option -> unit + method string_of_selected_terms: string + method update_font_size: unit end @@ -40,13 +42,13 @@ class type sequentViewer = object inherit clickableMathView - (** @return the list of selected terms. Selections which are not terms are - * ignored *) +(* |+* @return the list of selected terms. Selections which are not terms are + * ignored +| method get_selected_terms: Cic.term list - (** @return the list of selected hypothese. Selections which are not - * hypotheses are ignored *) - method get_selected_hypotheses: Cic.hypothesis list + |+* @return the list of selected hypothese. Selections which are not + * hypotheses are ignored +| + method get_selected_hypotheses: Cic.hypothesis list *) (** load a sequent and render it into parent widget *) method load_sequent: Cic.metasenv -> int -> unit -- 2.39.2