aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqOps.ml26
-rw-r--r--ide/ide.mllib1
-rw-r--r--ide/session.ml3
-rw-r--r--ide/wg_Tooltip.ml54
-rw-r--r--ide/wg_Tooltip.mli14
-rw-r--r--interp/constrintern.ml21
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/interface.mli1
-rw-r--r--lib/lib.mllib1
-rw-r--r--lib/serialize.ml27
10 files changed, 143 insertions, 6 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index d136833d0..15ca34b2f 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 45627ea26..fde206732 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 4e95fefca..46780b275 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 000000000..f85792a4e
--- /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 000000000..756814dc9
--- /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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d25bc1d9..4e63b16fa 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -670,8 +670,27 @@ let check_no_explicitation l =
| (_, Some (loc, _)) :: _ ->
user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
+(* This code is taken from dumpglob, and should be shared with it *)
+let feedback_global loc ref =
+ if !Flags.ide_slave then
+ let remove_sections dir =
+ if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+ Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
+ else
+ dir in
+ let sp = Nametab.path_of_global ref in
+ let lib_dp = Lib.library_part ref in
+ let ty = "" in
+ let mod_dp,id = Libnames.repr_path sp in
+ let mod_dp = remove_sections mod_dp in
+ let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+ let filepath = Names.DirPath.to_string lib_dp in
+ let modpath = Names.DirPath.to_string mod_dp_trunc in
+ let ident = Names.Id.to_string id in
+ Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty))
+
let dump_extended_global loc = function
- | TrueGlobal ref -> Dumpglob.add_glob loc ref
+ | TrueGlobal ref -> feedback_global loc ref; Dumpglob.add_glob loc ref
| SynDef sp -> Dumpglob.add_glob_kn loc sp
let intern_extended_global_of_qualid (loc,qid) =
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9667df31c..a9b596b99 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -15,6 +15,7 @@ CList
CString
CArray
Util
+Loc
Serialize
Xml_utils
Flags
diff --git a/lib/interface.mli b/lib/interface.mli
index 3ff05f6f2..e1419da9b 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -123,6 +123,7 @@ type edit_id = int
type feedback_content =
| AddedAxiom
| Processed
+ | GlobRef of Loc.t * string * string * string * string
type feedback = {
edit_id : edit_id;
diff --git a/lib/lib.mllib b/lib/lib.mllib
index eb7285bdd..eabac2cfd 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
Xml_lexer
Xml_parser
-Loc
Errors
Bigint
Dyn
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 823f4245d..186c3dc89 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -525,15 +525,42 @@ let is_message = function
| Element ("message", _, _) -> true
| _ -> false
+let of_loc loc =
+ let start, stop = Loc.unloc loc in
+ Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
+
+let to_loc xml = match xml with
+| Element ("loc", l,[]) ->
+ (try
+ let start = List.assoc "start" l in
+ let stop = List.assoc "stop" l in
+ Loc.make_loc (int_of_string start, int_of_string stop)
+ with Not_found | Invalid_argument _ -> raise Marshal_error)
+| _ -> raise Marshal_error
+
let to_feedback_content xml = do_match xml "feedback_content"
(fun s args -> match s with
| "addedaxiom" -> AddedAxiom
| "processed" -> Processed
+ | "globref" ->
+ (match args with
+ | [loc; filepath; modpath; ident; ty] ->
+ GlobRef(to_loc loc, to_string filepath, to_string modpath,
+ to_string ident, to_string ty)
+ | _ -> raise Marshal_error)
| _ -> raise Marshal_error)
let of_feedback_content = function
| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
| Processed -> constructor "feedback_content" "processed" []
+| GlobRef(loc, filepath, modpath, ident, ty) ->
+ constructor "feedback_content" "globref" [
+ of_loc loc;
+ of_string filepath;
+ of_string modpath;
+ of_string ident;
+ of_string ty
+ ]
let of_feedback msg =
let content = of_feedback_content msg.content in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 05:55:13 +0000