package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file widget.ml

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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

class type t = Wutil.widget
class type widget = Wutil.widget

class type action =
  object
    inherit widget
    method set_tooltip : string -> unit
  end

class type ['a] signal =
  object
    method fire : 'a -> unit
    method set_enabled : bool -> unit
    method lock : (unit -> unit) -> unit
    method connect : ('a -> unit) -> unit
    method on_check : 'a -> (bool -> unit) -> unit
    method on_value : 'a -> (unit -> unit) -> unit
    method on_event : (unit -> unit) -> unit
  end

class type ['a] selector =
  object
    inherit ['a] signal
    method set : 'a -> unit
    method get : 'a
    method send : ('a -> unit) -> unit -> unit
  end

(* -------------------------------------------------------------------------- *)
(* ---  Labels                                                            --- *)
(* -------------------------------------------------------------------------- *)

open Wutil

type align = [`Left | `Right | `Center]
type style = [`Label | `Descr | `Code | `Title]
type color = [ GDraw.color | `NORMAL ]

let xalign = function `Left -> 0.0 | `Right -> 1.0 | `Center -> 0.5

class label ?(style=`Label) ?(align=`Left) ?width ?text () =
  let w = GMisc.label ?text ~xalign:(xalign align) () in
  object
    inherit Wutil.gobj_widget w
    val mutable fg = None
    val mutable bg = None

    method set_fg (c : color) =
      match fg , c with
      | None , `NORMAL -> ()
      | Some c0 , `NORMAL ->
        w#misc#modify_fg [ `NORMAL , `COLOR c0 ]
      | None , (#GDraw.color as c) ->
        fg <- Some (w#misc#style#fg `NORMAL) ;
        w#misc#modify_fg [ `NORMAL , c ]
      | Some _ , (#GDraw.color as c) ->
        w#misc#modify_fg [ `NORMAL , c ]

    method set_bg (c : color) =
      match bg , c with
      | None , `NORMAL -> ()
      | Some c0 , `NORMAL ->
        w#misc#modify_bg [ `NORMAL , `COLOR c0 ]
      | None , (#GDraw.color as c) ->
        bg <- Some (w#misc#style#bg `NORMAL) ;
        w#misc#modify_bg [ `NORMAL , c ]
      | Some _ , (#GDraw.color as c) ->
        w#misc#modify_bg [ `NORMAL , c ]

    initializer
      Wutil.on width w#set_width_chars ;
      match style with
      | `Label -> ()
      | `Code -> set_monospace w
      | `Title -> set_bold_font w
      | `Descr ->
        w#set_single_line_mode false ;
        w#set_line_wrap true ;
        w#set_justify `LEFT ;
        set_small_font w

    method set_text = w#set_text
    method set_tooltip msg =
      Wutil.set_tooltip w (if msg = "" then None else Some msg)
  end

(* -------------------------------------------------------------------------- *)
(* ---  Icons                                                             --- *)
(* -------------------------------------------------------------------------- *)

type icon = [ GtkStock.id | `Share of string | `None ]

let default_icon =
  let xpm =
    [| "12 12 2 1";
       ". c #ffffff";
       "# c #000000";
       "############";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "#..........#";
       "############"|]
  in once (fun () -> GdkPixbuf.from_xpm_data xpm)

let pixbufs = Hashtbl.create 63
let shared_icon (f:string) =
  try Hashtbl.find pixbufs f
  with Not_found ->
    let file = Printf.sprintf "%s/%s" !Wutil.share f in
    let pixbuf =
      try GdkPixbuf.from_file file
      with Glib.GError _ ->
        Wutil.warning "Icon '%s' not found" file ;
        default_icon ()
    in Hashtbl.add pixbufs f pixbuf ; pixbuf

let gimage = function
  | `None -> GMisc.image ()
  | `Share f -> GMisc.image ~pixbuf:(shared_icon f) ()
  | #GtkStock.id as stock -> GMisc.image ~stock ()

class image (icn:icon) =
  let img = gimage icn in
  object
    inherit gobj_widget img
    method set_icon (icn:icon) =
      match icn with
      | `None -> img#clear ()
      | `Share f -> img#set_pixbuf (shared_icon f)
      | #GtkStock.id as id -> img#set_stock id
  end

(* -------------------------------------------------------------------------- *)
(* ---  Buttons                                                           --- *)
(* -------------------------------------------------------------------------- *)

class button_skel ?align ?(icon=`None) ?tooltip (button:GButton.button_skel) =
  object(self)
    val mutable images = []
    initializer
      begin
        self#set_icon icon ;
        Wutil.on align (fun a -> button#set_xalign (xalign a)) ;
        set_tooltip button tooltip ;
        button#misc#set_can_focus false ;
        button#set_focus_on_click false ;
      end
    inherit gobj_action button
    method set_label = button#set_label
    method set_border e = button#set_relief (if e then `NORMAL else `NONE)
    method set_icon (i:icon) =
      match i with
      | `None -> button#unset_image ()
      | #icon as icn ->
        let image =
          try List.assoc icn images
          with Not_found ->
            let img = gimage icn in
            images <- (icn,img)::images ; img
        in button#set_image image#coerce
  end

class button ?align ?icon ?label ?(border=true) ?tooltip () =
  let relief = if border then `NORMAL else `NONE in
  let button = GButton.button ?label ~relief ~show:true () in
  object(self)
    inherit [unit] signal as s
    inherit! button_skel ?align ?icon ?tooltip (button :> GButton.button_skel) as b
    method! set_enabled e = s#set_enabled e ; b#set_enabled e
    method default = button#grab_default
    initializer
      ignore (button#connect#clicked ~callback:self#fire)
  end

(* -------------------------------------------------------------------------- *)
(* ---  On/Off Buttons                                                    --- *)
(* -------------------------------------------------------------------------- *)

class checkbox ~label ?tooltip () =
  let button = GButton.check_button ~label ~show:true () in
  object
    inherit [bool] selector false as s
    inherit! gobj_action button as b
    method! set_enabled e = s#set_enabled e ; b#set_enabled e
    method set_label l = button#set_label l
    method! set a = s#set a ; button#set_active a
    initializer
      begin
        set_tooltip button tooltip ;
        ignore (button#connect#clicked
                  ~callback:(fun () -> s#set button#active)) ;
      end
  end

let toggle_icon_warning = ref true

class toggle ?align ?icon ?label ?(border=true) ?tooltip () =
  let relief = if border then `NORMAL else `NONE in
  let button = GButton.toggle_button ?label ~relief ~show:true () in
  object
    inherit [bool] selector false as s
    inherit! button_skel ?align ?icon ?tooltip (button :> GButton.button_skel) as b
    method! set_enabled e = s#set_enabled e ; b#set_enabled e
    method! set = button#set_active
    method! set_icon icn =
      if icn <> `None && !toggle_icon_warning then
        ( Wutil.warning "[Widget] Icon may not appear on toggle buttons" ;
          toggle_icon_warning := false ) ;
      b#set_icon icn
    initializer
      ignore (button#connect#clicked ~callback:(fun () -> s#set button#active))
  end

class switch ?tooltip () =
  let pix_on = shared_icon "switch-on.png" in
  let pix_off = shared_icon "switch-off.png" in
  let evt = GBin.event_box () in
  let img = GMisc.image ~pixbuf:pix_on ~packing:evt#add () in
  object(self)
    inherit [bool] selector false as s
    inherit! gobj_action evt as b
    method! set_enabled e = s#set_enabled e ; b#set_enabled e
    method! set a = s#set a ; img#set_pixbuf (if a then pix_on else pix_off)
    initializer
      begin
        set_tooltip evt tooltip ;
        ignore (evt#event#connect#button_release
                  ~callback:(fun _evt -> self#set (not s#get) ; false)) ;
      end
  end

(* -------------------------------------------------------------------------- *)
(* ---  Button Group                                                      --- *)
(* -------------------------------------------------------------------------- *)

(* only used inside groups -> not exported to API *)
class radio_group ~label ?tooltip () =
  let button = GButton.radio_button ~label ~show:true () in
  object
    inherit [bool] selector false as s
    inherit! gobj_action button
    method! set e = s#set e ; if e then button#set_active true
    method group = function
      | None -> Some button#group
      | (Some g) as sg -> button#set_group g ; sg
    initializer
      begin
        set_tooltip button tooltip ;
        ignore (button#connect#clicked
                  ~callback:(fun () -> s#set button#active)) ;
      end
  end

(* only used inside groups -> not exported to API *)
class toggle_group ?label ?icon ?tooltip () =
  let button = GButton.button ?label ~show:true ~relief:`NONE () in
  object
    inherit [bool] selector false as s
    inherit! button_skel ?icon ?tooltip (button :> GButton.button_skel) as b
    method! set_enabled e = s#set_enabled e ; b#set_enabled e
    method! set a = s#set a ; button#set_relief (if a then `NORMAL else `NONE)
    initializer ignore (button#connect#clicked
                          ~callback:(fun () -> s#set (not s#get)))
  end

class ['a] group (default : 'a) =
  object(self)
    inherit ['a] selector default
    val mutable cases : (bool selector * 'a) list = []
    val mutable group = None
    initializer self#connect
        (fun v -> List.iter
            (fun (w,v0) -> w#set (v=v0)) cases)

    method private add_case (w : bool selector) (v : 'a) =
      begin
        w#set ( v = self#get ) ;
        w#connect (fun e -> if e then self#set v) ;
        cases <- (w,v) :: cases ;
      end

    method add_toggle ?label ?icon ?tooltip ~value () =
      let toggle = new toggle_group ?label ?icon ?tooltip () in
      self#add_case (toggle :> bool selector) value ;
      (toggle :> widget)

    method add_radio ~label ?tooltip ~value () =
      let radio = new radio_group ~label ?tooltip () in
      self#add_case (radio :> bool selector) value ;
      group <- radio#group group ;
      (radio :> widget)

    method! set_enabled e =
      List.iter (fun (w,_) -> w#set_enabled e) cases

  end

(* -------------------------------------------------------------------------- *)
(* ---  Spinner                                                           --- *)
(* -------------------------------------------------------------------------- *)

class spinner ?min ?max ?(step=1) ~value ?tooltip () =
  let b = GEdit.spin_button ~digits:0 () in
  object
    inherit [int] selector value as s
    inherit! gobj_action b
    method! set_enabled e = s#set_enabled e ; b#misc#set_sensitive e
    method! set a = s#set a ; b#set_value (float value)
    method set_min n = b#adjustment#set_bounds ~lower:(float n) ()
    method set_max n = b#adjustment#set_bounds ~upper:(float n) ()
    initializer
      begin
        set_tooltip b tooltip ;
        let fmap v = function None -> v | Some x -> float x in
        b#adjustment#set_bounds
          ~lower:(fmap (float min_int) min) ~upper:(fmap (float max_int) max)
          ~step_incr:(float step) () ;
        b#set_value (float value) ;
        let callback () = s#set b#value_as_int in
        ignore (b#connect#value_changed ~callback) ;
      end
  end

(* -------------------------------------------------------------------------- *)
(* ---  PopDown                                                           --- *)
(* -------------------------------------------------------------------------- *)

let render_options opt a =
  try List.assoc a opt
  with Not_found -> "<unknown>"

class ['a] menu ~default ?(options=[]) ?render ?items () =
  let strings = List.map snd options in
  let (cmb,(model,_)) as combo = GEdit.combo_box_text ~strings ~wrap_width:1 () in
  object(self)

    inherit gobj_action cmb as widget
    inherit! ['a] selector default as select

    initializer
      begin
        on render self#set_render ;
        on items self#set_items ;
      end

    val mutable printer = render_options options
    val mutable values = Array.of_list (List.map fst options)

    method set_options opt =
      printer <- render_options opt ;
      self#set_items (List.map fst opt)

    method set_render p = printer <- p

    method! set_enabled e =
      select#set_enabled e ; widget#set_enabled e

    method get_items = Array.to_list values

    method set_items xs =
      begin
        values <- Array.of_list xs ; model#clear () ;
        Array.iter (fun x -> GEdit.text_combo_add combo (printer x)) values ;
        let e = select#get in
        self#lock (fun () ->
            Array.iteri (fun i x -> if x=e then cmb#set_active i) values) ;
      end

    method private clicked n =
      if 0 <= n && n < Array.length values then
        select#set values.(n)

    method! set x =
      begin
        select#set x ;
        Array.iteri (fun i e -> if x=e then cmb#set_active i) values ;
      end

    initializer
      ignore (cmb#connect#notify_active ~callback:self#clicked)

  end

(* -------------------------------------------------------------------------- *)
(* ---  Popup Menu                                                        --- *)
(* -------------------------------------------------------------------------- *)

class popup () =
  let menu = GMenu.menu () in
  object

    val mutable empty = true
    val mutable separator = false

    method clear =
      begin
        List.iter menu#remove menu#children ;
        empty <- true ;
        separator <- false ;
      end

    method add_separator = separator <- true

    method add_item ~label ~callback =
      if not empty && separator then
        ignore (GMenu.separator_item ~packing:menu#append ());
      let item = GMenu.menu_item ~label ~packing:menu#append () in
      ignore (item#connect#activate ~callback) ;
      empty <- false ; separator <- false

    method run () =
      if not empty then
        let time = GMain.Event.get_current_time () in
        menu#popup ~button:3 ~time

  end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct