Entering special symbols in Isabelle/VSCode · General

I just started using Isabelle/VSCode and quickly ran into my first problem: I often don’t know how to enter special symbols. Outside of terms, shortcuts that don’t start with a backslash, like ==> for ⟹ and << for ‹ don’t work, and inside terms, not even those that start with a backslash work (a completion window just won’t pop up). Any hints on what to do about that?

Wolfgang Jeltsch (Jan 05 2023 at 03:55):

After quite a lot of trying and searching the web, I at least found that pressing Ctrl + Space will bring up the completion window also when entering terms. It’s certainly annoying having to press this key combination every time you enter a non-ASCII character in a term, but it makes it at least possible to use Isabelle/VSCode.

What I still couldn’t get working is auto-completion of abbreviations like ==>, so that I’m currently forced to enter things like \L⟨Ctrl+Space⟩⟨Return⟩ongr instead.

Wolfgang Jeltsch (Jan 05 2023 at 04:00):

@Denis Paluca, I see you’re in this Zulip space as well. Based on your bachelor thesis, I understand that you’ve implemented the current completion technology. If you could help me getting it working, I’d be extremely thankful. :pray:

Kevin Kappelmann (Jan 09 2023 at 07:49):

Hi Wolfgang, you can use Snippets to configure such - and much more complex - shortcuts. It is worth taking a couple of minutes to read the website I linked. For example, here are some snippets that I use for Isabelle:

    "Long right arrow": {
        "prefix": ["==>", "Long right arrow"],
        "body": ["⟹"],
        "description": "Long right arrow"
    },
    "ML": {
        "prefix": ["ML", "ml"],
        "body": ["ML‹", "\t$0", "›"],
        "description": "Open ML environment"
    },
    "cartouches": {
        "prefix": ["cartouches"],
        "body": ["‹$1› $0"],
        "description": "Open cartouches"
    },
    "subscripts": {
        "prefix": ["subscripts", "_"],
        "body": ["⇘$1⇙ $0"],
        "description": "Open subscripts"
    }

Note that $<number> can be used for jump markers. Triggering a snippet will move your cursor to the first jump marker. Pressing <tab> will move the cursor to the next jump marker.

Kevin Kappelmann (Jan 09 2023 at 07:58):

Talking about special characters, completion, etc., here are some user settings of mine that may further improve your user experience. (the first line is deliberately disabled)

{
    // "editor.fontFamily": "'Isabelle DejaVu Sans Mono",
    "editor.unicodeHighlight.ambiguousCharacters": false,
    "terminal.integrated.fontFamily": "monospace",
    "editor.tabSize": 2,
    "editor.minimap.enabled": false,
    "files.trimTrailingWhitespace": true,
    "workbench.panel.defaultLocation": "right",
    "editor.acceptSuggestionOnEnter": "off",
    "editor.suggestOnTriggerCharacters": true,
    "editor.suggestSelection": "recentlyUsedByPrefix",
    "editor.quickSuggestions": {
        "other": true,
        "comments": true,
        "strings": true
    },
    "editor.wordBasedSuggestions": true,
    "editor.tabCompletion": "on",
    "workbench.editor.tabSizing": "shrink",
    "explorer.confirmDragAndDrop": false,
    "explorer.autoReveal": false,
    "editor.renderWhitespace": "none",
    "search.seedOnFocus": true
  }

Wolfgang Jeltsch (Jan 11 2023 at 02:47):

Thanks a lot for these elaborate answers, at which I have to take a deeper look later.

Regarding snippets, did I get this correctly that snippets are a VS Code feature, independent of Isabelle, and the problem I’m experiencing is because just no Isabelle-specific snippets are pre-configured?

Regarding the problem of completion lists not popping up in terms, is the source of the problem that such popups are not configured via editor.quickSuggestions for terms, which VS Code mistakes for strings, when appearing between quotation marks, and perhaps comments, when appearing between cartouches?

All in all, I interpret your answer that Isabelle/VSCode is capable of doing what I expected it to do, but is just not configured to do that by default. I wonder why that is. Is there a good reason for not enabling automatic completion popups in terms or not having the typical replacements pre-configured as snippets? I mean, Isabelle/jEdit does have the corresponding features out of the box. Is it because the bare VS Code is configured in a certain way by default? But this is not a vanilla VS Code, but a VS Code bundled with Isabelle; so it should have all that configuration out of the box.

Who should be asked for fixes for these things? Who is actually maintaining Isabelle/VSCode? Makarius? @Fabian Huch? @Denis Paluca?

