aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/tags.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-10-22 22:34:08 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-10-22 23:49:34 +0200
commit6171d9768a03734480233050aa58a6a776726c31 (patch)
tree8d63c5ede12a2ba42b97e047a9538d7149120855 /ide/tags.ml
parentd651d81a13d78f0466d2a08c06e7f2318c42da5f (diff)
Little code restructuration in CoqIDE tags.
- Removing tag "found" (unused since bd18c0821 "Now CoqIDE has a nice find & replace mechanism"). - Removing setting the priority of the debugging tag edit_zone: it was set at exactly the level it would have been by default minus 1, which is the level of tooltip, which have no associated visible markers, so the setting was a priori w/o effect. - For clarity, reorganizing order of tags into ephemere ones and non ephemere ones.
Diffstat (limited to 'ide/tags.ml')
-rw-r--r--ide/tags.ml22
1 files changed, 5 insertions, 17 deletions
diff --git a/ide/tags.ml b/ide/tags.ml
index d389cde30..402027179 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -17,32 +17,20 @@ module Script =
struct
(* More recently defined tags have highest priority in case of overlapping *)
let table = GText.tag_table ()
- let comment = make_tag table ~name:"comment" []
let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"]
let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
let error_bg = make_tag table ~name:"error_bg" []
let to_process = make_tag table ~name:"to_process" []
let processed = make_tag table ~name:"processed" []
- let incomplete = make_tag table ~name:"incomplete" [
- `BACKGROUND_STIPPLE_SET true;
- ]
+ let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true]
let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
- let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
- let sentence = make_tag table ~name:"sentence" []
let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
-
let ephemere =
[error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified]
-
- let all =
- comment :: found :: sentence :: ephemere
-
- let edit_zone =
- let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in
- t#set_priority (List.length all);
- t
- let all = edit_zone :: all
-
+ let comment = make_tag table ~name:"comment" []
+ let sentence = make_tag table ~name:"sentence" []
+ let edit_zone = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] (* for debugging *)
+ let all = edit_zone :: comment :: sentence :: ephemere
end
module Proof =
struct