diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index d2f362f0..95d60cc4 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -57,11 +57,11 @@ type event = | ParseMore of Document.event | SendProofView of Types.sentence_id | SendBlockOnError of Types.sentence_id + | SendMoveCursor of Range.t type handled_event = { state : state option; events: event Sel.Event.t list; - blocking_error: blocking_error option; update_view: bool; notification: Notification.Server.t option; } @@ -80,15 +80,28 @@ let pp_event fmt = function Stdlib.Format.fprintf fmt "SendProofView %d" @@ (Stateid.to_int id) | SendBlockOnError id -> Stdlib.Format.fprintf fmt "SendBlockOnError %d" @@ (Stateid.to_int id) + | SendMoveCursor range -> + Stdlib.Format.fprintf fmt "SendBlockOnError %s" @@ (Range.to_string range) 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 -> ParseMore e) x let inject_doc_events events = List.map inject_doc_event events -let mk_proof_view_event position = - Sel.now ~priority:PriorityManager.proof_view (SendProofView (position)) +let mk_proof_view_event id = + Sel.now ~priority:PriorityManager.proof_view (SendProofView (id)) let mk_observe_event id = Sel.now ~priority:PriorityManager.execution (Observe id) +let mk_move_cursor_event id = + let priority = Dm.PriorityManager.move_cursor in + Sel.now ~priority @@ SendMoveCursor id +let mk_block_on_error_event last_range error_id = + let priority = Dm.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] type events = event Sel.Event.t list @@ -259,7 +272,7 @@ let create_execution_event background event = let priority = if background then None else Some PriorityManager.execution in Sel.now ?priority event -let create_blocking_error_range state error_id = +let state_before_error state error_id = match Document.get_sentence state.document error_id with | None -> state, None | Some { start } -> @@ -268,33 +281,32 @@ let create_blocking_error_range state error_id = let start = Position.{line=0; character=0} in let end_ = Position.{line=0; character=0} in let last_range = Range.{start; end_} in - let error_range = Document.range_of_id_with_blank_space state.document error_id in let observe_id = Top in - ({state with observe_id}, Some {last_range; error_range}) + {state with observe_id}, Some last_range | Some { id } -> let last_range = Document.range_of_id_with_blank_space state.document id in - let error_range = Document.range_of_id_with_blank_space state.document error_id in let observe_id = (Id id) in - ({state with observe_id}, Some {last_range; error_range}) + {state with observe_id}, Some last_range -let observe ~background state id ~should_block_on_error : (state * event Sel.Event.t list * blocking_error option) = +let observe ~background state id ~should_block_on_error : (state * event Sel.Event.t list) = match Document.get_sentence state.document id with - | None -> (state, [], None) (* TODO error? *) + | None -> state, [] (* TODO error? *) | Some { id } -> Option.iter Sel.Event.cancel state.cancel_handle; 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 -> + | 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 cancel_handle = Some (Sel.Event.get_cancellation_handle event) in - ({state with execution_state; cancel_handle}, [event], None) + {state with execution_state; cancel_handle}, [event] | None -> match error_id with | None -> - ({state with execution_state}, [], None) + {state with execution_state}, [] | Some error_id -> - let state, blocking_error_range = create_blocking_error_range state error_id in - ({state with execution_state}, [], blocking_error_range) + let state, last_range = state_before_error state error_id in + let events = mk_block_on_error_event last_range error_id in + {state with execution_state}, events let reset_to_top st = { st with observe_id = Top } @@ -318,24 +330,24 @@ let interpret_to st id ~check_mode = | Settings.Mode.Manual -> let event = mk_observe_event id in let pv_event = mk_proof_view_event id in - st, [event] @ [pv_event], None + st, [event] @ [pv_event] | Settings.Mode.Continuous -> match ExecutionManager.is_executed st.execution_state id with - | true -> st, [mk_proof_view_event id], None - | false -> st, [], None + | true -> st, [mk_proof_view_event id] + | false -> st, [] let interpret_to_next_position st pos ~check_mode = match id_of_sentence_after_pos st pos with - | None -> (st, [], None) (* document is empty *) + | None -> (st, []) (* document is empty *) | Some id -> - let st, events, blocking_error = interpret_to st id ~check_mode in - (st, events, blocking_error) + let st, events = interpret_to st id ~check_mode in + (st, events) let interpret_to_position st pos ~check_mode ~point_interp_mode = match point_interp_mode with | Settings.PointInterpretationMode.Cursor -> begin match id_of_pos st pos with - | None -> (st, [], None) (* document is empty *) + | None -> (st, []) (* document is empty *) | Some id -> interpret_to st id ~check_mode end | Settings.PointInterpretationMode.NextCommand -> @@ -365,42 +377,42 @@ let get_previous_range st pos = let interpret_to_previous st ~check_mode = match st.observe_id with - | Top -> (st, [], None) + | Top -> (st, []) | (Id id) -> match Document.get_sentence st.document id with - | None -> (st, [], None) (* TODO error? *) + | None -> (st, []) (* TODO error? *) | Some { start } -> match Document.find_sentence_before st.document start with | None -> Vernacstate.unfreeze_full_state st.init_vs; - { st with observe_id=Top }, [], None + { st with observe_id=Top }, [] | Some { id } -> interpret_to st id ~check_mode let interpret_to_next st ~check_mode = match st.observe_id with | Top -> begin match Document.get_first_sentence st.document with - | None -> (st, [], None) (*The document is empty*) + | None -> st, [] (*The document is empty*) | Some { id } -> interpret_to st id ~check_mode end | Id id -> match Document.get_sentence st.document id with - | None -> (st, [], None) (* TODO error? *) + | None -> st, [] (* TODO error? *) | Some { stop } -> match Document.find_sentence_after st.document (stop+1) with - | None -> (st, [], None) + | None -> st, [] | Some { id } -> interpret_to st id ~check_mode let interpret_to_end st ~check_mode = match Document.get_last_sentence st.document with - | None -> (st, [], None) + | None -> (st, []) | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to st id ~check_mode let interpret_in_background st ~should_block_on_error = match Document.get_last_sentence st.document with - | None -> (st, [], None) + | None -> (st, []) | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); observe ~background:true st id ~should_block_on_error let is_above st id1 id2 = @@ -492,21 +504,23 @@ let execute st id vst_for_next_todo started task background block = | Some _ -> let (next, execution_state,vst_for_next_todo,events, exec_error) = ExecutionManager.execute st.execution_state st.document (vst_for_next_todo, [], false) task block in - let st, blocking_error = + let st, block_events = match exec_error with - | None -> st, None - | Some id -> create_blocking_error_range st id + | None -> st, [] + | Some error_id -> let st, last_range = state_before_error st error_id in + let events = if block then mk_block_on_error_event last_range error_id 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 - match event, blocking_error with - | None, None -> execution_finished { st with execution_state } id started + match event, block_events with + | None, [] -> execution_finished { st with execution_state } id started (* There is no new tasks, and no errors -> execution finished *) | _ -> let cancel_handle = Option.map Sel.Event.get_cancellation_handle event in let event = Option.cata (fun event -> [event]) [] event in let state = Some {st with execution_state; cancel_handle} in let update_view = true in - let events = inject_em_events events @ event in - {state; events; blocking_error; update_view; notification=None} + let events = inject_em_events events @ block_events @ event in + {state; events; update_view; notification=None} let get_proof st diff_mode id = let previous_st id = @@ -579,8 +593,10 @@ let handle_event ev st block background diff_mode = let range = Document.range_of_id st.document id in let notification = Some (Notification.Server.BlockOnError {uri; range}) in {state=(Some st); events=[]; blocking_error=None; update_view=false; notification} - - + | SendMoveCursor range -> + let {uri} = st in + let notification = Some (Notification.Server.MoveCursor {uri; range}) in + {state=(Some st); events=[]; blocking_error=None; update_view=false; notification} let context_of_id st = function | None -> Some (ExecutionManager.get_initial_context st.execution_state) diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 832923e6..3c37fee6 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -88,7 +88,7 @@ val interpret_to_end : state -> check_mode:Settings.Mode.t -> (state * events * (** [interpret_to_end doc] navigates to the last sentence in [doc] and returns the resulting state. *) -val interpret_in_background : state -> should_block_on_error:bool -> (state * events * blocking_error option) +val interpret_in_background : state -> should_block_on_error:bool -> (state * events) (** [interpret_in_background doc] same as [interpret_to_end] but computation is done in background (with lower priority) *)