diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:13 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:13 +0000 |
| commit | a936e9ae133f103ed9f781a7aa363c0006a2f178 (patch) | |
| tree | 6fc689fc24f3c8909dad28a46578dc9c3456f65d /ide/tags.ml | |
| parent | 2b9bc762ae31266212e7ab2defec7df41b08b6f8 (diff) | |
Coqide ported to STM
Main changes for STM:
1) protocol changed to carry edit/state ids
2) colouring reflects the actual status of every span (evaluated or not)
3) button to force the evaluation of the whole buffer
4) cmd_stack and backtracking completely changed to use state numbers
instead of counting sentences
5) feedback messages are completely asynchronous, and the whole protocol
could be made so with a minor effort, but there is little point in it
right now. Left as a future improvement. Missing bit: add
sentence-id to responses of interp command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/tags.ml')
| -rw-r--r-- | ide/tags.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/tags.ml b/ide/tags.ml index 9af54831f..e668616bf 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -21,6 +21,7 @@ struct let table = GText.tag_table () let comment_sentence = make_tag table ~name:"comment_sentence" [] 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 ;`EDITABLE false] let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold";`EDITABLE false] @@ -28,7 +29,7 @@ struct let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) let all = - [comment_sentence; error; to_process; processed; unjustified; + [comment_sentence; error; error_bg; to_process; processed; unjustified; found; sentence; tooltip] end module Proof = |