summaryrefslogtreecommitdiff
path: root/ide/tags.ml
blob: c9b57af4cbd10edefc018e6689e2847737723c87 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)


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

(* These work fine for colorblind people too *)
let default_processed_color = "light green"
let default_processing_color = "light blue"
let default_error_color = "#FFCCCC"
let default_error_fg_color = "red"
let default_color = "cornsilk"

let processed_color = ref default_processed_color
let processing_color = ref default_processing_color
let error_color = ref default_error_color
let error_fg_color = ref default_error_fg_color

module Script =
struct
  let table = GText.tag_table ()
  let comment = make_tag table ~name:"comment" []
  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color]
  let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
  let incomplete = make_tag table ~name:"incomplete" [
          `BACKGROUND !processing_color;
          `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 all =
    [comment; error; error_bg; to_process; processed; incomplete; unjustified;
     found; sentence; tooltip]

  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
  
end
module Proof =
struct
  let table = GText.tag_table ()
  let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color]
  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"]
  let warning = make_tag table ~name:"warning" [`FOREGROUND "orange"]
  let item = make_tag table ~name:"item" [`WEIGHT `BOLD]
end

let string_of_color clr =
  let r = Gdk.Color.red clr in
  let g = Gdk.Color.green clr in
  let b = Gdk.Color.blue clr in
  Printf.sprintf "#%04X%04X%04X" r g b

let color_of_string s =
  let colormap = Gdk.Color.get_system_colormap () in
  Gdk.Color.alloc ~colormap (`NAME s)

let get_processed_color () = color_of_string !processed_color

let set_processed_color clr =
  let s = string_of_color clr in
  processed_color := s;
  Script.processed#set_property (`BACKGROUND s);
  Proof.highlight#set_property (`BACKGROUND s)

let get_processing_color () = color_of_string !processing_color

let set_processing_color clr =
  let s = string_of_color clr in
  processing_color := s;
  Script.incomplete#set_property (`BACKGROUND s);
  Script.to_process#set_property (`BACKGROUND s)

let get_error_color () = color_of_string !error_color

let set_error_color clr =
  let s = string_of_color clr in
  error_color := s;
  Script.error_bg#set_property (`BACKGROUND s)

let get_error_fg_color () = color_of_string !error_fg_color

let set_error_fg_color clr =
  let s = string_of_color clr in
  error_fg_color := s;
  Script.error#set_property (`FOREGROUND s)