Documentation

Lean.Data.Lsp.Utf16

LSP uses UTF-16 for indexing, so we need to provide some primitives to interact with Lean strings using UTF-16 indices.

Equations
  • c.utf16Size = if c.val 65535 then 1 else 2
Instances For
    Equations
    Instances For

      Computes the UTF-16 offset of the n-th Unicode codepoint in the substring of s starting at UTF-8 offset off. Yes, this is actually useful.

      Equations
      Instances For
        Equations
        • s.codepointPosToUtf16Pos pos = s.codepointPosToUtf16PosFrom pos 0
        Instances For

          Computes the position of the Unicode codepoint at UTF-16 offset utf16pos in the substring of s starting at UTF-8 offset off.

          Equations
          Instances For
            Equations
            • s.utf16PosToCodepointPos pos = s.utf16PosToCodepointPosFrom pos 0
            Instances For

              Starting at utf8pos, finds the UTF-8 offset of the p-th codepoint.

              Equations
              • s.codepointPosToUtf8PosFrom x 0 = x
              • s.codepointPosToUtf8PosFrom x p.succ = s.codepointPosToUtf8PosFrom (s.next x) p
              Instances For

                Computes an UTF-8 offset into text.source from an LSP-style 0-indexed (ln, col) position.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • text.leanPosToLspPos { line := line, column := col } = { line := line - 1, character := text.source.codepointPosToUtf16PosFrom col (Lean.FileMap.lineStartPos text (line - 1)) }
                  Instances For
                    Equations
                    • text.utf8PosToLspPos pos = text.leanPosToLspPos (text.toPosition pos)
                    Instances For

                      Gets the LSP range from a String.Range.

                      Equations
                      • text.utf8RangeToLspRange range = { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
                      Instances For

                        Convert the Lean DeclarationRange to an LSP Range by turning the 1-indexed line numbering into a 0-indexed line numbering and converting the character offset within the line to a UTF-16 indexed offset.

                        Equations
                        • r.toLspRange = { start := { line := r.pos.line - 1, character := r.charUtf16 }, «end» := { line := r.endPos.line - 1, character := r.endCharUtf16 } }
                        Instances For