aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/tags.ml
diff options
context:
space:
mode:
authorGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-23 20:57:33 +0000
committerGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-23 20:57:33 +0000
commitcc0d671fa1f73e8984d9116b855e1c4a08cae6af (patch)
tree8925e6d801dffd66fe43967b19298e1bd290c961 /ide/tags.ml
parent8ea95ff47dcbad4f28a37dfd40882f4c83bcc49c (diff)
Ergonomy and robustness fix
Sentences are locked up to the period, and it's now possible to eval when there is no final whitespace. CoqIde will refuse to evaluate further if there is no whitespace, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/tags.ml')
-rw-r--r--ide/tags.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/tags.ml b/ide/tags.ml
index beb24071f..e78f5c822 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -33,7 +33,7 @@ struct
let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"]
let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"]
- let sentence_end = make_tag table ~name:"sentence_end" []
+ let lax_end = make_tag table ~name:"sentence_end" []
end
module Proof =
struct