Documentation

Lean.Server.Utils

def IO.throwServerError {α : Type} (err : String) :
IO α

Throws an IO.userError.

Equations
Instances For

    Chains two streams by creating a new stream s.t. writing to it just writes to a but reading from it also duplicates the read output into b, c.f. a | tee b on Unix. NB: if a is written to but this stream is never read from, the output will not be duplicated. Use this if you only care about the data that was actually read.

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

      Like tee a | b on Unix. See chainOut.

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

        Prefixes all written outputs with pre.

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

          Meta-Data of a document.

          • URI where the document is located.

          • version : Nat

            Version number of the document. Incremented whenever the document is edited.

          • Current text of the document. It is maintained such that it is normalized using String.crlfToLf, which preserves logical line/column numbers. (Note: we assume that edit operations never split or merge \r\n line endings.)

          • dependencyBuildMode : Lean.Lsp.DependencyBuildMode

            Controls when dependencies of the document are built on textDocument/didOpen notifications.

          Instances For
            Equations

            Extracts an InputContext from doc.

            Equations
            • doc.mkInputContext = { input := doc.text.source, fileName := ((System.Uri.fileUriToPath? doc.uri).getD { toString := doc.uri }).toString, fileMap := doc.text }
            Instances For

              Replaces the range r (using LSP UTF-16 positions) in text (using UTF-8 positions) with newText.

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

                Duplicates an I/O stream to a log file fName in LEAN_SERVER_LOG_DIR if that envvar is set.

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

                  Returns the document contents with the change applied.

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

                    Returns the document contents with all changes applied.

                    Equations
                    Instances For

                      Constructs a textDocument/publishDiagnostics notification.

                      Equations
                      Instances For

                        Constructs a $/lean/fileProgress notification.

                        Equations
                        Instances For

                          Constructs a $/lean/fileProgress notification from the given position onwards.

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

                              Converts an UTF-8-based String.range in text to an equivalent LSP UTF-16-based Lsp.Range in text.

                              Equations
                              Instances For

                                Attempts to find a module name in the roots denoted by srcSearchPath for uri. Fails if uri is not a file:// uri or if the given uri cannot be found in srcSearchPath.

                                Equations
                                Instances For