diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /ide/tags.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'ide/tags.ml')
-rw-r--r-- | ide/tags.ml | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/ide/tags.ml b/ide/tags.ml new file mode 100644 index 00000000..e78f5c82 --- /dev/null +++ b/ide/tags.ml @@ -0,0 +1,50 @@ + +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + + +let make_tag (tt:GText.tag_table) ~name prop = + let new_tag = GText.tag ~name () in + new_tag#set_properties prop; + tt#add new_tag#as_tag; + new_tag + +module Script = +struct + let table = GText.tag_table () + let kwd = make_tag table ~name:"kwd" [`FOREGROUND "blue"] + let qed = make_tag table ~name:"qed" [`FOREGROUND "blue"] + let decl = make_tag table ~name:"decl" [`FOREGROUND "orange red"] + let proof_decl = make_tag table ~name:"proof_decl" [`FOREGROUND "orange red"] + let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"] + let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"] + let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"] + let to_process = make_tag table ~name:"to_process" [`BACKGROUND "light blue" ;`EDITABLE false] + let processed = make_tag table ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false] + let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false] + let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] + let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false] + let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"] + let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"] + let lax_end = make_tag table ~name:"sentence_end" [] +end +module Proof = +struct + let table = GText.tag_table () + let highlight = make_tag table ~name:"highlight" [`BACKGROUND "light green"] + let hypothesis = make_tag table ~name:"hypothesis" [] + let goal = make_tag table ~name:"goal" [] +end +module Message = +struct + let table = GText.tag_table () + let error = make_tag table ~name:"error" [`FOREGROUND "red"] +end + |