Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: invalid namespace completions #5322

Merged
merged 2 commits into from
Sep 13, 2024
Merged

fix: invalid namespace completions #5322

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
32854c1
fix: invalid namespace completions
mhuisi Sep 12, 2024
7dadb0c
test: fix broken test
mhuisi Sep 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion src/Lean/Environment.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1016,7 +1016,15 @@ private def registerNamePrefixes : Environment → Name → Environment

@[export lean_environment_add]
private def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
let env := registerNamePrefixes env cinfo.name
let name := cinfo.name
let env := match name with
| .str _ s =>
if s.get 0 == '_' then
-- Do not register namespaces that only contain internal declarations.
env
else
registerNamePrefixes env name
| _ => env
env.addAux cinfo

@[export lean_display_stats]
Expand Down
2 changes: 1 addition & 1 deletion tests/lean/stdio.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ out.putStrLn "print stdout"
let err ← IO.getStderr;
(err.putStr "print stderr" : IO Unit)

open usingIO IO
open IO

def test : IO Unit := do
FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do
Expand Down
Loading