diff options
| -rw-r--r-- | ide/coq_lex.mll | 5 | ||||
| -rw-r--r-- | ide/sentence.ml | 2 | ||||
| -rw-r--r-- | ide/tags.ml | 4 | ||||
| -rw-r--r-- | ide/tags.mli | 2 |
4 files changed, 5 insertions, 8 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index d1d7c66294..7eb0f28c87 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -45,10 +45,7 @@ and sentence initial stamp = parse match comment lexbuf with | None -> raise Unterminated | Some comm_last -> - (* A comment alone is a sentence. - A comment in a sentence doesn't terminate the sentence. - Note: comm_end is the position of the comment final ')' *) - if initial then stamp comm_last Tags.Script.comment_sentence; + stamp comm_last Tags.Script.comment; sentence initial stamp lexbuf } | "\"" { diff --git a/ide/sentence.ml b/ide/sentence.ml index 7b98d52964..7706c8d340 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -35,7 +35,7 @@ let rec backward_search cond (iter:GText.iter) = else backward_search cond iter#backward_char let is_sentence_end s = - s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence + s#has_tag Tags.Script.sentence let is_char s c = s#char = Char.code c diff --git a/ide/tags.ml b/ide/tags.ml index de3287720f..556430aafc 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -19,7 +19,7 @@ let processing_color = ref "light blue" module Script = struct let table = GText.tag_table () - let comment_sentence = make_tag table ~name:"comment_sentence" [] + let comment = make_tag table ~name:"comment" [] let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"] let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND "#FFCCCC"] let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color] @@ -30,7 +30,7 @@ struct let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) let all = - [comment_sentence; error; error_bg; to_process; processed; unjustified; + [comment; error; error_bg; to_process; processed; unjustified; found; sentence; tooltip] let edit_zone = diff --git a/ide/tags.mli b/ide/tags.mli index f79ae1f111..3c59002694 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -9,7 +9,7 @@ module Script : sig val table : GText.tag_table - val comment_sentence : GText.tag + val comment : GText.tag val error : GText.tag val error_bg : GText.tag val to_process : GText.tag |