aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-10 14:15:34 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-10 14:15:34 +0000
commit9045d41219334a037648731a5a9a162f5845f92b (patch)
tree51be97e11ee033392c35b4667bb86b353a60a503 /ide/session.ml
parent07089bf8337db9bfd0a9c1318580aff1d8823f43 (diff)
CoqIDE: error reporting fixed
Many things were wrong. Error tags were deleted by mistake, the screen was recentered on `INSERT using the wrong function (that cause some horizontal scrolling even if it was not needed), the cursor not advanced to the end of the wrong sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/session.ml')
-rw-r--r--ide/session.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/session.ml b/ide/session.ml
index 31e76935f..c42ed98da 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -179,8 +179,8 @@ let set_buffer_handlers
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
+ Sentence.tag_on_insert buffer
end;
- Sentence.tag_on_insert buffer
end in
let mark_deleted_cb m =
match GtkText.Mark.get_name m with