Documentation

Lean.Server.Utils

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

Throws an IO.userError.

Equations
    Instances For
      def IO.FS.Stream.chainRight (a b : Stream) (flushEagerly : Bool := false) :

      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
        Instances For
          def IO.FS.Stream.chainLeft (a b : Stream) (flushEagerly : Bool := false) :

          Like tee a | b on Unix. See chainOut.

          Equations
            Instances For

              Prefixes all written outputs with pre.

              Equations
                Instances For

                  Meta-Data of a document.

                  • URI where the document is located.

                  • mod : Name

                    Module name corresponding to uri. We store the module name instead of recomputing it as needed to ensure that we can still determine the original module name even when the file has been deleted in the mean-time.

                  • version : Nat

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

                  • text : FileMap

                    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 : Lsp.DependencyBuildMode

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

                  Instances For

                    Extracts an InputContext from doc.

                    Equations
                      Instances For

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

                        Equations
                          Instances For

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

                            Equations
                              Instances For

                                Returns the document contents with the change applied.

                                Equations
                                  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
                                                  Instances For

                                                    Constructs a $/lean/fileProgress notification marking processing as done.

                                                    Equations
                                                      Instances For

                                                        Finds the URI corresponding to modName in searchSearchPath. Yields none if the file corresponding to modName has been deleted in the mean-time.

                                                        Equations
                                                          Instances For

                                                            Finds the module name corresponding to uri in srcSearchPath.

                                                            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