diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 6b53e263444cf27c82f4f5753890e0711967d23d..23b95bce9a59a1f7347a36efbccaccb0e47cead2 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1523,8 +1523,11 @@ let _ = let () = Cmdline.run_after_configuring_stage (fun () -> + feedback "BEFORE Project.remove"; Remove_projects.iter (fun project -> Project.remove ~project ()); - Remove_projects.clear ()) + feedback "AFTER Project.remove"; + Remove_projects.unsafe_set Project.Datatype.Set.empty; + feedback "AFTER Clearing option") (* ************************************************************************* *) (** {2 Others options} *) diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml index 55280721f01c32fbc314ed7bc74e1571363aae86..f761614035b8976bbee565128f5f5fe31087c547 100644 --- a/src/libraries/project/project.ml +++ b/src/libraries/project/project.ml @@ -361,6 +361,9 @@ let journalized_set_current = let set_current ?(on=false) ?(selection=State_selection.full) p = if not (equal p (current ())) then journalized_set_current on selection p +let set_current_as_last_created () = + Extlib.may (fun p -> set_current p) !last_created_by_copy_ref + (** Indicates if we should keep [p] as the current project when calling {!on p}. *) let keep_current: bool ref = ref false diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli index d24b9b72f021aa85a77861a275c364da006b82cf..ec2f4d49c9be6e619e6cd6dc672ffe4a53f31c8e 100644 --- a/src/libraries/project/project.mli +++ b/src/libraries/project/project.mli @@ -142,6 +142,10 @@ val set_keep_current: bool -> unit of the current {!on}) iff [b] is [true]. @since Aluminium-20160501 *) +(**/**) +val set_current_as_last_created: unit -> unit +(**/**) + val copy: ?selection:State_selection.t -> ?src:t -> t -> unit (** Copy a project into another one. Default project for [src] is [current ()]. Replace the destination by [src]. diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml index bb11d8d56877746f7cea5b12005396ff6ddbeaad..d5693f4e0b969477c1b079cced18ade7adcee4f2 100644 --- a/src/plugins/gui/design.ml +++ b/src/plugins/gui/design.ml @@ -1863,7 +1863,9 @@ let toplevel play = Task.on_idle := (fun f -> ignore (Glib.Timeout.add ~ms:50 ~callback:f)); let project_name = Gui_parameters.Project_name.get () in - if project_name <> "" then + if project_name = "" then + Project.set_current_as_last_created () + else Project.set_current (Project.from_unique_name project_name); Ast.compute () with e -> (* An error occurred: we need to enforce the splash screen