remove the checkboxes when the incremental analysis is disabled

reb-ddm · reb-ddm · commit 13166c2a3d7b · 2026-04-23T11:21:03.000+02:00
diff --git a/core/agents/kappaswitchman_mpi.ml b/core/agents/kappaswitchman_mpi.ml
@@ -141,7 +141,9 @@ let on_message exec_command message_delimiter =
                        Lwt.return (B (Nothing, msg_id, out))
                      | "FileUpdateWS" ->
                        let id =
-                         JsonUtil.read_next_item Yojson.Basic.read_string st b
+                         JsonUtil.read_next_item
+                           (JsonUtil.read_option Yojson.Basic.read_string)
+                           st b
                        in
                        manager#file_update_ws id >>= fun out ->
                        Lwt.return (B (Nothing, msg_id, out))
diff --git a/core/api/api.ml b/core/api/api.ml
@@ -37,7 +37,7 @@ class type virtual manager_model = object
   method file_create : int -> string -> string -> unit result Lwt.t
   method file_get : string -> (string * int) result Lwt.t
   method file_update : string -> string -> unit result Lwt.t
-  method file_update_ws : string -> unit result Lwt.t
+  method file_update_ws : string option -> unit result Lwt.t
   method file_move : int -> string -> unit result Lwt.t
   method file_delete : string -> unit result Lwt.t
 end
diff --git a/core/api/api.mli b/core/api/api.mli
@@ -33,7 +33,7 @@ class type virtual manager_model = object
   method file_create : int -> string -> string -> unit result Lwt.t
   method file_get : string -> (string * int) result Lwt.t
   method file_update : string -> string -> unit result Lwt.t
-  method file_update_ws : string -> unit result Lwt.t
+  method file_update_ws : string option -> unit result Lwt.t
   method file_move : int -> string -> unit result Lwt.t
   method file_delete : string -> unit result Lwt.t
 end
diff --git a/core/api/kamoha_client.ml b/core/api/kamoha_client.ml
@@ -110,7 +110,8 @@ class virtual new_client ~post mailbox : Api.manager_model =
           JsonUtil.write_sequence b
             [
               (fun b -> Yojson.Basic.write_string b "FileUpdateWS");
-              (fun b -> Yojson.Basic.write_string b file_id);
+              (fun b ->
+                JsonUtil.write_option Yojson.Basic.write_string b file_id);
             ])
 
     method file_move file_position file_id =
diff --git a/core/api/switchman_client.ml b/core/api/switchman_client.ml
@@ -240,7 +240,8 @@ class virtual new_client ~is_running ~post mailbox =
           JsonUtil.write_sequence b
             [
               (fun b -> Yojson.Basic.write_string b "FileUpdateWS");
-              (fun b -> Yojson.Basic.write_string b file_id);
+              (fun b ->
+                JsonUtil.write_option Yojson.Basic.write_string b file_id);
             ])
 
     method file_move file_position file_id =
diff --git a/core/api/switchman_client.mli b/core/api/switchman_client.mli
@@ -33,7 +33,7 @@ object
     string -> string -> (unit, Result_util.message list) Result_util.t Lwt.t
 
   method file_update_ws :
