Lean.Server.Utils

source

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

IO α

Equations

IO.throwServerError err = throw (IO.userError err)

source

def IO.FS.Stream.chainRight (a : IO.FS.Stream) (b : IO.FS.Stream) (flushEagerly : optParam Bool false) :

IO.FS.Stream

Equations

IO.FS.Stream.chainRight a b flushEagerly = { isEof := a.isEof, flush := SeqRight.seqRight a.flush fun x => b.flush, read := fun sz => do let bs ← IO.FS.Stream.read a sz IO.FS.Stream.write b bs let _do_jp : Unit → IO ByteArray := fun y => pure bs if flushEagerly = true then do let y ← b.flush _do_jp y else do let y ← pure PUnit.unit _do_jp y, write := a.write, getLine := do let ln ← a.getLine IO.FS.Stream.putStr b ln let _do_jp : Unit → IO String := fun y => pure ln if flushEagerly = true then do let y ← b.flush _do_jp y else do let y ← pure PUnit.unit _do_jp y, putStr := a.putStr }

source

def IO.FS.Stream.chainLeft (a : IO.FS.Stream) (b : IO.FS.Stream) (flushEagerly : optParam Bool false) :

IO.FS.Stream

Equations

IO.FS.Stream.chainLeft a b flushEagerly = { isEof := b.isEof, flush := SeqRight.seqRight a.flush fun x => b.flush, read := b.read, write := fun bs => do IO.FS.Stream.write a bs let _do_jp : Unit → IO Unit := fun y => IO.FS.Stream.write b bs if flushEagerly = true then do let y ← a.flush _do_jp y else do let y ← pure PUnit.unit _do_jp y, getLine := b.getLine, putStr := fun s => do IO.FS.Stream.putStr a s let _do_jp : Unit → IO Unit := fun y => IO.FS.Stream.putStr b s if flushEagerly = true then do let y ← a.flush _do_jp y else do let y ← pure PUnit.unit _do_jp y }

source

def IO.FS.Stream.withPrefix (a : IO.FS.Stream) (pre : String) :

IO.FS.Stream

Equations

IO.FS.Stream.withPrefix a pre = { isEof := a.isEof, flush := a.flush, read := a.read, write := fun bs => do IO.FS.Stream.putStr a pre IO.FS.Stream.write a bs, getLine := a.getLine, putStr := fun s => IO.FS.Stream.putStr a (pre ++ s) }

source

def Lean.Lsp.DocumentUri.ofPath (fname : System.FilePath) :

Lean.Lsp.DocumentUri

Equations

Lean.Lsp.DocumentUri.ofPath fname = let fname := (System.FilePath.normalize fname).toString; let fname := if System.Platform.isWindows = true then String.map (fun c => if (c == Char.ofNat 92) = true then Char.ofNat 47 else c) fname else fname; "file:///" ++ String.dropWhile fname fun a => a == Char.ofNat 47

source

def Lean.Lsp.DocumentUri.toPath? (uri : Lean.Lsp.DocumentUri) :

Option System.FilePath

Equations

Lean.Lsp.DocumentUri.toPath? uri = Id.run (let _do_jp := fun y => let p := String.drop uri (String.length "file://"); let _do_jp := fun p y => some { toString := p }; if System.Platform.isWindows = true then let p := String.map (fun c => if (c == Char.ofNat 47) = true then Char.ofNat 92 else c) p; do let y ← pure PUnit.unit _do_jp p y else do let y ← pure PUnit.unit _do_jp p y; if (!String.startsWith uri "file:///") = true then pure none else do let y ← pure PUnit.unit _do_jp y)

source

structure Lean.Server.DocumentMeta :

Type

uri : Lean.Lsp.DocumentUri
version : Nat
text : Lean.FileMap

source

instance Lean.Server.instInhabitedDocumentMeta :

Inhabited Lean.Server.DocumentMeta

Equations

Lean.Server.instInhabitedDocumentMeta = { default := { uri := default, version := default, text := default } }

source

