package frama-c

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

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

let compare_prj (_p1, n1) (_p2, n2) =
  String.compare n1 n2

let projects_list ?(filter=fun _ -> true) () =
  let projects =
    Project.fold_on_projects
      (fun acc p ->
         if filter p then ((p, Project.get_unique_name p) :: acc) else acc)
      []
  in
  List.sort compare_prj projects

(* use the same order than the projects list.
   is not possible with an hashtbl.
   So we use a reference over a set of couple *)
module PrjRadiosSet =
  Set.Make
    (struct
      type t = (Project.t * string) * GButton.radio_button * GMenu.menu_item
      let compare (p1, _, _) (p2, _, _) = compare_prj p1 p2
    end)

let project_radios : PrjRadiosSet.t ref = ref PrjRadiosSet.empty

(** Create a new project *)
let new_project main_ui =
  Gtk_helper.source_files_chooser
    (main_ui :> Gtk_helper.source_files_chooser_host)
    []
    (fun filenames ->
       let project = Project.create "interactive" in
       let init () =
         Kernel.Files.set (List.map Datatype.Filepath.of_string filenames);
         File.init_from_cmdline ()
       in
       Project.on project init ();
       Project.set_current project)

let delete_project project =
  let name = Project.get_unique_name project in
  let ok =
    GToolbox.question_box
      ~title:(Format.sprintf "Deleting project %S" name)
      ~buttons:[ "Confirm"; "Cancel" ]
      (Format.sprintf "Do you want to destroy project %S?" name)
  in
  if ok = 1 then begin
    (try
       Project.remove ~project ()
     with Project.Cannot_remove _ ->
       let p = Project.create "default" in
       Project.on p File.init_from_cmdline ();
       try Project.remove () with Project.Cannot_remove _ -> assert false)
  end

module Filenames = Hashtbl.Make(Project)
let filenames : Filepath.Normalized.t Filenames.t = Filenames.create 7

let save_in
    (host_window: Design.main_window_extension_points) parent project name =
  try
    Project.save ~project name;
    Filenames.replace filenames project name
  with Project.IOError s ->
    host_window#error ~parent "Cannot save: %s" s

let save_project_as (main_ui: Design.main_window_extension_points) project =
  let dialog =
    GWindow.file_chooser_dialog
      ~action:`SAVE
      ~title:("Save project " ^ Project.get_unique_name project)
      ~parent:main_ui#main_window ()
  in
  (*dialog#set_do_overwrite_confirmation true ; only in later lablgtk2 *)
  dialog#add_button_stock `CANCEL `CANCEL ;
  dialog#add_select_button_stock `SAVE `SAVE ;
  main_ui#protect ~cancelable:true ~parent:(dialog :> GWindow.window_skel)
    (fun () ->
       match dialog#run () with
       | `SAVE ->
         Option.iter
           (save_in main_ui (dialog :> GWindow.window_skel) project)
           (Option.map Filepath.Normalized.of_string dialog#filename)
       | `DELETE_EVENT | `CANCEL -> ());
  dialog#destroy ()

let save_project (host_window: Design.main_window_extension_points) project =
  try
    save_in
      host_window
      (host_window#main_window :> GWindow.window_skel)
      project
      (Filenames.find filenames project)
  with Not_found ->
    save_project_as host_window project

let load_project (host_window: Design.main_window_extension_points) =
  let dialog = GWindow.file_chooser_dialog
      ~action:`OPEN
      ~title:"Load a saved project"
      ~parent:host_window#main_window ()
  in
  dialog#add_button_stock `CANCEL `CANCEL ;
  dialog#add_select_button_stock `OPEN `OPEN ;
  host_window#protect ~cancelable:true ~parent:(dialog:>GWindow.window_skel)
    (fun () -> match dialog#run () with
       | `OPEN ->
         begin match dialog#filename with
           | None -> ()
           | Some f ->
             (try ignore (Project.load (Filepath.Normalized.of_string f))
              with Project.IOError s | Failure s ->
                host_window#error
                  ~reset:true ~parent:(dialog:>GWindow.window_skel)
                  "Cannot load: %s" s)
         end
       | `DELETE_EVENT | `CANCEL -> ());
  dialog#destroy ()

let mk_project_markup p =
  let name = Extlib.html_escape (Project.get_unique_name p) in
  if Project.is_current p then "<b>" ^ name ^ "</b>" else name

