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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
(************************************************************************)
(* 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 *)
(************************************************************************)
open Util
type color = GDraw.color
module Segment :
sig
type +'a t
val length : 'a t -> int
val resize : 'a t -> int -> 'a t
val empty : 'a t
val add : int -> 'a -> 'a t -> 'a t
val remove : int -> 'a t -> 'a t
val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
end =
struct
type 'a t = {
length : int;
content : 'a Int.Map.t;
}
let empty = { length = 0; content = Int.Map.empty }
let length s = s.length
let resize s len =
if s.length <= len then { s with length = len }
else
let filter i v = i < len in
{ length = len; content = Int.Map.filter filter s.content }
let add i v s =
if i < s.length then
{ s with content = Int.Map.add i v s.content }
else s
let remove i s = { s with content = Int.Map.remove i s.content }
let fold eq f s accu =
let make k v (cur, accu) = match cur with
| None -> Some (k, k, v), accu
| Some (i, j, w) ->
if k = j + 1 && eq v w then Some (i, k, w), accu
else Some (k, k, v), (i, j, w) :: accu
in
let p, segments = Int.Map.fold make s.content (None, []) in
let segments = match p with
| None -> segments
| Some p -> p :: segments
in
List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments
end
let i2f = float_of_int
let f2i = int_of_float
let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
| `BLACK, `BLACK -> true
| `COLOR c1, `COLOR c2 -> c1 == c2
| `NAME s1, `NAME s2 -> String.equal s1 s2
| `RGB (r1, g1, b1), `RGB (r2, g2, b2) -> r1 = r2 && g1 = g2 && b1 = b2
| `WHITE, `WHITE -> true
| _ -> false
class segment () =
let box = GBin.frame () in
let draw = GMisc.image ~packing:box#add () in
object (self)
inherit GObj.widget box#as_widget
val mutable width = 1
val mutable height = 20
val mutable data = Segment.empty
val mutable default : color = `WHITE
val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
initializer
box#misc#set_size_request ~height ();
let cb rect =
let w = rect.Gtk.width in
let h = rect.Gtk.height in
(** Only refresh when size actually changed, otherwise loops *)
if self#misc#visible && (width <> w || height <> h) then begin
width <- w;
height <- h;
self#redraw ();
end
in
let _ = box#misc#connect#size_allocate cb in
(** Initial pixmap *)
draw#set_pixmap pixmap
method length = Segment.length data
method set_length len =
data <- Segment.resize data len;
if self#misc#visible then self#refresh ()
method private fill_range color i j =
let i = i2f i in
let j = i2f j in
let width = i2f width in
let len = i2f (Segment.length data) in
let x = f2i ((i *. width) /. len) in
let x' = f2i ((j *. width) /. len) in
let w = x' - x in
pixmap#set_foreground color;
pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true ();
draw#set_mask None;
method add i color =
data <- Segment.add i color data;
if self#misc#visible then self#fill_range color i (i + 1)
method remove i =
data <- Segment.remove i data;
if self#misc#visible then self#fill_range default i (i + 1)
method set_default_color color = default <- color
method default_color = default
method private redraw () =
pixmap <- GDraw.pixmap ~width ~height ();
draw#set_pixmap pixmap;
self#refresh ();
method private refresh () =
pixmap#set_foreground default;
pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
let fold i j v () = self#fill_range v i (j + 1) in
Segment.fold color_eq fold data ();
draw#set_mask None;
end
|
