def Lean.Lsp.Position.advance (p : Position) (s : Substring) : Position

Assuming that s is the content of a file starting at position p, advance p to the end of s.

Equations

• One or more equations did not get rendered due to their size.

structure ProofWidgets.MakeEditLinkProps : Type

• edit : Lean.Lsp.TextDocumentEdit

  The edit to perform on the file.

• newSelection? : Option Lean.Lsp.Range

  Which textual range to select after the edit. The range is interpreted in the file that edit applies to. If present and start == end, the cursor is moved to start and nothing is selected. If not present, the selection is not changed.

• title? : Option String

  The title property, if any, to set on the displayed <a> link.

def ProofWidgets.instFromJsonMakeEditLinkProps.fromJson : Lean.Json → Except String MakeEditLinkProps

Equations

• One or more equations did not get rendered due to their size.

instance ProofWidgets.instFromJsonMakeEditLinkProps : Lean.FromJson MakeEditLinkProps

Equations

• ProofWidgets.instFromJsonMakeEditLinkProps = { fromJson? := ProofWidgets.instFromJsonMakeEditLinkProps.fromJson }

def ProofWidgets.instToJsonMakeEditLinkProps.toJson : MakeEditLinkProps → Lean.Json

Equations

• One or more equations did not get rendered due to their size.

instance ProofWidgets.instToJsonMakeEditLinkProps : Lean.ToJson MakeEditLinkProps

Equations

• ProofWidgets.instToJsonMakeEditLinkProps = { toJson := ProofWidgets.instToJsonMakeEditLinkProps.toJson }

def ProofWidgets.MakeEditLinkProps.ofReplaceRange' (doc : Lean.Server.DocumentMeta) (range : Lean.Lsp.Range) (newText : String) (newSelection? : Option Lean.Lsp.Range := none) : MakeEditLinkProps

Replace range with newText. If newSelection? is absent, place the cursor at the end of the new text. If newSelection? is present, make the specified selection instead. See also MakeEditLinkProps.ofReplaceRange.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.MakeEditLinkProps.ofReplaceRange (doc : Lean.Server.DocumentMeta) (range : Lean.Lsp.Range) (newText : String) (newSelection? : Option (String.Pos × String.Pos) := none) : MakeEditLinkProps

Replace range with newText. If newSelection? is absent, place the cursor at the end of the new text. If newSelection? is present, select the range it specifies within newText. See also MakeEditLinkProps.ofReplaceRange'.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.MakeEditLink : Component MakeEditLinkProps

A link that, when clicked, makes the specified edit and potentially moves the cursor or makes a selection.

Equations

• One or more equations did not get rendered due to their size.