let reset ?filter (menu: GMenu.menu) =
  (* Do not reset all if there is no change. *)
  let pl = projects_list ?filter () in
  let same_projects =
    (* use that project_radios and pl are sorted in the same way *)
    try
      let rest =
        PrjRadiosSet.fold
          (fun (p1, _, _) acc ->
             match acc with
             | [] -> raise Exit
             | p2 :: acc ->
               if compare_prj p1 p2 = 0 then acc else raise Exit)
          !project_radios
          pl
      in
      rest = []
    with Exit ->
      false
  in
  if same_projects then begin
    (* update the item status according to the current project anyway *)
    PrjRadiosSet.iter
      (fun ((p, _), r, i) ->
         r#set_active (Project.is_current p);
         let widgets = i#children in
         match widgets with
         | [ w ] ->
           (try
              let label = GMisc.label_cast w in
              label#set_label (mk_project_markup p);
              label#set_use_markup true
            with Gobject.Cannot_cast (t1,t2) ->
              Gui_parameters.warning
                "Child of project menu item of kind %s while %s was expected"
                t1 t2)
         | [] -> Gui_parameters.warning "Project menu item without child"
         | _ -> Gui_parameters.warning "Project menu item with %d child"
                  (List.length widgets)
      )
      !project_radios;
    false
  end else begin
    PrjRadiosSet.iter (fun (_, _, i) -> menu#remove i) !project_radios;
    project_radios := PrjRadiosSet.empty;
    true
  end

let duplicate_project project =
  ignore
    (Project.create_by_copy ~last:false ~src:project (Project.get_name project))

let rec rename_project
    (main_ui: Design.main_window_extension_points) menu project
  =
  let old = Project.get_unique_name project in
  let s =
    Gtk_helper.input_string
      ~parent:main_ui#main_window
      ~title:"Renaming project"
      (Format.sprintf "New name for project %S:" old)
  in
  (match s with
   | None -> ()
   | Some s ->
     try
       ignore (Project.from_unique_name s);
       main_ui#error "Project of name %S already exists" s
     with Project.Unknown_project ->
       Project.set_name project s);
  recompute main_ui menu

and mk_project_entry window menu ?group p =
  let pname = Project.get_unique_name p in
  let markup = mk_project_markup p in
  let item = GMenu.menu_item ~packing:menu#append () in
  let _label = GMisc.label ~markup ~xalign:0. ~packing:item#add () in
  let submenu = GMenu.menu ~packing:item#set_submenu () in
  let current = GMenu.menu_item ~packing:submenu#append () in
  let p_item = GButton.radio_button
      ?group
      ~active:(Project.is_current p)
      ~packing:current#add
      ~label:"Set current"
      ()
  in
  let callback () = Project.set_current p in
  ignore (current#connect#activate ~callback);
  project_radios := PrjRadiosSet.add ((p, pname), p_item, item) !project_radios;
  let add_action stock text callback =
    let image = GMisc.image ~xalign:0. ~stock () in
    let image = image#coerce in
    let item =
      Gtk_helper.image_menu_item ~image ~text ~packing:submenu#append
    in
    ignore (item#connect#activate ~callback)
  in
  add_action `COPY "Duplicate project"
    (fun () -> duplicate_project p);
  add_action `DELETE "Delete project" (fun () -> delete_project p);
  add_action `SAVE "Save project" (fun () -> save_project window p);
  add_action `SAVE_AS "Save project as" (fun () -> save_project_as window p);
  add_action
    `SELECT_FONT "Rename project" (fun () -> rename_project window menu p);
  p_item

and make_project_entries ?filter window menu =
  match projects_list ?filter () with
  | [] -> assert (filter <> None)
  | (pa, _name) :: tl ->
    let mk = mk_project_entry window menu in
    let pa_item = mk pa in
    let group = pa_item#group in
    List.iter (fun (pa, _) -> ignore (mk ~group pa)) tl

and recompute ?filter window menu =
  let is_reset = reset ?filter menu in
  if is_reset then make_project_entries ?filter window menu

open Menu_manager

(** Register this dialog in main window menu bar *)
let () =
  Design.register_extension
    (fun window ->
       let menu_manager = window#menu_manager () in
       let _item, menu = menu_manager#add_menu "_Project" in
       let constant_items =
         menu_manager#add_entries
           menu
           [
             menubar ~icon:`NEW "New project"
               (Unit_callback (fun () -> new_project window));
             menubar ~icon:`REVERT_TO_SAVED "Load project"
               (Unit_callback (fun () -> load_project window));
             menubar ~icon:`COPY "Duplicate current project"
               (Unit_callback
                  (fun () -> duplicate_project (Project.current())));
             menubar ~icon:`DELETE "Delete current project"
               (Unit_callback (fun () -> delete_project (Project.current ())));
             menubar ~icon:`SELECT_FONT "Rename current project"
               (Unit_callback
                  (fun () -> rename_project window menu (Project.current ())));
           ]
       in
       let new_item = constant_items.(0) in
       new_item#add_accelerator `CONTROL 'n';
       constant_items.(3)#add_accelerator `CONTROL 'd';
       ignore (GMenu.separator_item ~packing:menu#append ());
       let callback_prj _p = recompute window menu in
       let callback_rm_prj p =
         let filter p' = not (Project.equal p p') in
         recompute ~filter window menu
       in
       let hook () = recompute window menu in
       Project.register_create_hook callback_prj;
       Project.register_after_set_current_hook ~user_only:true callback_prj;
       Project.register_before_remove_hook callback_rm_prj;
       Project.register_after_load_hook hook;
       Project.register_after_global_load_hook hook;
       recompute window menu)

(*
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