package frama-c

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

Source file wtable.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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

type ('a,'b) column =
  ?title:string -> 'b list -> ('a -> 'b list) -> GTree.view_column

class type virtual ['a] custom =
  object
    inherit ['a,'a,unit,unit] GTree.custom_tree_model
    method reload : unit
  end

class type ['a] columns =
  object
    method view : GTree.view
    (** the tree *)

    method scroll : GBin.scrolled_window
    (** scrolled tree (build on demand) *)

    method coerce : GObj.widget
    (** widget of the scroll *)

    method pack : (GObj.widget -> unit) -> unit
    (** packs the scroll *)

    method reload : unit
    (** Structure has changed *)

    method update_all : unit
    (** (only) Content of rows has changed *)

    method update_row : 'a -> unit
    method insert_row : 'a -> unit
    method set_focus : 'a -> GTree.view_column -> unit
    method on_click : ('a -> GTree.view_column -> unit) -> unit
    method on_right_click : ('a -> GTree.view_column -> unit) -> unit
    method on_double_click : ('a -> GTree.view_column -> unit) -> unit
    method set_selection_mode : Gtk.Tags.selection_mode -> unit
    method on_selection : (unit -> unit) -> unit
    method count_selected : int
    method iter_selected : ('a -> unit) -> unit
    method is_selected : 'a -> bool
    method add_column_text   : ('a,GTree.cell_properties_text) column
    method add_column_pixbuf : ('a,GTree.cell_properties_pixbuf) column
    method add_column_toggle : ('a,GTree.cell_properties_toggle) column
    method add_column_empty : GTree.view_column
    (** Add an empty column that always appears after the columns created
        by the other [add_column] methods. *)
  end

class type ['a] listmodel =
  object
    method reload : unit
    method size : int
    method index : 'a -> int
    method get : int -> 'a
  end

class type ['a] treemodel =
  object
    method reload : unit
    method has_child : 'a -> bool
    method children : 'a option -> int
    method child_at : 'a option -> int -> 'a
    method parent : 'a -> 'a option
    method index : 'a -> int
  end

(* -------------------------------------------------------------------------- *)
(* --- Columns                                                            --- *)
(* -------------------------------------------------------------------------- *)

let add_column (view:GTree.view) empty data ?title renderer render =
  begin
    let column = GTree.view_column ?title ~renderer:(renderer,[]) () in
    column#set_resizable true ;
    (* column#set_sizing `FIXED ;  *)
    column#set_cell_data_func renderer
      (fun model iter ->
         let props = match data (model#get_path iter) with
           | None -> []
           | Some e -> render e in
         renderer#set_properties props) ;
    ignore (view#append_column column);
    begin
      match empty with
      | None -> ()
      | Some e -> ignore (view#move_column e ~after:column)
    end ;
    column
  end

class ['a] makecolumns ?packing ?width ?height
    (view:GTree.view) (model : 'a #custom) =
  object(self)

    val mutable scroll = None

    initializer match packing with
      | Some packing -> self#pack packing
      | None -> ()

    method scroll =
      match scroll with
      | None ->
        let s = GBin.scrolled_window ?width ?height () in
        s#add view#coerce ; scroll <- Some s ; s
      | Some s -> s

    method pack packing = packing self#scroll#coerce
    method view = view
    method coerce = self#scroll#coerce

    method update_all = GtkBase.Widget.queue_draw view#as_tree_view

    method update_row x =
      try
        (*TODO : get the rectangle for raw and use queue_draw_area
          See  : http://www.gtkforums.com/viewtopic.php?t=1716
          Sadly this is not available in LablGtk2 yet...*)
        model#custom_row_changed (model#custom_get_path x) x
      with Not_found -> ()

    method insert_row x =
      try
        let path = model#custom_get_path x in
        model#custom_row_inserted path x
      with Not_found -> ()

    method reload =
      begin
        (* Delete all nodes in view *)
        let root = GTree.Path.create [0] in
        model#foreach
          (fun _p _i ->
             (* Do not use p since the path is changed by the call
                  to custom_row_deleted*)
             model#custom_row_deleted root;
             false) ;
        (* Then call model *)
        model#reload ;
      end

    method on_right_click f =
      let callback evt =
        let open GdkEvent in
        if Button.button evt = 3 then
          begin
            let x = int_of_float (Button.x evt) in
            let y = int_of_float (Button.y evt) in
            match view#get_path_at_pos ~x ~y with
            | Some (path,col,_,_) ->
              begin
                match model#custom_get_iter path with
                | None -> false
                | Some item ->
                  let () = f item col in false
              end
            | _ -> false
          end
        else false
      in ignore (view#event#connect#button_release ~callback)

    method on_click f =
      let callback () =
        match view#get_cursor () with
        | Some path , Some col ->
          begin
            match model#custom_get_iter path with
            | None -> ()
            | Some item -> f item col
          end
        | _ -> ()
      in ignore (view#connect#cursor_changed ~callback)

    method on_double_click f =
      let callback path col =
        match model#custom_get_iter path with
        | None -> ()
        | Some item -> f item col
      in ignore (view#connect#row_activated ~callback)

    method is_selected item =
      try view#selection#path_is_selected (model#custom_get_path item)
      with Not_found -> false

    method on_selection f =
      ignore (view#selection#connect#changed ~callback:f)

    method set_selection_mode = view#selection#set_mode

    method count_selected = view#selection#count_selected_rows

    method iter_selected f =
      List.iter
        (fun p ->
           match model#custom_get_iter p with
           | None -> ()
           | Some item -> f item)
        view#selection#get_selected_rows

    method set_focus item col =
      try
        let path = model#custom_get_path item in
        view#scroll_to_cell path col ;
        view#selection#select_path path ;
      with Not_found -> ()

    val mutable empty : GTree.view_column option = None

    method add_column_text ?title props render =
      let cell = GTree.cell_renderer_text props in
      add_column view empty model#custom_get_iter ?title cell render

    method add_column_pixbuf ?title props render =
      let cell = GTree.cell_renderer_pixbuf props in
      add_column view empty model#custom_get_iter ?title cell render

    method add_column_toggle ?title props render =
      let cell = GTree.cell_renderer_toggle props in
      add_column view empty model#custom_get_iter ?title cell render

    method add_column_empty =
      let column = GTree.view_column ~title:"" () in
      empty <- Some column ;
      ignore (view#append_column column);
      column

  end

(* -------------------------------------------------------------------------- *)
(* --- Gtk List Model                                                     --- *)
(* -------------------------------------------------------------------------- *)

class ['a] glist_model (m : 'a listmodel) =
  object
    method reload = m#reload
    inherit ['a,'a,unit,unit] GTree.custom_tree_model (new GTree.column_list)
    method! custom_flags = [`LIST_ONLY]
    method custom_decode_iter a () () = a
    method custom_encode_iter a = (a,(),())

    method custom_get_iter path =
      let idx:int array = GtkTree.TreePath.get_indices path in
      match idx with
      | [||] -> None
      | [|i|] -> (try let e = m#get i in
                    Some e
                  with Not_found -> None)
      | _ -> failwith "Invalid path of depth>1 in a list"

    method custom_get_path e =
      GtkTree.TreePath.create [m#index e]

    method custom_value (_:Gobject.g_type) (_:'a) ~column:_ =
      failwith "GwList: empty columns"

    method custom_iter_children e = match e with
      | None when (m#size > 0) ->
        Some(m#get 0)
      | _ ->
        None

    method custom_iter_has_child (_:'a) =
      false

    method custom_iter_n_children = function
      | Some _ -> failwith "GwList: no children"
      | None -> m#size

    method custom_iter_nth_child r k = match r with
      | Some _ -> failwith "GwList: no nth-child"
      | None ->
        if k < m#size then Some (m#get k) else None

    method custom_iter_parent (_:'a) = None

    method custom_iter_next e =
      let r =
        try
          let k = succ (m#index e) in
          if k < m#size then Some (m#get k) else None
        with Not_found -> None
      in
      r
  end

(* -------------------------------------------------------------------------- *)
(* --- Gtk List View                                                      --- *)
(* -------------------------------------------------------------------------- *)

class ['a] list
    ?packing ?width ?height
    ?(headers=true) ?(rules=true)
    (m : 'a listmodel) =
  let model = new glist_model m in
  let view = GTree.view ~model
      ~headers_visible:headers
      ~rules_hint:rules
      ~show:true () in
  object
    inherit ['a] makecolumns ?packing ?width ?height view model
  end

(* -------------------------------------------------------------------------- *)
(* --- Gtk Tree Model                                                     --- *)
(* -------------------------------------------------------------------------- *)

let rec get_iter m r idx k =
  if k >= Array.length idx then r else
    let a = m#child_at r idx.(k) in
    get_iter m (Some a) idx (succ k)

let rec get_path ks m a =
  let ks = m#index a :: ks in
  match m#parent a with
  | None -> ks
  | Some b -> get_path ks m b

class ['a] gtree_model (m : 'a treemodel) =
  object
    method reload = m#reload
    inherit ['a,'a,unit,unit] GTree.custom_tree_model (new GTree.column_list)
    method custom_decode_iter a () () = a
    method custom_encode_iter a = (a,(),())

    method custom_get_iter path =
      let idx = GtkTree.TreePath.get_indices path in
      if Array.length idx = 0 then None else
        let a = m#child_at None idx.(0) in
        get_iter m (Some a) idx 1

    method custom_get_path e =
      let ks = get_path [] m e in
      GtkTree.TreePath.create ks

    method custom_value (_:Gobject.g_type) (_:'a) ~column:(_:int) : Gobject.basic
      = Format.eprintf "Wtable.custom_value@." ; assert false

    method custom_iter_children r =
      let node = match r with None -> true | Some f -> m#has_child f in
      if node && m#children r > 0 then Some (m#child_at r 0) else None

    method custom_iter_has_child r =
      m#has_child r && m#children (Some r) > 0
    method custom_iter_n_children = m#children
    method custom_iter_nth_child r k =
      if k < m#children r then Some (m#child_at r k) else None
    method custom_iter_parent r = m#parent r
    method custom_iter_next e =
      let p = m#parent e in
      let k = succ (m#index e) in
      if k < m#children p then Some (m#child_at p k) else None

  end

(* -------------------------------------------------------------------------- *)
(* --- Gtk Tree View                                                      --- *)
(* -------------------------------------------------------------------------- *)

class ['a] tree
    ?packing ?width ?height
    ?(headers=true) ?(rules=true) (m : 'a treemodel) =
  let model = new gtree_model m in
  let view = GTree.view ~model
      ~headers_visible:headers
      ~rules_hint:rules
      ~show:true ()
  in
  object
    inherit ['a] makecolumns ?packing ?width ?height view model
  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