Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@rtetley
rtetley committed Nov 25, 2024
1 parent 305a024 commit 8c8249a
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 40 deletions.
94 changes: 55 additions & 39 deletions language-server/dm/documentManager.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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

Expand Down Expand Up @@ -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 } ->
Expand All @@ -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 }

Expand All @@ -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 ->
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion language-server/dm/documentManager.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) *)

Expand Down

0 comments on commit 8c8249a

Please sign in to comment.