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
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions