diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-07 15:16:30 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-07 15:16:30 +0000 |
commit | 8a257c7d5f10cd7939611c7bb10be5415f4cc887 (patch) | |
tree | 500d60aee06d32c1307abba63c287532466709c5 /ide/coq_lex.mll | |
parent | 9d02da1c3d31c7599c7da3421f928d5aa9a5e816 (diff) |
Coqide understand { and }
It doesn't use them for indenting.
Worst, the undo around "End ..." bug leaks on '}' !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14267 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_lex.mll')
-rw-r--r-- | ide/coq_lex.mll | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 2ce8777c3..51e0610bc 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -83,6 +83,8 @@ let ident = firstchar identchar* let sentence_sep = '.' [ ' ' '\r' '\n' '\t' ] +let undotted_command = [ '{' '}' ] + let multiword_declaration = "Module" (space+ "Type")? | "Program" space+ ident @@ -185,6 +187,13 @@ and sentence stamp = parse sentence stamp lexbuf } | ".." | _ { sentence stamp lexbuf} + | undotted_command space? { (* the space? here is a awful consequence of + the way lexing is asked by Coqide.split_slice_lax: + a training whitespace is add at the end of text + and then dropped. This space has consequently to be + part of the sentence *) + if not !start then sentence stamp lexbuf (* in the middle of a command our token + aren't command *)} | sentence_sep { } | eof { raise Not_found } |