Documentation

ProofWidgets.Component.MakeEditLink

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.
  • 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.

Instances For

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.

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.