aboutsummaryrefslogtreecommitdiff
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml9
1 files changed, 9 insertions, 0 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 52e184564f..689d4908f7 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -215,8 +215,17 @@ object(self)
document_length <- pred document_length;
segment#set_length document_length;
in
+ let on_click id =
+ let find _ _ s = Int.equal s.index id in
+ let sentence = Doc.find document find in
+ let mark = sentence.stop in
+ let iter = script#buffer#get_iter_at_mark mark in
+ script#buffer#place_cursor iter;
+ ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
+ in
let _ = (Doc.connect document)#pushed on_push in
let _ = (Doc.connect document)#popped on_pop in
+ let _ = segment#connect#clicked on_click in
()
method private tooltip_callback ~x ~y ~kbd tooltip =