Skip to content

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

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

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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