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.

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.

instance ProofWidgets.instFromJsonMakeEditLinkProps : Lean.FromJson MakeEditLinkProps

instance ProofWidgets.instToJsonMakeEditLinkProps : Lean.ToJson MakeEditLinkProps

def ProofWidgets.MakeEditLinkProps.ofReplaceRange' (meta : 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.

def ProofWidgets.MakeEditLinkProps.ofReplaceRange (meta : 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'.

def ProofWidgets.MakeEditLink : Component MakeEditLinkProps

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