fix: export more symbols needed by Verso (#4956)
This enables the Verso LSP server extensions to work.
This commit is contained in:
parent
b144107ed5
commit
bcbd7299e9
1 changed files with 7 additions and 2 deletions
|
|
@ -96,8 +96,13 @@ def shouldExport (n : Name) : Bool :=
|
|||
-- libleanshared to avoid Windows symbol limit
|
||||
!(`Lean.Compiler.LCNF).isPrefixOf n &&
|
||||
!(`Lean.IR).isPrefixOf n &&
|
||||
-- Lean.Server.findModuleRefs is used in Verso
|
||||
(!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs)
|
||||
-- Lean.Server.findModuleRefs is used in SubVerso, and the contents of RequestM are used by the
|
||||
-- full Verso as well as anything else that extends the LSP server.
|
||||
(!(`Lean.Server.Watchdog).isPrefixOf n) &&
|
||||
(!(`Lean.Server.ImportCompletion).isPrefixOf n) &&
|
||||
(!(`Lean.Server.Completion).isPrefixOf n)
|
||||
|
||||
|
||||
|
||||
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
|
||||
let ps := decl.params
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue