package vscoq-language-server
Install
Dune Dependency
Authors
Maintainers
Sources
md5=f528c1760966ac10d48b5f1c5531411a
sha512=1f69538ae5f78854b34e3f1a9d408714843e899bb96d063c2bfac410339b6a13ee5f30d5e7b3cd2bbd673169bcfdb550153ba741092cdc3ee3a8ca6446cc2240
doc/vscoq-language-server.dm/Dm/DocumentManager/index.html
Module Dm.DocumentManager
Source
The document manager holds the view that Coq has of the currently open states. It makes it easy for IDEs to handle text edits, navigate and get feedback. Note that it does not require IDEs to parse vernacular sentences.
type blocking_error = {
last_range : Protocol.LspWrapper.Range.t;
error_range : Protocol.LspWrapper.Range.t;
}
type handled_event = {
state : state option;
events : events;
update_view : bool;
notification : Protocol.ExtProtocol.Notification.Server.t option;
}
val init :
Vernacstate.t ->
opts:Coqargs.injection_command list ->
Lsp.Types.DocumentUri.t ->
text:string ->
state * events
init st opts uri text
initializes the document manager with initial vernac state st
on which command line opts will be set.
apply_text_edits doc edits
updates the text of doc
with edits
. A ParseEvent is triggered, once processed: the new document is parsed, outdated executions states are invalidated, and the observe id is updated.
reset_to_top state
updates the state to make the observe_id Top
val get_next_range :
state ->
Protocol.LspWrapper.Position.t ->
Protocol.LspWrapper.Range.t option
get_next_range st pos
get the range of the next sentence relative to pos
val get_previous_range :
state ->
Protocol.LspWrapper.Position.t ->
Protocol.LspWrapper.Range.t option
get_previous_pos st pos
get the range of the previous sentence relative to pos
val interpret_to_position :
state ->
Protocol.LspWrapper.Position.t ->
Protocol.Settings.Mode.t ->
point_interp_mode:Protocol.Settings.PointInterpretationMode.t ->
state * events
interpret_to_position state pos check_mode point_interp_mode
navigates to the last sentence ending before or at pos
and returns the resulting state, events that need to take place, and a possible blocking error.
val interpret_to_next_position :
state ->
Protocol.LspWrapper.Position.t ->
Protocol.Settings.Mode.t ->
state * events
interpret_to_next_position state pos check_mode
navigates to the first sentence after or at pos
(excluding whitespace) and returns the resulting state, events that need to take place, a possible blocking error.
interpret_to_previous doc check_mode
navigates to the previous sentence in doc
and returns the resulting state.
interpret_to_next doc
navigates to the next sentence in doc
and returns the resulting state.
interpret_to_end doc
navigates to the last sentence in doc
and returns the resulting state.
interpret_in_background doc
same as interpret_to_end
but computation is done in background (with lower priority)
executes_ranges doc mode
returns the ranges corresponding to the sentences that have been executed. mode
allows to send a "cut" range that only goes until the observe_id in the case of manual mode
returns the range of the sentence referenced by observe_id *
val get_messages :
state ->
Types.sentence_id ->
(Protocol.LspWrapper.DiagnosticSeverity.t * Protocol.Printing.pp) list
returns the messages associated to a given position
val get_info_messages :
state ->
Protocol.LspWrapper.Position.t option ->
(Protocol.LspWrapper.DiagnosticSeverity.t * Protocol.Printing.pp) list
returns the Feedback.Info level messages associated to a given position
all_diagnostics doc
returns the diagnostics corresponding to the sentences that have been executed in doc
.
val get_proof :
state ->
Protocol.Settings.Goals.Diff.Mode.t ->
Types.sentence_id option ->
Protocol.ProofState.t option
val get_completions :
state ->
Protocol.LspWrapper.Position.t ->
CompletionItems.completion_item list
val handle_event :
event ->
state ->
block:bool ->
Protocol.Settings.Mode.t ->
Protocol.Settings.Goals.Diff.Mode.t ->
handled_event
handles events and returns a new state if it was updated. On top of the next events, it also returns info on whether execution has halted due to an error and returns a boolean flag stating whether the view should be updated
val search :
state ->
id:string ->
Protocol.LspWrapper.Position.t ->
string ->
Protocol.LspWrapper.notification Sel.Event.t list
val about :
state ->
Protocol.LspWrapper.Position.t ->
pattern:string ->
(Protocol.Printing.pp, Types.error) Result.t
Returns an optional Result: if None, the position did not have a word, if Some, an Ok/Error result is returned.
val jump_to_definition :
state ->
Protocol.LspWrapper.Position.t ->
(Protocol.LspWrapper.Range.t * string) option
val check :
state ->
Protocol.LspWrapper.Position.t ->
pattern:string ->
(Protocol.Printing.pp, Types.error) Result.t
val locate :
state ->
Protocol.LspWrapper.Position.t ->
pattern:string ->
(Protocol.Printing.pp, Types.error) Result.t
val print :
state ->
Protocol.LspWrapper.Position.t ->
pattern:string ->
(Protocol.Printing.pp, Types.error) Result.t