Skip to content

Unicode file paths displayed as URI-encoded in the infoview #759

@kuotsanhsu

Description

@kuotsanhsu

Description

File paths with non-ASCII/special characters are displayed as percentage-encoded in the infoview. See the image in the next section.

Steps to Reproduce

  1. Create a Lean source file with non-ASCII characters, e.g. Gödel.lean.
  2. Open the file and the infoview.
Image

Versions

Lean info:

  • code --list-extensions --show-versions: leanprover.lean4@0.0.229
  • lean --version: Lean (version 4.29.0, arm64-apple-darwin24.6.0, commit 98dc76e3c0a9b856c9b98726b713fb04fab16740, Release)

VSCode info:

  • Version: 1.115.0 (Universal)
  • Commit: 41dd792b5e652393e7787322889ed5fdc58bd75b
  • Electron: 39.8.5
  • ElectronBuildId: 13703022
  • Chromium: 142.0.7444.265
  • Node.js: 22.22.1
  • V8: 14.2.231.22-electron.0
  • OS: Darwin arm64 25.3.0

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions