package frama-c

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

Source file menu_manager.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
(**************************************************************************)
(*                                                                        *)
(*  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 where =
  | Toolbar of GtkStock.id * string * string
  | Menubar of GtkStock.id option * string
  | ToolMenubar of GtkStock.id * string * string

type callback_state =
  | Unit_callback of (unit -> unit)
  | Bool_callback of (bool -> unit) * (unit -> bool)

type entry =
  { e_where: where;
    e_callback: callback_state;
    e_sensitive: unit -> bool }

let toolbar
    ?(sensitive=(fun _ -> true)) ~icon ~label ?(tooltip=label) callback =
  { e_where = Toolbar (icon, label, tooltip);
    e_callback = callback;
    e_sensitive = sensitive }

let menubar ?(sensitive=(fun _ -> true)) ?icon text callback =
  { e_where = Menubar (icon, text);
    e_callback = callback;
    e_sensitive = sensitive }

let toolmenubar
    ?(sensitive=(fun _ -> true)) ~icon ~label ?(tooltip=label) callback =
  { e_where = ToolMenubar (icon, label, tooltip);
    e_callback = callback;
    e_sensitive = sensitive }

type button_type =
  | BStandard of GButton.tool_button
  | BToggle of GButton.toggle_tool_button

let bt_type_as_skel = function
  | BStandard b -> (b :> GButton.tool_button_skel)
  | BToggle b -> (b :> GButton.tool_button_skel)

type menu_item_type =
  | MStandard of GMenu.menu_item
  | MCheck of GMenu.check_menu_item

let mitem_type_as_skel = function
  | MCheck m -> (m :> GMenu.menu_item_skel)
  | MStandard m -> (m :> GMenu.menu_item_skel)

class item ?menu ?menu_item ?button group = object (self)

  method menu_item =
    match menu_item with Some (MStandard m) -> Some m | _ -> None

  method check_menu_item =
    match menu_item with Some (MCheck m) -> Some m | _ -> None

  method menu_item_skel =
    match menu_item with Some m -> Some (mitem_type_as_skel m) | _ -> None

  method tool_button =
    match button with Some (BStandard b) -> Some b | _ -> None

  method toggle_tool_button =
    match button with Some (BToggle b) -> Some b | _ -> None

  method tool_button_skel =
    match button with Some b -> Some (bt_type_as_skel b) | None -> None

  method add_accelerator modifier c =
    Option.iter
      (fun (i : GMenu.menu_item_skel) ->
         i#add_accelerator
           ~group ~flags:[ `VISIBLE ] ~modi:[ modifier ] (int_of_char c))
      self#menu_item_skel

  method menu: GMenu.menu option = menu

end

(* the analyses-menu will be at the last position of the menubar *)
let add_submenu container ~pos label =
  let item =
    let packing item = container#insert item ~pos in
    GMenu.menu_item ~use_mnemonic:true ~packing ~label ()
  in
  let m = GMenu.menu () in
  item#set_submenu m;
  item, m

(*
external set_menu :  Obj.t -> unit = "ige_mac_menu_set_menu_bar"
*)

class menu_manager ?packing (_:Gtk_helper.host) =
  let menubar = GMenu.menu_bar ?packing () in
  (*  let () = set_menu (Obj.field (Obj.repr ((menubar)#as_widget)) 1) in *)
  let factory = new GMenu.factory menubar in
  let toolbar = GButton.toolbar ?packing () in
  object (self)

    val mutable first_tool_separator = None

    val analyses_menu = snd (add_submenu menubar ~pos:(-1) "_Analyses")

    val debug_item_and_menu = add_submenu menubar ~pos:(-1) "_Debug"
    val mutable debug_actions = []

    val mutable menubar_items = []
    val mutable toolbar_buttons = []
    val mutable set_active_states = []

    (** {2 API for plug-ins} *)

    method add_plugin ?title = self#add_entries ?title analyses_menu

    method add_debug ?title ?(show=fun () -> true) entries =
      let items = self#add_entries ?title (snd debug_item_and_menu) entries in
      let action item =
        if show () then begin
          Option.iter (fun i -> i#misc#show ()) item#menu_item;
          Option.iter (fun i -> i#misc#show ()) item#tool_button
        end else begin
          Option.iter (fun i -> i#misc#hide ()) item#menu_item;
          Option.iter (fun i -> i#misc#hide ()) item#tool_button
        end
      in
      let l = List.rev debug_actions in
      Array.iter
        (fun i ->
           action i;
           debug_actions <- (fun () -> action i) :: l)
        items;
      items

    (** {2 High-level API} *)

    method add_menu ?(pos=List.length menubar#children - 2) s =
      add_submenu ~pos factory#menu s

    method add_entries ?title ?pos container entries =
      (* Toolbar *)
      let toolbar_pos =
        (* The first group will be at the end of the toolbar.
           By default, add all the others just before this very first group. *)
        ref (match pos, first_tool_separator with
            | None, None -> 0
            | None, Some sep ->
              max
                0
                (toolbar#get_item_index (sep:>GButton.tool_item)#as_tool_item)
            | Some p, _ -> p)
      in
      let toolbar_packing w =
        toolbar#insert ~pos:!toolbar_pos w;
        incr toolbar_pos
      in
      let add_tool_separator () =
        if !toolbar_pos > 0 || first_tool_separator = None then begin
          let s = GButton.separator_tool_item ~packing:toolbar_packing () in
          match first_tool_separator with
          | None -> first_tool_separator <- Some s
          | Some _ -> ()
        end
      in
      let extra_tool_separator () = match pos with
        | Some 0 -> add_tool_separator ()
        | _ -> ()
      in
      let add_item_toolbar stock label tooltip callback sensitive =
(*
      let tooltip =
        try
          if (GtkStock.Item.lookup stock).GtkStock.label = "" then Some tooltip
          else None
        with Not_found -> Some tooltip
      in
*)
        let b = match callback with
          | Unit_callback callback ->
            let b = GButton.tool_button
                ~label:tooltip ~stock ~packing:toolbar_packing ()
            in
            b#set_label label;
            ignore (b#connect#clicked ~callback);
            BStandard b
          | Bool_callback (callback, active) ->
            let b = GButton.toggle_tool_button
                ~active:(active ()) ~label:tooltip ~stock
                ~packing:toolbar_packing ()
            in
            b#set_label tooltip;
            ignore (b#connect#toggled
                      ~callback:(fun () -> callback b#get_active));
            set_active_states <-
              (fun () -> b#set_active (active ())) :: set_active_states;
            BToggle b
        in
        (bt_type_as_skel b)#misc#set_tooltip_text tooltip;
        toolbar_buttons <- (b, sensitive) :: toolbar_buttons;
        b
      in
      (* Menubar *)
      let menu_pos = ref (match pos with None -> -1 | Some p -> p) in
      let container_packing w =
        container#insert ~pos:!menu_pos w;
        if !menu_pos <> -1 then incr menu_pos
      in
      let (!!) = Lazy.force in
      let menubar_packing, in_menu =
        let aux =
          lazy (* if [title] is not None, we want to create the submenu only once,
                  and late enough *)
            (match title with
             | None -> container_packing, container
             | Some s ->
               let sub = snd (add_submenu container ~pos:!menu_pos s) in
               (fun w -> sub#append w), sub
            )
        in
        lazy (fst !!aux), lazy (snd !!aux)
      in
      let add_menu_separator =
        fun () ->
          if !menu_pos > 0 || (!menu_pos = -1 && container#children <> []) then
            ignore (GMenu.separator_item ~packing:container_packing ())
      in
      let add_item_menu stock_opt label callback sensitive =
        let item = match stock_opt, callback with
          | None, Unit_callback callback ->
            let mi = GMenu.menu_item ~packing:!!menubar_packing ~label () in
            ignore (mi#connect#activate ~callback);
            MStandard mi
          | Some stock, Unit_callback callback ->
            let image = (GMisc.image ~stock ~xalign:0. () :> GObj.widget) in
            let text = label in
            let packing = !!menubar_packing in
            let mi = Gtk_helper.image_menu_item ~image ~text ~packing in
            ignore (mi#connect#activate ~callback);
            MStandard mi
          | _, Bool_callback (callback, active) ->
            let mi = GMenu.check_menu_item
                ~packing:!!menubar_packing ~label ~active:(active ()) ()
            in
            ignore (mi#connect#activate
                      ~callback:(fun () -> callback mi#active));
            set_active_states <-
              (fun () -> mi#set_active (active ())) :: set_active_states;
            MCheck mi
        in
        menubar_items <- (item, sensitive) :: menubar_items;
        item
      in
      let extra_menu_separator () = match pos with
        | Some 0 -> add_menu_separator ()
        | _ -> ()
      in
      (* Entries *)
      let add_item { e_where = kind; e_callback = callback; e_sensitive = sensitive} =
        match kind with
        | Toolbar(stock, label, tooltip) ->
          let button = add_item_toolbar stock label tooltip callback sensitive in
          new item ~button factory#accel_group
        | Menubar(stock_opt, label) ->
          let menu_item = add_item_menu stock_opt label callback sensitive in
          new item ~menu:!!in_menu ~menu_item factory#accel_group
        | ToolMenubar(stock, label, tooltip) ->
          let button = add_item_toolbar stock label tooltip callback sensitive in
          let menu_item = add_item_menu (Some stock) label callback sensitive in
          new item ~menu:!!in_menu ~menu_item ~button factory#accel_group
      in
      let edit_menubar =
        List.exists
          (function { e_where = Menubar _ | ToolMenubar _ } -> true | _ -> false)
          entries
      in
      let edit_toolbar =
        List.exists
          (function { e_where = Toolbar _ | ToolMenubar _ } -> true | _ -> false)
          entries
      in
      if edit_menubar then add_menu_separator ();
      if edit_toolbar then add_tool_separator ();
      let entries = List.map add_item entries in
      if edit_menubar then extra_menu_separator ();
      if edit_toolbar then extra_tool_separator ();
      Array.of_list entries

    method set_sensitive b =
      List.iter
        (fun (i, f) -> (bt_type_as_skel i)#misc#set_sensitive (b && f ()))
        toolbar_buttons;
      List.iter
        (fun (i, f) -> (mitem_type_as_skel i)#misc#set_sensitive (b && f()))
        menubar_items

    (** {2 Low-level API} *)

    method factory = factory
    method menubar = menubar
    method toolbar = toolbar

    method refresh () =
      List.iter
        (fun (i, f) -> (bt_type_as_skel i)#misc#set_sensitive (f ()))
        toolbar_buttons;
      List.iter
        (fun (i, f) -> (mitem_type_as_skel i)#misc#set_sensitive (f()))
        menubar_items;
      List.iter (fun f -> f ()) set_active_states;


    initializer
      let reset () =
        self#refresh ();
        List.iter (fun f -> f ()) debug_actions;
        let debug_item = fst debug_item_and_menu in
        if !Plugin.positive_debug_ref > 0 then debug_item#misc#show ()
        else debug_item#misc#hide ()
      in
      reset ();
      Boot.Main.extend reset

  end

(*
Local Variables:
compile-command: "make -C ../../.."
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