-    string -> (unit, Result_util.message list) Result_util.t Lwt.t
+    string option -> (unit, Result_util.message list) Result_util.t Lwt.t
 
   method get_constraints_list :
     ( (string * Public_data.agent list Public_data.lemma list) list,
diff --git a/core/grammar/kamoha_mpi.ml b/core/grammar/kamoha_mpi.ml
@@ -95,7 +95,9 @@ let on_message yield post =
                        Lwt.return (B (Nothing, msg_id, lift_answer out))
                      | "FileUpdateWS" ->
                        let id =
-                         JsonUtil.read_next_item Yojson.Basic.read_string st b
+                         JsonUtil.read_next_item
+                           (JsonUtil.read_option Yojson.Basic.read_string)
+                           st b
                        in
                        let out = Kfiles.file_set_working_set ~id catalog in
                        Lwt.return (B (Nothing, msg_id, lift_answer out))
diff --git a/core/grammar/kfiles.ml b/core/grammar/kfiles.ml
@@ -96,13 +96,19 @@ let file_patch ~id content catalog =
     Result.Ok ()
 
 let file_set_working_set ~id catalog =
-  match Hashtbl.find_all catalog.elements id with
-  | [] -> Result.Error ("Unknown file \"" ^ id ^ "\"")
-  | _ :: _ :: _ -> Result.Error "Serious problems in file catalog"
-  | [ { rank; _ } ] ->
-    let () = catalog.current_ws := Some rank in
+  match id with
+  | None ->
+    let () = catalog.current_ws := None in
     let () = catalog.ast := Empty in
     Result.Ok ()
+  | Some id ->
+    (match Hashtbl.find_all catalog.elements id with
+    | [] -> Result.Error ("Unknown file \"" ^ id ^ "\"")
+    | _ :: _ :: _ -> Result.Error "Serious problems in file catalog"
+    | [ { rank; _ } ] ->
+      let () = catalog.current_ws := Some rank in
+      let () = catalog.ast := Empty in
+      Result.Ok ())
 
 let file_delete ~id catalog =
   match Hashtbl.find_all catalog.elements id with
diff --git a/core/grammar/kfiles.mli b/core/grammar/kfiles.mli
@@ -26,7 +26,7 @@ val file_move :
 (** Fails if [position] is not available *)
 
 val file_patch : id:string -> string -> catalog -> (unit, string) Result.result
-val file_set_working_set : id:string -> catalog -> (unit, string) result
+val file_set_working_set : id:string option -> catalog -> (unit, string) result
 val file_delete : id:string -> catalog -> (unit, string) Result.result
 
 val file_get : id:string -> catalog -> (string * int, string) Result.result
diff --git a/gui/state/state_file.ml b/gui/state/state_file.ml
@@ -10,10 +10,24 @@ open Lwt.Infix
 
 type slot = { local: string option; name: string }
 type active = { rank: int; cursor_pos: Loc.position; out_of_sync: bool }
-type model = { current: active option; directory: slot Mods.IntMap.t }
+
+type model = {
+  current: active option;
+  directory: slot Mods.IntMap.t;
+  incremental: bool;
+}
 
 let dummy_cursor_pos = { Loc.line = -1; Loc.chr = 0 }
-let blank_state = { current = None; directory = Mods.IntMap.empty }
+
+let blank_state =
+  {
+    current = None;
+    directory = Mods.IntMap.empty;
+    incremental =
+      (React.S.value State_project.model).State_project.model_parameters
+        .State_project.enable_incremental_analysis;
+  }
+
 let model_hooked, set_directory_state = Hooked.S.create blank_state
 let model = Hooked.S.to_react_signal model_hooked
 
@@ -33,13 +47,27 @@ let current_filename =
         m.current)
     model
 
-let is_incremental () =
-  (React.S.value State_project.model).State_project.model_parameters
-    .State_project.enable_incremental_analysis
+let is_incremental () = (React.S.value model).incremental
+
+let toggle_incremental_analysis enable_incremental_analysis =
+  let state = React.S.value model in
+  if state.incremental <> enable_incremental_analysis then (
+    let () =
+      set_directory_state
+        { state with incremental = enable_incremental_analysis }
+    in
+    State_project.eval_with_project ~label:__LOC__
+      (fun (manager : Api.concrete_manager) ->
+        if enable_incremental_analysis then
+          manager#file_update_ws (React.S.value current_filename)
+        else
+          manager#file_update_ws None)
+  ) else
+    Lwt.return (Result_util.ok ())
 
 let update_ws_if_incremental manager filename _ =
   if is_incremental () then
-    manager#file_update_ws filename
+    manager#file_update_ws (Some filename)
   else
     Lwt.return (Result_util.ok ())
 
@@ -116,7 +144,7 @@ let update_directory ~reset current catalog =
          state.directory)
       catalog
   in
