diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 26 | ||||
| -rw-r--r-- | ide/ide.mllib | 1 | ||||
| -rw-r--r-- | ide/session.ml | 3 | ||||
| -rw-r--r-- | ide/wg_Tooltip.ml | 54 | ||||
| -rw-r--r-- | ide/wg_Tooltip.mli | 14 |
5 files changed, 94 insertions, 4 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index d136833d00..15ca34b2fa 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -79,7 +79,8 @@ object(self) val cmd_stack = Stack.create () initializer - Coq.set_feedback_handler _ct self#process_feedback + Coq.set_feedback_handler _ct self#process_feedback; + Wg_Tooltip.set_tooltip_callback (script :> GText.view) method private get_start_of_input = buffer#get_iter_at_mark (`NAME "start_of_input") @@ -165,6 +166,18 @@ object(self) else Tags.Script.processed in buffer#apply_tag tag ~start ~stop + method private attach_tooltip sentence loc text = + let pre_chars, post_chars = Loc.unloc loc in + let start_sentence = buffer#get_iter_at_mark sentence.start in + let stop_sentence = buffer#get_iter_at_mark sentence.stop in + let phrase = start_sentence#get_slice ~stop:stop_sentence in + let pre = Ideutils.glib_utf8_pos_to_offset phrase ~off:pre_chars in + let post = Ideutils.glib_utf8_pos_to_offset phrase ~off:post_chars in + 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 + method private process_feedback msg = let id = msg.Interface.edit_id in if id = 0 || Stack.is_empty cmd_stack then () else @@ -176,8 +189,14 @@ object(self) set_flags sentence (CList.add_set `UNSAFE sentence.flags); self#mark_as_needed sentence | Interface.Processed, Some sentence -> self#mark_as_needed sentence - | _, None -> Minilib.log "Coqide/Coq is really asynchronous now!" - (* In this case we shoud look for (exec_)id into cmd_stack *) + | Interface.GlobRef(loc, filepath, modpath, ident, ty), Some sentence -> + self#attach_tooltip sentence loc + (Printf.sprintf "%s %s %s" filepath ident ty) + | _ -> + if sentence = None then + Minilib.log "Coqide/Coq is really asynchronous now!" + (* In this case we shoud look for (exec_)id into cmd_stack *) + else Minilib.log "Unsupported feedback message" method private commit_queue_transaction sentence = (* A queued command has been successfully done, we push it to [cmd_stack]. @@ -312,6 +331,7 @@ object(self) let stop = buffer#get_iter_at_mark stop_mark in 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#move_mark ~where:start (`NAME "start_of_input"); buffer#delete_mark start_mark; buffer#delete_mark stop_mark diff --git a/ide/ide.mllib b/ide/ide.mllib index 45627ea261..fde206732a 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -19,6 +19,7 @@ Coq Coq_lex Sentence Gtk_parsing +Wg_Tooltip Wg_ProofView Wg_MessageView Wg_Find diff --git a/ide/session.ml b/ide/session.ml index 4e95fefca3..46780b2757 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -101,7 +101,8 @@ let set_buffer_handlers buffer script = let () = buffer#move_mark (`NAME "prev_insert") ~where in let start = get_start () in let stop = buffer#end_iter in - buffer#remove_tag Tags.Script.error ~start ~stop + buffer#remove_tag Tags.Script.error ~start ~stop; + buffer#remove_tag Tags.Script.tooltip ~start ~stop in let end_action_cb () = let start = get_start () in diff --git a/ide/wg_Tooltip.ml b/ide/wg_Tooltip.ml new file mode 100644 index 0000000000..f85792a4ef --- /dev/null +++ b/ide/wg_Tooltip.ml @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This super inefficient thing should be an interval tree *) +module Table = struct + type 'a t = ((int * int) * 'a) list ref + + let in_interval x (i1,i2) = i1 - x <= 0 && i2 - x > 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 = + CList.map_filter (fun (i,c) -> if in_interval x i then Some c else None) !l +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 + view#misc#set_tooltip_text + (String.concat "\n" + (CList.uniquize (List.map Lazy.force ss))) + 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 new file mode 100644 index 0000000000..756814dc9b --- /dev/null +++ b/ide/wg_Tooltip.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val apply_tooltip_tag : + GText.buffer -> + start:GText.iter -> stop:GText.iter -> + markup:string lazy_t -> unit + +val set_tooltip_callback : GText.view -> unit |