From 6171d9768a03734480233050aa58a6a776726c31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 22 Oct 2017 22:34:08 +0200
Subject: 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.
---
 ide/tags.ml | 22 +++++-----------------
 1 file changed, 5 insertions(+), 17 deletions(-)

(limited to 'ide/tags.ml')

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
-- 
cgit v1.2.3