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

Doc string proof of concept #998

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

Doc string proof of concept #998

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
1439af4
feat: add doc string support
rtetley Jan 20, 2025
5413438
feat: docstrings shift
rtetley Jan 21, 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
7 changes: 7 additions & 0 deletions language-server/dm/document.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,7 @@ type document = {
sentences_by_end : sentence LM.t;
parsing_errors_by_end : parsing_error LM.t;
comments_by_end : comment LM.t;
hover_info : HoverInfo.t;
schedule : Scheduler.schedule;
outline : outline;
parsed_loc : int;
Expand Down Expand Up @@ -612,6 +613,11 @@ let invalidate top_edit top_id parsed_doc new_sentences =
let invalid_ids, doc = invalidate_diff parsed_doc scheduler_state Stateid.Set.empty diff in
unchanged_id, invalid_ids, doc

let shift_hover_info document ~from ~amount =
let {hover_info} = document in
let hover_info = HoverInfo.shift hover_info ~from ~amount in
{document with hover_info}

(** Validate document when raw text has changed *)
let validate_document ({ parsed_loc; raw_doc; cancel_handle } as document) =
(* Cancel any previous parsing event *)
Expand Down Expand Up @@ -676,6 +682,7 @@ let create_document init_synterp_state text =
outline = [];
init_synterp_state;
cancel_handle = None;
hover_info = HoverInfo.empty ();
}

let apply_text_edit document edit =
Expand Down
2 changes: 2 additions & 0 deletions language-server/dm/document.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,8 @@ val raw_document : document -> RawDocument.t

val outline : document -> outline

val shift_hover_info : document -> from:int -> amount:int -> document

val create_document : Vernacstate.Synterp.t -> string -> document
(** [create_document init_synterp_state text] creates a fresh document with content defined by
[text] under [init_synterp_state]. *)
Expand Down
1 change: 1 addition & 0 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -537,6 +537,7 @@ let apply_text_edits state edits =
let edit_length = edit_stop - edit_start in
let exec_st = ExecutionManager.shift_diagnostics_locs exec_st ~start:edit_stop ~offset:(String.length new_text - edit_length) in
let execution_state = ExecutionManager.shift_overview exec_st ~before:(Document.raw_document state.document) ~after:(Document.raw_document document) ~start:edit_stop ~offset:(String.length new_text - edit_length) in
let document = Document.shift_hover_info document ~from:edit_stop ~amount:(String.length new_text - edit_length) in
{state with execution_state; document}
in
let state = List.fold_left apply_edit_and_shift_diagnostics_locs_and_overview state edits in
Expand Down
Loading