Skip to content

Avoid duplicate beginParsing events #1184

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
gares wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Avoid duplicate beginParsing events #1184

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
40dd039
uniq
gares Dec 1, 2025
b9d7216
bup sel
gares Dec 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 25 additions & 19 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,27 +107,40 @@ let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x
let inject_em_events events = List.map inject_em_event events
let inject_doc_event x = Sel.Event.map (fun e -> DocumentEvent e) x
let inject_doc_events events = List.map inject_doc_event events


let mk_proof_view_event id =
Sel.now ~priority:PriorityManager.proof_view (SendProofView (Some id))
let mk_proof_view_event_empty =
Sel.now ~priority:PriorityManager.proof_view (SendProofView None)

let mk_interp_to_event mode tgt =
[Sel.now ~priority:PriorityManager.interp_to (InterpretTo(mode,tgt))]
Sel.now ~priority:PriorityManager.interp_to (InterpretTo(mode,tgt))

let mk_observe_event id =
Sel.now ~priority:PriorityManager.execution (Observe id)
let mk_move_cursor_event id =
let priority = PriorityManager.move_cursor in
Sel.now ~priority @@ SendMoveCursor id

let mk_red_flash_event error_id =
let priority = PriorityManager.move_cursor in
Sel.now ~priority ~undup:(=) @@ SendBlockOnError error_id

let mk_execution_event background event =
let priority = if background then None else Some PriorityManager.execution in
Sel.now ?priority event

let mk_parse_begin_event =
let priority = PriorityManager.launch_parsing in
Sel.now ~priority ~undup:(=) ParseBegin

let mk_block_on_error_event last_range error_id background =
let update_goal_view = [mk_proof_view_event error_id] in
if background then
update_goal_view
else
let red_flash =
[Sel.now ~priority:PriorityManager.move_cursor @@ SendBlockOnError error_id] in
let red_flash = [mk_red_flash_event error_id] in
let move_cursor =
match last_range with
| Some last_range -> [mk_move_cursor_event last_range]
Expand Down Expand Up @@ -315,10 +328,6 @@ let get_info_messages st pos =
let feedback = feedback |> List.filter info in
List.map (fun (lvl,_oloc,_,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_rocqpp msg) feedback

let create_execution_event background event =
let priority = if background then None else Some PriorityManager.execution in
Sel.now ?priority event

let state_before_error state error_id loc =
match Document.get_sentence state.document error_id with
| None -> state, None
Expand All @@ -342,7 +351,7 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
let vst_for_next_todo, execution_state, task, error_id = ExecutionManager.build_tasks_for state.document (Document.schedule state.document) state.execution_state id should_block_on_error in
match task with
| Some task -> (* task will only be Some if there is no error *)
let event = create_execution_event background (Execute {id; vst_for_next_todo; task; started = Unix.gettimeofday ()}) in
let event = mk_execution_event background (Execute {id; vst_for_next_todo; task; started = Unix.gettimeofday ()}) in
let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in
{state with execution_state; cancel_handle}, [event]
| None ->
Expand Down Expand Up @@ -535,10 +544,10 @@ let real_interpret_to_end st check_mode =
log (fun () -> "interpret_to_end id = " ^ Stateid.to_string id);
interpret_to st id check_mode

let interpret_to_end check_mode = mk_interp_to_event check_mode End
let interpret_to_next check_mode = mk_interp_to_event check_mode Next
let interpret_to_previous check_mode = mk_interp_to_event check_mode Previous
let interpret_to_position p check_mode ~point_interp_mode = mk_interp_to_event check_mode (Point(p,point_interp_mode))
let interpret_to_end check_mode = [mk_interp_to_event check_mode End]
let interpret_to_next check_mode = [mk_interp_to_event check_mode Next]
let interpret_to_previous check_mode = [mk_interp_to_event check_mode Previous]
let interpret_to_position p check_mode ~point_interp_mode = [mk_interp_to_event check_mode (Point(p,point_interp_mode))]


let interpret_in_background st ~should_block_on_error =
Expand Down Expand Up @@ -589,8 +598,7 @@ let init init_vs ~opts uri ~text =
let document = Document.create_document init_vs.Vernacstate.synterp text in
let execution_state, feedback = ExecutionManager.init init_vs in
let state = { uri; opts; init_vs; document; execution_state; observe_id=Top; cancel_handle = None; document_state = Parsing } in
let priority = Some PriorityManager.launch_parsing in
let event = Sel.now ?priority ParseBegin in
let event = mk_parse_begin_event in
state, [event] @ [inject_em_event feedback]

let reset { uri; opts; init_vs; document; execution_state; } =
Expand All @@ -601,8 +609,7 @@ let reset { uri; opts; init_vs; document; execution_state; } =
let execution_state, feedback = ExecutionManager.init init_vs in
let observe_id = Top in
let state = { uri; opts; init_vs; document; execution_state; observe_id; cancel_handle = None ; document_state = Parsing } in
let priority = Some PriorityManager.launch_parsing in
let event = Sel.now ?priority ParseBegin in
let event = mk_parse_begin_event in
state, [event] @ [inject_em_event feedback]

let apply_text_edits state edits =
Expand All @@ -617,8 +624,7 @@ let apply_text_edits state edits =
{state with execution_state; document}
in
let state = List.fold_left apply_edit_and_shift_diagnostics_locs_and_overview state edits in
let priority = Some PriorityManager.launch_parsing in
let sel_event = Sel.now ?priority ParseBegin in
let sel_event = mk_parse_begin_event in
state, [sel_event]

let execution_finished st id started =
Expand Down Expand Up @@ -660,7 +666,7 @@ let execute st id vst_for_next_todo started task background block =
let events = if block then mk_block_on_error_event error_range error_id background else [] in
st, events
in
let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in
let event = Option.map (fun task -> mk_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in
match event, block_events with
| None, [] -> execution_finished { st with execution_state } id started (* There is no new tasks, and no errors -> execution finished *)
| _ ->
Expand Down
2 changes: 1 addition & 1 deletion language-server/vsrocq-language-server.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ depends: [
"ppx_optcomp"
"result" { >= "1.5" }
"lsp" { >= "1.15"}
"sel" {>= "0.6.0"}
"sel" {>= "0.8.0"}
]
conflicts: [
"vscoq-language-server" {< "2.2.7~"}
Expand Down
Loading