To give interested people the view of an Isabelle/VSCode newcomer: This behavior can really be a showstopper. With virtually no documentation of Isabelle/VSCode (the only “documentation” I found was the command line to start it mentioned in the NEWS (!) file) and nothing on the web about these issues, you are more or less lost immediately. What kept me using Isabelle/VSCode was only that I use the Neo keyboard layout, which already provides a lot of the necessary special characters, and my ability to craft and use a custom X compose table for adding a few more such characters, combined with my eagerness to not touch jEdit again, because VS Code just looks so much nicer. I can vividly imagine that many other newcomers to Isabelle/VSCode will throw it away quickly after having figured out that in its default configuration it is essentially unusable. I’m not writing this to annoy people, but to provide those who are perhaps in some inner circles and therefore know all the tricks with the perspective of a newbie without access to the coffee room of the Logic and Verification Chair of TUM, in the hope that it helps making Isabelle/VSCode also usable for these users.

Mathias Fleury (Jan 11 2023 at 05:34):

I think that Makarius considers VSCode as "use it at your own risk" and that the lack on documentation is on purpose to avoid getting bugs

Mathias Fleury (Jan 11 2023 at 05:38):

Wolfgang Jeltsch (Jan 11 2023 at 15:01):

What’s considered the future of Isabelle/VSCode? My understanding so far has been that it is supposed to replace Isabelle/jEdit in the middle run. Is this the case, or is Isabelle/VSCode only considered a sort of alternative solution for freaks?

Is there anyone maintaining Isabelle/VSCode? What if someone has fixes for bugs or deficiencies, like the apparent lack of certain out-of-the-box input support? Will anyone accept patches, or will they be dismissed, because nobody wants to spend time on changing the official version?

Wolfgang Jeltsch (Jan 11 2023 at 15:14):

Hmm, one thing I’ve started wondering about is whether snippets are really the “official” way of getting Isabelle symbols from sequences like ==>. After all, Isabelle/VSCode is supposed to have this replacement feature described in @Denis Paluca’s thesis. This feature is apparently somehow present in the current Isabelle/VSCode version, given that it has a setting Isabelle: Replacement, where you can chose which unique abbreviations should be replaced (none, non-alphanumeric, or all).

The presence of this feature would explain why Isabelle/VSCode doesn’t come with a snippet configuration for special symbols: the intended way would be to not use snippets but this Isabelle replacement. @Kevin Kappelmann, did you configure snippets only because the Isabelle replacement feature didn’t work? And is anyone aware of a way to make the replacement feature work?

Kevin Kappelmann (Jan 11 2023 at 16:03):

I remember that at some point, we had the automatic replacement of symbols like =>. But there were some problems (e.g. it also replaced => in ML files) and I suppose it was thus later removed.

Wolfgang Jeltsch (Jan 11 2023 at 16:24):

Hmm, that would explain it. I mean it would be good to have a replacement feature that queries the Isabelle symbol database, so that you don’t have to configure your symbol replacements manually, but messing up ML code is probably a showstopper. @Fabian Huch, do you know whether there are plans to revive this feature in a corrected form at some point?

Fabian Huch (Jan 12 2023 at 09:30):

Isabelle/VSCode is mostly an experiment that is not on par with Isabelle/jEdit. Its main use is accessibility, as the VSCode platform provides interfaces e.g. for blind Mathematicians.
We did have better Symbol replacement back when Isabelle/VSCode was a VSCode plugin; you'll have to ask Makarius (or view the history) what got stripped again and why when VSCode was integrated into the Isabelle platform.
As for further development, I currently can't dedicate any resources to that, but if one is willing to contribute to VSCode then I'd be happy to incorporate that into the distribution.

Zixuan Fan (Jan 12 2023 at 09:40):

Just out of curiosity: how is Isabelle/VSCode different from a VSCode plugin? The only thing that I am sure is that VSCodium uses a different licence from the normal VSCode, hence some plugins are not available.

Fabian Huch (Jan 12 2023 at 10:03):

The VSCode plugin interface is not rich enough for seamless Isabelle integration, e.g., you can't create custom encodings. Hence Isabelle/VSCode is a patched VSCode version.

Wolfgang Jeltsch (Jan 13 2023 at 18:28):

Oh, it’s not just a language server, but a language server plus VS Code patches? Interesting! I didn’t know that.

I had hopes that with Isabelle/VSCode being available, it would be rather easy to create Isabelle support for Vim and Neovim, which support language server integration. Would that be possible in case it is possible to configure custom encodings for these editors, or is there more needed?

Stream: General

Topic: Entering special symbols in Isabelle/VSCode

Wolfgang Jeltsch (Jan 05 2023 at 01:49):