From 94ad539b17f1509540517ccdedefcda7cdd5fd4f Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Mon, 30 Sep 2013 16:10:02 +0000 Subject: CoqIDE: wg_Tooltip removed, new tooltip handling - tooltips are attached to sentences - to find the tooltip text one goes back until the first start of sentence mark, finds the corresponding sentence and displays the tooltip - focused editing does not invalidate tooltips this way, since the text, its tags and marks is moved around consistently git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16821 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqOps.ml | 52 +++++++++++++++++++++++++++++++++++++++++++---- ide/ide.mllib | 1 - ide/wg_Tooltip.ml | 59 ------------------------------------------------------ ide/wg_Tooltip.mli | 14 ------------- 4 files changed, 48 insertions(+), 78 deletions(-) delete mode 100644 ide/wg_Tooltip.ml delete mode 100644 ide/wg_Tooltip.mli (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1deb0a8ba..92b2a5e74 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -28,6 +28,7 @@ module SentenceId : sig start : GText.mark; stop : GText.mark; mutable flags : flag list; + mutable tooltips : (int * int * string lazy_t) list; edit_id : int; mutable state_id : Stateid.t option; } @@ -42,6 +43,8 @@ module SentenceId : sig val remove_flag : sentence -> mem_flag -> unit val same_sentence : sentence -> sentence -> bool val hidden_edit_id : unit -> int + val find_all_tooltips : sentence -> int -> string lazy_t list + val add_tooltip : sentence -> int -> int -> string lazy_t -> unit val dbg_to_string : GText.buffer -> sentence -> string @@ -51,6 +54,7 @@ end = struct start : GText.mark; stop : GText.mark; mutable flags : flag list; + mutable tooltips : (int * int * string lazy_t) list; edit_id : int; mutable state_id : Stateid.t option; } @@ -62,6 +66,7 @@ end = struct flags = flags; edit_id = !id; state_id = None; + tooltips = []; } let hidden_edit_id () = decr id; !id @@ -76,13 +81,18 @@ end = struct let remove_flag s mf = s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id + let find_all_tooltips s off = + CList.map_filter (fun (start,stop,t) -> + if start <= off && off <= stop then Some t else None) + s.tooltips + let add_tooltip s a b t = s.tooltips <- (a,b,t) :: s.tooltips let dbg_to_string (b : GText.buffer) s = let ellipsize s = Str.global_replace (Str.regexp "^[\n ]*") "" (if String.length s > 20 then String.sub s 0 17 ^ "..." else s) in - Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s]" + Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s] %s" s.edit_id (Stateid.to_string (Option.default Stateid.dummy s.state_id)) (b#get_iter_at_mark s.start)#offset @@ -90,6 +100,10 @@ end = struct (ellipsize ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop))) (String.concat "," (List.map str_of_flag s.flags)) + (ellipsize + (String.concat "," + (List.map (fun (a,b,t) -> + Printf.sprintf "<%d,%d> %s" a b (Lazy.force t)) s.tooltips))) end @@ -148,9 +162,37 @@ object(self) initializer Coq.set_feedback_handler _ct self#enqueue_feedback; - Wg_Tooltip.set_tooltip_callback (script :> GText.view); + script#misc#set_has_tooltip true; + ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback); feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback + method private tooltip_callback ~x ~y ~kbd tooltip = + let x, y = script#window_to_buffer_coords `WIDGET x y in + let iter = script#get_iter_at_location x y in + if iter#has_tag Tags.Script.tooltip then begin + let s = + let rec aux iter = + let marks = iter#marks in + if marks = [] then aux iter#backward_char + else + let mem_marks s = + List.exists (fun m -> + Gobject.get_oid m = + Gobject.get_oid (buffer#get_mark s.start)) marks in + try Stack.find mem_marks cmd_stack + with Not_found -> aux iter#backward_char in + aux iter in + let ss = + find_all_tooltips s + (iter#offset - (buffer#get_iter_at_mark s.start)#offset) in + let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in + GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON; + script#misc#set_tooltip_markup ("" ^ msg ^ "") + end else begin + script#misc#set_tooltip_text ""; script#misc#set_has_tooltip true + end; + false + method destroy () = feedback_timer.Ideutils.kill () @@ -266,7 +308,9 @@ object(self) let start = start_sentence#forward_chars pre in let stop = start_sentence#forward_chars post in let markup = lazy text in - Wg_Tooltip.apply_tooltip_tag buffer ~start ~stop ~markup + buffer#apply_tag Tags.Script.tooltip ~start ~stop; + add_tooltip sentence pre post markup; + self#print_stack method private is_dummy_id id = match id with @@ -549,7 +593,7 @@ object(self) " "^string_of_int stop#offset); buffer#remove_tag Tags.Script.processed ~start ~stop; buffer#remove_tag Tags.Script.unjustified ~start ~stop; -(* buffer#remove_tag Tags.Script.tooltip ~start ~stop; *) + buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") end; diff --git a/ide/ide.mllib b/ide/ide.mllib index 81e36763e..ce4fcca0d 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -19,7 +19,6 @@ Coq Coq_lex Sentence Gtk_parsing -Wg_Tooltip Wg_ProofView Wg_MessageView Wg_Find diff --git a/ide/wg_Tooltip.ml b/ide/wg_Tooltip.ml deleted file mode 100644 index 62598dd50..000000000 --- a/ide/wg_Tooltip.ml +++ /dev/null @@ -1,59 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0 - let overlap_interval (i1,i2 as x) (j1,j2 as y) = - in_interval i1 y || in_interval i2 y || in_interval j1 x - - let create () = ref [] - let add l i c = l := (i,c) :: !l - let remove_all l i = - l := List.filter (fun (j,_) -> not (overlap_interval i j)) !l - let find_all l x = - let res = - CList.map_filter - (fun (i,c) -> if in_interval x i then Some c else None) - !l - in - if res = [] then raise Not_found else res -end - -let table : string lazy_t Table.t = Table.create () - -let tooltip_callback (view : GText.view) ~x ~y ~kbd tooltip = - let x, y = view#window_to_buffer_coords `WIDGET x y in - let iter = view#get_iter_at_location x y in - if iter#has_tag Tags.Script.tooltip then begin - try - let ss = Table.find_all table iter#offset in - let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in - GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON; - view#misc#set_tooltip_markup ("" ^ msg ^ "") - with Not_found -> () - end else begin - view#misc#set_tooltip_text ""; view#misc#set_has_tooltip true - end; - false - -let remove_tag_callback tag ~start ~stop = - if tag#get_oid = Tags.Script.tooltip#get_oid then - Table.remove_all table (start#offset,stop#offset) - -let apply_tooltip_tag (buffer : GText.buffer) ~start ~stop ~markup = - Table.add table (start#offset,stop#offset) markup; - buffer#apply_tag Tags.Script.tooltip ~start ~stop - -let set_tooltip_callback view = - view#misc#set_has_tooltip true; - ignore(view#misc#connect#query_tooltip ~callback:(tooltip_callback view)); - ignore(view#buffer#connect#remove_tag ~callback:remove_tag_callback) - diff --git a/ide/wg_Tooltip.mli b/ide/wg_Tooltip.mli deleted file mode 100644 index 756814dc9..000000000 --- a/ide/wg_Tooltip.mli +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - start:GText.iter -> stop:GText.iter -> - markup:string lazy_t -> unit - -val set_tooltip_callback : GText.view -> unit -- cgit v1.2.3