-  set_directory_state { current; directory }
+  set_directory_state { state with current; directory }
 
 let create_file ~(filename : string) ~(content : string) : unit Api.lwt_result =
   State_project.eval_with_project ~label:"create_file" (fun manager ->
@@ -200,12 +228,13 @@ let set_content (content : string) : unit Api.lwt_result =
           { local = Some content; name }
           state.directory
       in
-      let () = set_directory_state { current = state.current; directory } in
+      let () = set_directory_state { state with directory } in
       Lwt.return (Result_util.ok ())
     | { local = None; name } ->
       let () =
         set_directory_state
           {
+            state with
             current =
               Some
                 {
@@ -232,7 +261,7 @@ let set_compile file_id (compile : bool) : unit Api.lwt_result =
       let directory =
         Mods.IntMap.add rank { local = None; name } state.directory
       in
-      let () = set_directory_state { current = state.current; directory } in
+      let () = set_directory_state { state with directory } in
       State_project.eval_with_project ~label:"set_compile" (fun manager ->
           manager#file_create rank name content)
     ) else
@@ -250,9 +279,7 @@ let set_compile file_id (compile : bool) : unit Api.lwt_result =
                         { local = Some content; name }
                         state.directory
                     in
-                    let () =
-                      set_directory_state { current = state.current; directory }
-                    in
+                    let () = set_directory_state { state with directory } in
                     State_project.eval_with_project ~label:"set_compile'"
                       (fun manager -> manager#file_delete name)
                   ) else (
@@ -271,7 +298,7 @@ let remove_file () : unit Api.lwt_result =
             { rank; cursor_pos = dummy_cursor_pos; out_of_sync = false })
           (Mods.IntMap.root directory)
       in
-      let () = set_directory_state { current; directory } in
+      let () = set_directory_state { state with current; directory } in
       let x = send_refresh None in
       match local with
       | Some _ -> x
@@ -305,9 +332,9 @@ let do_a_move state file_id rank =
       State_project.eval_with_project ~label:"remove_file" (fun manager ->
           manager#file_move rank file_id
           >>= Api_common.result_bind_with_lwt ~ok:(fun () ->
-                  Lwt.return (Result_util.ok { current; directory })))
+                  Lwt.return (Result_util.ok { state with current; directory })))
     else
-      Lwt.return (Result_util.ok { current; directory })
+      Lwt.return (Result_util.ok { state with current; directory })
 
 let rec set_position state file_id rank =
   match Mods.IntMap.find_option rank state.directory with
@@ -340,14 +367,14 @@ let cursor_activity ~line ~ch =
   | Some { rank; out_of_sync; _ } ->
     set_directory_state
       {
+        v with
         current =
           Some
             {
               rank;
               cursor_pos = { Loc.line = succ line; chr = ch };
               out_of_sync;
             };
-        directory = v.directory;
       }
 
 let out_of_sync out_of_sync =
@@ -356,10 +383,7 @@ let out_of_sync out_of_sync =
   | None -> ()
   | Some { rank; cursor_pos; _ } ->
     set_directory_state
-      {
-        current = Some { rank; cursor_pos; out_of_sync };
-        directory = v.directory;
-      }
+      { v with current = Some { rank; cursor_pos; out_of_sync } }
 
 let sync ?(reset = false) () : unit Api.lwt_result =
   State_project.eval_with_project ~label:"select_file" (fun manager ->
diff --git a/gui/state/state_file.mli b/gui/state/state_file.mli
@@ -40,10 +40,16 @@ val out_of_sync : bool -> unit
 
 type slot = { local: string option; name: string }
 type active = { rank: int; cursor_pos: Loc.position; out_of_sync: bool }
-type model = { current: active option; directory: slot Mods.IntMap.t }
+
+type model = {
+  current: active option;
+  directory: slot Mods.IntMap.t;
+  incremental: bool;
+}
 
 val model : model React.signal
 val current_filename : string option React.signal
+val toggle_incremental_analysis : bool -> unit Api.lwt_result
 
 val apply_on_current_pos_of_model :
   (string -> Loc.position -> 'a) -> model -> 'a option
diff --git a/gui/ui/panel_tabs/tab_editor/editor.ml b/gui/ui/panel_tabs/tab_editor/editor.ml
@@ -239,11 +239,18 @@ let working_set_elements_checkboxes =
         let () =
           Codemirror.clearGutter ~cm:codemirror ~gutter_id:working_set_gutter
         in
-        manager#get_working_set_elements >|= fun x ->
-        (match x.Result_util.value with
-        | Result.Ok rules ->
-          add_checkbox_to_working_set_elements rules codemirror
-        | Result.Error _ -> ()))
+        let model = React.S.value State_project.model in
+        if
+          model.State_project.model_parameters
+            .State_project.enable_incremental_analysis
+        then
+          manager#get_working_set_elements >|= fun x ->
+          match x.Result_util.value with
+          | Result.Ok rules ->
+            add_checkbox_to_working_set_elements rules codemirror
+          | Result.Error _ -> ()
+        else
+          Lwt.return ())
 
 let onload () : unit =
   let () = Editor_menu_file.onload () in
diff --git a/gui/ui/panel_tabs/tab_editor/tab_editor.ml b/gui/ui/panel_tabs/tab_editor/tab_editor.ml
@@ -211,13 +211,22 @@ let init_non_weakly_reversible_transitions () =
                Lwt.return (Result_util.ok ()))))
     State_project.model
 
+let init_incremental_analysis () =
+  React.S.l1
+    (fun model ->
+      State_file.toggle_incremental_analysis
+        model.State_project.model_parameters
+          .State_project.enable_incremental_analysis)
+    State_project.model
+
 let dont_gc_me = ref []
 
 let onload () =
   let () = Editor.onload () in
   dont_gc_me := init_dead_rules () :: !dont_gc_me;
   dont_gc_me := init_dead_agents () :: !dont_gc_me;
   dont_gc_me := init_non_weakly_reversible_transitions () :: !dont_gc_me;
+  dont_gc_me := init_incremental_analysis () :: !dont_gc_me;
   let () = Subtab_contact_map.onload () in
   let () = Subtab_influences.onload () in
   let () = Subtab_constraints.onload () in

Original file line number	Diff line number	Diff line change
`@@ -110,7 +110,8 @@ class virtual new_client ~post mailbox : Api.manager_model =`
`110`	`110`	`JsonUtil.write_sequence b`
`111`	`111`	`[`
`112`	`112`	`(fun b -> Yojson.Basic.write_string b "FileUpdateWS");`
`113`		`- (fun b -> Yojson.Basic.write_string b file_id);`
	`113`	`+ (fun b ->`
	`114`	`+ JsonUtil.write_option Yojson.Basic.write_string b file_id);`
`114`	`115`	`])`
`115`	`116`
`116`	`117`	`method file_move file_position file_id =`
Original file line number	Diff line number	Diff line change
`@@ -240,7 +240,8 @@ class virtual new_client ~is_running ~post mailbox =`
`240`	`240`	`JsonUtil.write_sequence b`
`241`	`241`	`[`
`242`	`242`	`(fun b -> Yojson.Basic.write_string b "FileUpdateWS");`
`243`		`- (fun b -> Yojson.Basic.write_string b file_id);`
	`243`	`+ (fun b ->`
	`244`	`+ JsonUtil.write_option Yojson.Basic.write_string b file_id);`
`244`	`245`	`])`
`245`	`246`
`246`	`247`	`method file_move file_position file_id =`