Skip to content

Commit

Permalink
feat: put all document related events (proofview, errors, move cursor…
Browse files Browse the repository at this point in the history 
…, etc..) back in documentManager

WIP
  • Loading branch information
@rtetley
rtetley committed Nov 22, 2024
1 parent 42a52e1 commit 305a024
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 52 deletions.
11 changes: 11 additions & 0 deletions language-server/dm/documentManager.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ type event =
| Observe of Types.sentence_id
| ParseMore of Document.event
| SendProofView of Types.sentence_id
| SendBlockOnError of Types.sentence_id

type handled_event = {
state : state option;
Expand All @@ -77,6 +78,9 @@ let pp_event fmt = function
| ParseMore _ -> Stdlib.Format.fprintf fmt "ParseMore event"
| SendProofView id ->
Stdlib.Format.fprintf fmt "SendProofView %d" @@ (Stateid.to_int id)
| SendBlockOnError id ->
Stdlib.Format.fprintf fmt "SendBlockOnError %d" @@ (Stateid.to_int id)

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
Expand Down Expand Up @@ -570,6 +574,13 @@ let handle_event ev st block background diff_mode =
let notification = Some (Notification.Server.ProofView params) in
let update_view = true in
{state=(Some st); events=[]; update_view; blocking_error=None; notification}
| SendBlockOnError id ->
let {uri} = st in
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}



let context_of_id st = function
| None -> Some (ExecutionManager.get_initial_context st.execution_state)
Expand Down
62 changes: 10 additions & 52 deletions language-server/vscoqtop/lspManager.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ let open_new_document uri text =
in

let vst = init_document local_args vst in
let st, events = try Dm.DocumentManager.init vst ~opts uri ~text with
let st, events = try Dm.DocumentManager.init vst ~opts:(Coqargs.injection_commands local_args) uri ~text with
e -> raise e
in
Hashtbl.add states (DocumentUri.to_path uri) { st ; visible = true; };
Expand Down Expand Up @@ -414,48 +414,21 @@ let coqtopInterpretToPoint params =
match Hashtbl.find_opt states (DocumentUri.to_path uri) with
| None -> log @@ "[interpretToPoint] ignoring event on non existent document"; []
| Some { st; visible } ->
let (st, events, error_range, position) =
match !point_interp_mode with
| Settings.PointInterpretationMode.Cursor ->
let st, evs, blocking_err = Dm.DocumentManager.interpret_to_position st position in
(st, evs, blocking_err, position)
| Settings.PointInterpretationMode.NextCommand ->
Dm.DocumentManager.interpret_to_next_position st position
let (st, events, error_range) = Dm.DocumentManager.interpret_to_position st position ~check_mode:!check_mode ~point_interp_mode:!point_interp_mode
in
replace_state (DocumentUri.to_path uri) st visible;
update_view uri st;
let sel_events = inject_dm_events (uri, events) in
match error_range with
| None ->
sel_events @ [ mk_proof_view_event uri (Some position)]
| Some {last_range; error_range} ->
if !check_mode = Settings.Mode.Manual then
sel_events @ mk_block_on_error_event uri last_range error_range
else
sel_events @ [mk_proof_view_event uri (Some error_range.end_)]
sel_events

let coqtopStepBackward params =
let Notification.Client.StepBackwardParams.{ textDocument = { uri }; position } = params in
match Hashtbl.find_opt states (DocumentUri.to_path uri) with
| None -> log "[stepBackward] ignoring event on non existent document"; []
| Some { st; visible } ->
if !check_mode = Settings.Mode.Continuous then
match position with
| None -> []
| Some pos ->
match Dm.DocumentManager.get_previous_range st pos with
| None -> []
| Some range -> [mk_move_cursor_event uri range]
else
let (st, events, _) = Dm.DocumentManager.interpret_to_previous st in
let range = Dm.DocumentManager.observe_id_range st in
let (st, events, _) = Dm.DocumentManager.interpret_to_previous st ~check_mode:!check_mode in
replace_state (DocumentUri.to_path uri) st visible;
update_view uri st;
match range with
| None ->
inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
| Some range ->
[ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]

let coqtopStepForward params =
let Notification.Client.StepForwardParams.{ textDocument = { uri }; position } = params in
Expand All @@ -470,14 +443,10 @@ let coqtopStepForward params =
| None -> []
| Some range -> [mk_move_cursor_event uri range]
else
let (st, events, error_range) = Dm.DocumentManager.interpret_to_next st in
let range = Dm.DocumentManager.observe_id_range st in
let (st, events, error_range) = Dm.DocumentManager.interpret_to_next st ~check_mode:!check_mode in
replace_state (DocumentUri.to_path uri) st visible;
update_view uri st;
match range, error_range with
| None, None -> inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
| _, Some { last_range; error_range} -> inject_dm_events (uri,events) @ mk_block_on_error_event_no_move uri error_range
| Some range, None -> [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
inject_dm_events (uri,events)


let make_CompletionItem i item : CompletionItem.t =
Expand Down Expand Up @@ -533,14 +502,10 @@ let coqtopInterpretToEnd params =
match Hashtbl.find_opt states (DocumentUri.to_path uri) with
| None -> log @@ "[interpretToEnd] ignoring event on non existent document"; []
| Some { st; visible } ->
let (st, events, error_range) = Dm.DocumentManager.interpret_to_end st in
let (st, events, error_range) = Dm.DocumentManager.interpret_to_end st ~check_mode:!check_mode in
replace_state (DocumentUri.to_path uri) st visible;
update_view uri st;
match error_range with
| None ->
inject_dm_events (uri,events) @ [ mk_proof_view_event uri None]
| Some {last_range; error_range} ->
inject_dm_events (uri,events) @ mk_block_on_error_event uri last_range error_range
inject_dm_events (uri,events)

let coqtopLocate id params =
let Request.Client.LocateParams.{ textDocument = { uri }; position; pattern } = params in
Expand Down Expand Up @@ -735,14 +700,7 @@ let handle_event = function
| SendProofView (uri, position) ->
begin match Hashtbl.find_opt states (DocumentUri.to_path uri) with
| None -> log @@ "ignoring event on non existent document"; []
| Some { st } ->
let proof = Dm.DocumentManager.get_proof st !diff_mode position in
let messages = Dm.DocumentManager.get_messages st position in
let messages =
if !full_messages then messages
else List.filter (fun (sev,_) -> sev == DiagnosticSeverity.Information) messages
in
send_proof_view Notification.Server.ProofViewParams.{ proof; messages }; []
| Some { st } -> []
end
| SendMoveCursor (uri, range) ->
send_move_cursor uri range; []
Expand Down

0 comments on commit 305a024

Please sign in to comment.