Merge PR #15772: Correctly prevent editable status of text when CoqIDE is busy.

Reviewed-by: herbelin
Co-authored-by: herbelin <[email protected]>

Author: coqbot-app[bot]

ide/coqide/coqide.ml

@@ -70,12 +70,6 @@ let on_current_term f =
   | None -> ()
   | Some t -> ignore (f t)
 
-let on_current_term_val default f =
-  let term = try Some notebook#current_term with Invalid_argument _ -> None in
-  match term with
-  | None -> default
-  | Some t -> f t
-
 let cb_on_current_term f _ = on_current_term f
 
 (** Nota: using && here has the advantage of working both under win32 and unix.
@@ -1295,17 +1289,6 @@ let toggle_items menu_name l =
 
 let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
 
-(* workaround: GTKSourceView3 ignores editable *)
-
-(* allowed in script panel, if editable, and elsewhere *)
-let can_paste () =
-  on_current_term_val true (fun t ->
-    (t.script#is_focus && t.script#editable2) || not t.script#is_focus)
-
-(* template insert only allowed in script panel *)
-let can_template () =
-  on_current_term_val false (fun t -> t.script#is_focus && t.script#editable2)
-
 (** Create alphabetical menu items with elements in sub-items.
     [l] is a list of lists, one per initial letter *)
 
@@ -1328,9 +1311,7 @@ let alpha_items menu_name item_name l =
       Buffer.contents buf
     in
     let callback _ =
-      on_current_term (fun sn ->
-        let text' = if can_template () then text' else "" in
-                      sn.buffer#insert_interactive text')
+      on_current_term (fun sn -> sn.buffer#insert_interactive text')
     in
     item (item_name^" "^(no_under text)) ~label:text ~callback menu_name
   in
@@ -1357,17 +1338,16 @@ let template_item (text, offset, len, key) =
   let label = "_"^name^" __" in
   let negoffset = String.length text - offset - len in
   let callback sn =
-    if can_paste () then
-      let b = sn.buffer in
-      if b#insert_interactive text then begin
-        let iter = b#get_iter_at_mark `INSERT in
-        ignore (iter#nocopy#backward_chars negoffset);
-        b#move_mark `INSERT ~where:iter;
-        ignore (iter#nocopy#backward_chars len);
-        b#move_mark `SEL_BOUND ~where:iter;
-      end
-    in
-    item name ~label ~callback:(cb_on_current_term callback) ~accel:(modifier^key)
+    let b = sn.buffer in
+    if b#insert_interactive text then begin
+      let iter = b#get_iter_at_mark `INSERT in
+      ignore (iter#nocopy#backward_chars negoffset);
+      b#move_mark `INSERT ~where:iter;
+      ignore (iter#nocopy#backward_chars len);
+      b#move_mark `SEL_BOUND ~where:iter;
+    end
+  in
+  item name ~label ~callback:(cb_on_current_term callback) ~accel:(modifier^key)
 
 (** Create menu items for pairs (query, shortcut key). *)
 let user_queries_items menu_name item_name l =
@@ -1448,19 +1428,15 @@ let build_ui () =
   menu edit_menu [
     item "Edit" ~label:"_Edit";
     item "Undo" ~accel:"<Primary>u" ~stock:`UNDO
-      ~callback:(cb_on_current_term (fun t -> if can_paste () then
-          t.script#undo ()));
+      ~callback:(cb_on_current_term (fun t -> t.script#undo ()));
     item "Redo" ~stock:`REDO
-      ~callback:(cb_on_current_term (fun t -> if can_paste () then
-          t.script#redo ()));
+      ~callback:(cb_on_current_term (fun t -> t.script#redo ()));
     item "Cut" ~stock:`CUT
-      ~callback:(fun _ -> if can_paste () then
-          emit_to_focus w GtkText.View.S.cut_clipboard);
+      ~callback:(fun _ -> emit_to_focus w GtkText.View.S.cut_clipboard);
     item "Copy" ~stock:`COPY
       ~callback:(fun _ -> emit_to_focus w GtkText.View.S.copy_clipboard);
     item "Paste" ~stock:`PASTE
-      ~callback:(fun _ -> if can_paste () then
-          emit_to_focus w GtkText.View.S.paste_clipboard);
+      ~callback:(fun _ -> emit_to_focus w GtkText.View.S.paste_clipboard);
     item "Find" ~stock:`FIND ~label:"Find / Replace"
       ~callback:(cb_on_current_term (fun t -> t.finder#show ()));
     item "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3"
@@ -1590,11 +1566,9 @@ let build_ui () =
   menu tools_menu [
     item "Tools" ~label:"_Tools";
     item "Comment" ~label:"_Comment" ~accel:"<CTRL>D"
-      ~callback:(cb_on_current_term (fun t -> if can_paste () then
-          t.script#comment ()));
+      ~callback:(cb_on_current_term (fun t -> t.script#comment ()));
     item "Uncomment" ~label:"_Uncomment" ~accel:"<CTRL><SHIFT>D"
-      ~callback:(cb_on_current_term (fun t -> if can_paste () then
-          t.script#uncomment ()));
+      ~callback:(cb_on_current_term (fun t -> t.script#uncomment ()));
     item "Coqtop arguments" ~label:"Coqtop _arguments"
       ~callback:MiscMenu.coqtop_arguments;
     item "LaTeX-to-unicode" ~label:"_LaTeX-to-unicode" ~accel:"<Shift>space"

ide/coqide/session.ml

@@ -118,34 +118,40 @@ let create_script coqtop source_buffer =
 
 let misc () = CDebug.(get_flag misc)
 
+type action_stack = Gtk.text_mark list option
+
+let call_coq_or_cancel_action coqtop coqops (buffer : GText.buffer) it =
+  let () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in
+  let mark = buffer#create_mark ~name:"target" it in
+  let action = coqops#go_to_mark (`MARK mark) in
+  ignore @@ Coq.try_grab coqtop action (fun () -> ())
+
+let init_user_action (stack : action_stack ref) = match !stack with
+| None -> stack := Some []
+| Some _ -> assert false
+
+let close_user_action (stack : action_stack ref) = match !stack with
+| None -> assert false
+| Some marks ->
+  let () = stack := None in
+  marks
+
+let handle_iter coqtop coqops (buffer : GText.buffer) it stack = match it with
+| None -> ()
+| Some it ->
+  match !stack with
+  | Some marks ->
+    (* We are inside an user action, deferring to its end *)
+    let mark = buffer#create_mark it in
+    stack := Some (mark :: marks)
+  | None ->
+    (* Otherwise we move to the mark now *)
+    call_coq_or_cancel_action coqtop coqops buffer it
+
 let set_buffer_handlers
   (buffer : GText.buffer) script (coqops : CoqOps.ops) coqtop
 =
-  let action_was_cancelled = ref true in
-  let no_coq_action_required = ref true in
-  let cur_action = ref 0 in
-  let new_action_id =
-    let id = ref 0 in
-    fun () -> incr id; !id in
-  let running_action = ref None in
-  let cancel_signal ?(stop_emit=true) reason =
-    Minilib.log ("user_action cancelled: "^reason);
-    action_was_cancelled := true;
-    if stop_emit then GtkSignal.stop_emit () in
-  let del_mark () =
-    try buffer#delete_mark (`NAME "target")
-    with GText.No_such_mark _ -> () in
-  let add_mark it = del_mark (); buffer#create_mark ~name:"target" it in
-  let call_coq_or_cancel_action f =
-    no_coq_action_required := false;
-    let action = !cur_action in
-    let action, fallback =
-      Coq.seq (Coq.lift (fun () -> running_action := Some action)) f,
-      fun () -> (* If Coq is busy due to the current action, we don't cancel *)
-        match !running_action with
-        | Some aid when aid = action -> ()
-        | _ -> cancel_signal ~stop_emit:false "Coq busy" in
-    ignore @@ Coq.try_grab coqtop action fallback in
+  let action_stack = ref None in
   let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
   let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
   let ensure_marks_exist () =
@@ -172,63 +178,55 @@ let set_buffer_handlers
     aux it it#copy in
   let insert_cb it s = if String.length s = 0 then () else begin
     if misc () then Minilib.log ("insert_cb " ^ string_of_int it#offset);
-    let text_mark = add_mark it in
     let () = update_prev it in
-    if it#has_tag Tags.Script.to_process ||
-       it#has_tag Tags.Script.incomplete then
-      cancel_signal "Altering the script being processed is not implemented"
-    else if it#has_tag Tags.Script.processed then
-      (* note code in Wg_scriptview.keypress_cb *)
-      call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
-    else if it#has_tag Tags.Script.error_bg then begin
-      match processed_sentence_just_before_error it with
-      | None -> ()
-      | Some prev_sentence_end ->
-          let text_mark = add_mark prev_sentence_end in
-          call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
-    end end in
+    let iter =
+      if it#has_tag Tags.Script.processed then Some it
+      else if it#has_tag Tags.Script.error_bg then
+        processed_sentence_just_before_error it
+      else None
+    in
+    handle_iter coqtop coqops buffer iter action_stack
+    end
+  in
   let delete_cb ~start ~stop =
     if misc () then Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
     let min_iter, max_iter =
       if start#compare stop < 0 then start, stop else stop, start in
     let () = update_prev min_iter in
-    let text_mark = add_mark min_iter in
-    let rec aux min_iter =
-      if min_iter#equal max_iter then ()
-      else if min_iter#has_tag Tags.Script.to_process ||
-              min_iter#has_tag Tags.Script.incomplete then
-        cancel_signal "Altering the script being processed is not implemented"
-      else if min_iter#has_tag Tags.Script.processed then
-        call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
-      else if min_iter#has_tag Tags.Script.error_bg then
-        match processed_sentence_just_before_error min_iter with
-        | None -> ()
-        | Some prev_sentence_end ->
-            let text_mark = add_mark prev_sentence_end in
-            call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
-      else aux min_iter#forward_char in
-    aux min_iter in
+    let rec aux iter =
+      if iter#equal max_iter then None
+      else if iter#has_tag Tags.Script.processed then
+        Some min_iter
+      else if iter#has_tag Tags.Script.error_bg then
+        processed_sentence_just_before_error iter
+      else aux iter#forward_char
+    in
+    let iter = aux min_iter in
+    handle_iter coqtop coqops buffer iter action_stack
+  in
   let begin_action_cb () =
-    if misc () then Minilib.log "begin_action_cb";
-    action_was_cancelled := false;
-    no_coq_action_required := true;
-    cur_action := new_action_id ();
+    let () = if misc () then Minilib.log "begin_action_cb" in
+    let () = init_user_action action_stack in
     let where = get_insert () in
-    buffer#move_mark (`NAME "prev_insert") ~where in
+    buffer#move_mark (`NAME "prev_insert") ~where
+  in
   let end_action_cb () =
-    if misc () then Minilib.log "end_action_cb";
-    ensure_marks_exist ();
-    if not !action_was_cancelled then begin
+    let () = if misc () then Minilib.log "end_action_cb" in
+    let marks = close_user_action action_stack in
+    let () = ensure_marks_exist () in
+    if CList.is_empty marks then
+      let start, stop = get_start (), get_stop () in
+      let () = List.iter (fun tag -> buffer#remove_tag tag ~start ~stop) Tags.Script.ephemere in
+      Sentence.tag_on_insert buffer
+    else
       (* If coq was asked to backtrack, the cleanup must be done by the
          backtrack_until function, since it may move the stop_of_input
          to a point indicated by coq. *)
-      if !no_coq_action_required then begin
-        let start, stop = get_start (), get_stop () in
-        List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
-                  Tags.Script.ephemere;
-        Sentence.tag_on_insert buffer
-      end;
-    end in
+      let iters = List.map (fun mark -> buffer#get_iter_at_mark (`MARK mark)) marks in
+      let iter = List.hd @@ List.sort (fun it1 it2 -> it1#compare it2) iters in
+      let () = List.iter (fun mark -> try buffer#delete_mark (`MARK mark) with GText.No_such_mark _ -> ()) marks in
+      call_coq_or_cancel_action coqtop coqops buffer iter
+  in
   let mark_deleted_cb m =
     match GtkText.Mark.get_name m with
     | Some "insert" -> ()
@@ -244,7 +242,13 @@ let set_buffer_handlers
     | Some s -> if misc () then Minilib.log (s^" moved")
     | None -> ()
   in
+  let set_busy b =
+    let prop = `EDITABLE b in
+    let tags = [Tags.Script.processed] in
+    List.iter (fun tag -> tag#set_property prop) tags
+  in
   (* Pluging callbacks *)
+  let () = Coq.setup_script_editable coqtop set_busy in
   let _ = buffer#connect#insert_text ~callback:insert_cb in
   let _ = buffer#connect#delete_range ~callback:delete_cb in
   let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in
@@ -409,7 +413,6 @@ let create file coqtop_args =
   let reset () = Coq.reset_coqtop coqtop in
   let buffer = create_buffer () in
   let script = create_script coqtop buffer in
-  Coq.setup_script_editable coqtop (fun v -> script#set_editable2 v);
   let proof = create_proof () in
   incr next_sid;
   let sid = !next_sid in
@@ -421,7 +424,6 @@ let create file coqtop_args =
   let messages = create_messages () in
   let segment = new Wg_Segment.segment () in
   let finder = new Wg_Find.finder basename (script :> GText.view) in
-  finder#setup_is_script_editable (fun _ -> script#editable2);
   let debugger = Wg_Debugger.debugger (Printf.sprintf "Debugger (%s)" basename) sid in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   let _ = fops#update_stats in

ide/coqide/tags.ml

@@ -22,10 +22,10 @@ struct
   let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"]
   let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
   let error_bg = make_tag table ~name:"error_bg" []
-  let to_process = make_tag table ~name:"to_process" []
+  let to_process = make_tag table ~name:"to_process" [`EDITABLE false]
   let processed = make_tag table ~name:"processed" []
   let debugging = make_tag table ~name:"debugging" []
-  let incomplete = make_tag table ~name:"incomplete" []
+  let incomplete = make_tag table ~name:"incomplete" [`EDITABLE false]
   let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
   let ephemere =

ide/coqide/wg_Find.ml

@@ -56,12 +56,7 @@ class finder name (view : GText.view) =
       let stop = view#buffer#get_iter `SEL_BOUND in
       view#buffer#get_text ~start ~stop ()
 
-    val mutable is_script_editable = ((fun _ -> failwith "is_script_editable") : unit -> bool)
-
-    method setup_is_script_editable (f : unit -> bool) = is_script_editable <- f
-
     method private may_replace () =
-      (is_script_editable ()) &&
       (self#search_text <> "") &&
       (Str.string_match self#regex (self#get_selected_word ()) 0)
 
@@ -135,11 +130,9 @@ class finder name (view : GText.view) =
           let next_ct = if edited then ct + 1 else ct in
           replace_at next next_ct (tot + 1)
       in
-      if is_script_editable () then begin
-        let () = view#buffer#begin_user_action () in
-        let () = replace_at view#buffer#start_iter 0 0 in
-        view#buffer#end_user_action ()
-      end
+      let () = view#buffer#begin_user_action () in
+      let () = replace_at view#buffer#start_iter 0 0 in
+      view#buffer#end_user_action ()
 
     method private set_not_found () =
       find_entry#misc#modify_bg [`NORMAL, `NAME "#F7E6E6"];

ide/coqide/wg_Find.mli

@@ -17,5 +17,4 @@ class finder : string -> GText.view ->
     method replace_all : unit -> unit
     method find_backward : unit -> unit
     method find_forward : unit -> unit
-    method setup_is_script_editable : (unit -> bool) -> unit
   end