def Lean.Server.replaceLspRange (text : Lean.FileMap) (r : Lean.Lsp.Range) (newText : String) :

Lean.FileMap

Equations

Lean.Server.replaceLspRange text r newText = let start := Lean.FileMap.lspPosToUtf8Pos text r.start; let end := Lean.FileMap.lspPosToUtf8Pos text r.end; let pre := String.extract text.source 0 start; let post := String.extract text.source end (String.bsize text.source); String.toFileMap (pre ++ newText ++ post)

source

def Lean.Server.maybeTee (fName : String) (isOut : Bool) (h : IO.FS.Stream) :

IO IO.FS.Stream

Equations

Lean.Server.maybeTee fName isOut h = do let a ← liftM (IO.getEnv "LEAN_SERVER_LOG_DIR") match a with | none => pure h | some logDir => do IO.FS.createDirAll { toString := logDir } let hTee ← IO.FS.Handle.mk (System.mkFilePath [logDir, fName]) IO.FS.Mode.write true let hTee : IO.FS.Stream := IO.FS.Stream.ofHandle hTee pure (if isOut = true then IO.FS.Stream.chainLeft hTee h true else IO.FS.Stream.chainRight h hTee true)

source

def Lean.Server.applyDocumentChange (oldText : Lean.FileMap) (change : Lean.Lsp.TextDocumentContentChangeEvent) :

Lean.FileMap

Equations

Lean.Server.applyDocumentChange oldText x = match x with | Lean.Lsp.TextDocumentContentChangeEvent.rangeChange range newText => Lean.Server.replaceLspRange oldText range newText | Lean.Lsp.TextDocumentContentChangeEvent.fullChange newText => String.toFileMap newText

source

def Lean.Server.foldDocumentChanges (changes : Array Lean.Lsp.TextDocumentContentChangeEvent) (oldText : Lean.FileMap) :

Lean.FileMap

Equations

Lean.Server.foldDocumentChanges changes oldText = Array.foldl Lean.Server.applyDocumentChange oldText changes 0 (Array.size changes)

source

def Lean.Server.publishDiagnostics (m : Lean.Server.DocumentMeta) (diagnostics : Array Lean.Lsp.Diagnostic) (hOut : IO.FS.Stream) :

IO Unit

Equations

Lean.Server.publishDiagnostics m diagnostics hOut = IO.FS.Stream.writeLspNotification hOut { method := "textDocument/publishDiagnostics", param := { uri := m.uri, version? := some (Int.ofNat m.version), diagnostics := diagnostics } }

source

def Lean.Server.publishProgress (m : Lean.Server.DocumentMeta) (processing : Array Lean.Lsp.LeanFileProgressProcessingInfo) (hOut : IO.FS.Stream) :

IO Unit

Equations

Lean.Server.publishProgress m processing hOut = IO.FS.Stream.writeLspNotification hOut { method := "$/lean/fileProgress", param := { textDocument := { uri := m.uri, version? := some m.version }, processing := processing } }

source

def Lean.Server.publishProgressAtPos (m : Lean.Server.DocumentMeta) (pos : String.Pos) (hOut : IO.FS.Stream) (kind : optParam Lean.Lsp.LeanFileProgressKind Lean.Lsp.LeanFileProgressKind.processing) :

IO Unit

Equations

Lean.Server.publishProgressAtPos m pos hOut kind = Lean.Server.publishProgress m #[{ range := { start := Lean.FileMap.utf8PosToLspPos m.text pos, end := Lean.FileMap.utf8PosToLspPos m.text (String.bsize m.text.source) }, kind := kind }] hOut

source

def Lean.Server.publishProgressDone (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) :

IO Unit

Equations

Lean.Server.publishProgressDone m hOut = Lean.Server.publishProgress m #[] hOut

source

def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) :

Lean.Lsp.Range

Equations

String.Range.toLspRange text r = { start := Lean.FileMap.utf8PosToLspPos text r.start, end := Lean.FileMap.utf8PosToLspPos text r.stop }