Skip to content
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

do not move cursor or flash red in continuous mode #972

Closed
wants to merge 1 commit into from
Closed

do not move cursor or flash red in continuous mode #972

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
25 changes: 15 additions & 10 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,15 +101,20 @@ let mk_observe_event id =
let mk_move_cursor_event id =
let priority = PriorityManager.move_cursor in
Sel.now ~priority @@ SendMoveCursor id
let mk_block_on_error_event last_range error_id =
let priority = PriorityManager.move_cursor in
let event = Sel.now ~priority @@ SendBlockOnError error_id in
match last_range with
| None ->
[event] @ [mk_proof_view_event error_id]
| Some range ->
[event] @ [mk_move_cursor_event range] @ [mk_proof_view_event error_id]

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 move_cursor =
match last_range with
| Some last_range -> [mk_move_cursor_event last_range]
| None -> [] in
red_flash @ move_cursor @ update_goal_view

type events = event Sel.Event.t list

let executed_ranges st mode =
Expand Down Expand Up @@ -313,7 +318,7 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
{state with execution_state}, []
| Some (error_id, loc) ->
let state, error_range = state_before_error state error_id loc in
let events = mk_block_on_error_event error_range error_id in
let events = mk_block_on_error_event error_range error_id background in
{state with execution_state}, events

let reset_to_top st = { st with observe_id = Top }
Expand Down Expand Up @@ -554,7 +559,7 @@ let execute st id vst_for_next_todo started task background block =
| None -> st, []
| Some (error_id, loc) ->
let st, error_range = state_before_error st error_id loc in
let events = if block then mk_block_on_error_event error_range error_id else [] in
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
Expand Down
Loading