Email Gateway (Aug 05 2023 at 03:01): Email Gateway (Aug 05 2023 at 03:01):From: Jimmy Situ <web@jimmystone.cn>
Hi, All
I want to install the Isabelle 2022 vscode extension but it reports the extension is not compatible with VS Code 1.78.2
Then I check the package.json in source code in the following link,
https://isabelle.in.tum.de/repos/isabelle/file/53b59fa42696/src/Tools/VSCode/extension/package.json#l20
It seems only support 1.70.1. Is it compatible with a later version of vscode?
Changing
"vscode": "1.70.1"
to
"vscode": "^1.70.1"
is better for compatible later version vscode?
Thanks
Jimmy Situ
Email Gateway (Aug 07 2023 at 08:19):From: Fabian Huch <huch@in.tum.de>
The extension in the extension marketplace is no longer supported,
instead you can start Isabelle/VScode directly from isabelle (see
'isabelle vscode -?').
Fabian
Email Gateway (Aug 07 2023 at 08:38):From: Mario Carneiro <di.gama@gmail.com>
Drive-by comment, but: why is this? I use many different languages from
vscode and I don't want to be using a separate mechanism just to start
"isabelle/vscode". It sounds like a path back to the jedit days, I don't
want the proof assistant controlling the editor lifetime.
Email Gateway (Aug 07 2023 at 09:07):From: Fabian Huch <huch@in.tum.de>
The VScode plugin interfaces are not sufficient. Hence, for a proper
integration, you do want that.
Also, Isabelle/VScode is not meant as a replacement for Isabelle/jEdit,
it's merely there for different purposes (e.g., accessibility).
Fabian
Email Gateway (Aug 07 2023 at 09:53):From: Mario Carneiro <di.gama@gmail.com>
On Mon, Aug 7, 2023 at 5:06 AM Fabian Huch <huch@in.tum.de> wrote:
The VScode plugin interfaces are not sufficient. Hence, for a proper
integration, you do want that.I am curious to hear more about these things. I have seen some pretty
advanced things done in vscode plugins, so I would like to know what kind
of thing is not possible, especially if it is possible to do if isabelle
starts vscode rather than vice versa. Or is isabelle shipping a patched
version of vscode?
Also, Isabelle/VScode is not meant as a replacement for Isabelle/jEdit,
it's merely there for different purposes (e.g., accessibility).Accessibility to whom? I don't see why it is necessary to declare at the
outset that your plugin only targets second-class support, rather than it
being a known issue that we would like to fix (which I can certainly
believe is the case). What are the barriers to using Isabelle/VScode "as a
replacement for Isabelle/jEdit"?
Mario
Email Gateway (Aug 07 2023 at 10:35):From: Mario Carneiro <di.gama@gmail.com>
Yes, I'm aware of the technical use of this term. But it is nevertheless
strange to me to be saying that you are developing a proof assistant
interface which is exclusively for use by blind people. And the question
remains: why was the plugin mode deprecated?
Email Gateway (Aug 07 2023 at 10:39):From: Fabian Huch <huch@in.tum.de>
I am curious to hear more about these things. I have seen some pretty
advanced things done in vscode plugins, so I would like to know what
kind of thing is not possible
For example, file encoding -- a number of workarounds have been tried
but induced their own problems.
Or is isabelle shipping a patched version of vscode?
Yes.
Fabian
Email Gateway (Aug 07 2023 at 10:41):From: Makarius <makarius@sketis.net>
Isabelle is indeed the master over the editor, not the other way round. We did
not do this at the start, e.g. with Proof General / Emacs in 1998: In those
archaic times there were constantly problems coming from the non-integration
of the prover and the editor.
Since 2008, our requirement is to make everything just work, without manual
intervention by the user. This requires to "pin" versions, in order to reduce
the space of variation to just 1.
Moreover, Isabelle/VSCode requires a patched version of VSCod(ium) --- just
like Isabelle/jEdit requires a patched version of jEdit.
So indeed, there is only one version of VSCode that Isabelle/VSCode can use:
the one that is bundled with Isabelle. (I will see if I can update that for
Isabelle2023 within the next 2-3 days.)
People who don't like that approach should be honest and don't use it.
Makarius
Email Gateway (Aug 07 2023 at 10:51):From: Walther Neuper <cl-isabelle-users@lists.cam.ac.uk>
Here accessibility is meant in a specific sense:
https://www.w3.org/WAI/fundamentals/accessibility-intro/
https://www.chromium.org/developers/design-documents/accessibility
And there are some publications about Isabelle/VSCode with respect to accessibility:
https://files.sketis.net/Isabelle_Workshop_2022/Isabelle_2022_paper_7.pdf
https://files.sketis.net/Isabelle_Workshop_2022/Isabelle_2022_paper_8.pdf
https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?Thedu22.8.pdf
https://static.miraheze.org/isacwiki/d/d0/IICHP-Paper.pdf
Email Gateway (Aug 07 2023 at 10:53):From: Makarius <makarius@sketis.net>
Presently, Isabelle/VSCode is merely an experimental PIDE front-end, while
Isabelle/jEdit is the real thing.
Isabelle/VSCode might point into a possible future, but it will require a lot
of work to get it on par with Isabelle/jEdit.
Accessibility is indeed a motivation for that, because VSCode (Chromium,
Electron) do support that reasonably well, while jEdit (Java Swing) does not
and never will.
The more Isabelle/VSCode progresses, the more we will rely on a particular
version (and patches for it).
The bundled versions from Isabelle2022 documents the changes as follows in its
README:
"""
This is VSCodium 1.70.1 from https://github.com/VSCodium/vscodium.git
It has been built from sources using "isabelle build_vscodium". This applies
a few changes required for Isabelle/VSCode, see "patches" directory for a
formal record.
"""
Makarius
Email Gateway (Aug 07 2023 at 10:53):From: Fabian Huch <huch@in.tum.de>
It is certainly not exclusive -- the whole purpose is to be inclusive,
and with the small restriction of using the bundled vscode, you can
certainly use it for other purposes (some people like to use
Isabelle/VScode for its vim keybindings plugin).
But development/maintenance capabilities are finite, and Isabelle/VScode
is not intended to replace Isabelle/jEdit.
Fabian
Email Gateway (Aug 07 2023 at 11:21):From: Mario Carneiro <di.gama@gmail.com>
On Mon, Aug 7, 2023 at 6:53 AM Fabian Huch <huch@in.tum.de> wrote:
But development/maintenance capabilities are finite, and Isabelle/VScode
is not intended to replace Isabelle/jEdit.
Right, this is exactly why it seems that incorporating vscode into isabelle
will always result in a sub-par vscode experience because you will not be
able to keep up with upstream development and will forever be shipping
outdated versions. Using a plugin solves that issue.
I'm reading the contents of
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Tools/VSCode/patches/
now to try to understand what specifically you need from the editor that
requires the base executable to be changed. It seems the main issue is the
fact that isabelle uses a non-standard text encoding. Do I understand
correctly that the utf8_decoder implemented in isabelle_encoding.ts is just
transcoding the files into UTF8? Maybe this encoding could be upstreamed to
vscode, or the extension could contribute a new encoding to the encodings
list. Is there an open issue upstream about this?
On Mon, Aug 7, 2023 at 6:53 AM Makarius <makarius@sketis.net> wrote:
Presently, Isabelle/VSCode is merely an experimental PIDE front-end, while
Isabelle/jEdit is the real thing.Isabelle/VSCode might point into a possible future, but it will require a
lot
of work to get it on par with Isabelle/jEdit.
This is a perfectly reasonable stance, as long as one keeps the path open
for it to become better.
The more Isabelle/VSCode progresses, the more we will rely on a particular
version (and patches for it).
Needless to say, this is going to cause a lock-out effect because people
can't use the editors they prefer to use.
On Mon, Aug 7, 2023 at 6:41 AM Makarius <makarius@sketis.net> wrote:
Isabelle is indeed the master over the editor, not the other way round. We
did
not do this at the start, e.g. with Proof General / Emacs in 1998: In
those
archaic times there were constantly problems coming from the
non-integration
of the prover and the editor.
Since 2008, our requirement is to make everything just work, without
manual
intervention by the user. This requires to "pin" versions, in order to
reduce
the space of variation to just 1.
I will usually take imperfect integration (e.g. just syntax highlighting)
of my preferred editor over a heavyweight all-in-one solution that doesn't
play well with any of my other tools. (At least you aren't shipping an
OS... yet.) But that's just my preference, and you make it very clear where
I should take my opinions.
What is the last working version of the extension? Perhaps someone else
could keep it alive, imperfect as it is.
Email Gateway (Aug 07 2023 at 11:51):From: Makarius <makarius@sketis.net>
On 07/08/2023 13:21, Mario Carneiro wrote:
On Mon, Aug 7, 2023 at 6:53 AM Fabian Huch <huch@in.tum.de
<mailto:huch@in.tum.de>> wrote:But development/maintenance capabilities are finite, and Isabelle/VScode
is not intended to replace Isabelle/jEdit.Right, this is exactly why it seems that incorporating vscode into isabelle
will always result in a sub-par vscode experience because you will not be able
to keep up with upstream development and will forever be shipping outdated
versions. Using a plugin solves that issue.
Well, there is a fundamental cultural mismatch: VSCode follows the paradigm
"latest is greatest", but that requires a lot of real-time resources to
maintain its many parts. (It ultimately does not work, as I've experienced
many times before, e.g. with Haskell or Scala extensions).
In congtrast to that, Isabelle is about making each release a static closure
of the best we could do at release time. That means all contributing
components will remain unchanged.
(Again: We did not start with that attitude initially. In the wild old days,
we did it like many other projects out there, and delivered much less quality.)
I'm reading the contents of
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Tools/VSCode/patches/ <https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Tools/VSCode/patches/> now to try to understand what specifically you need from the editor that requires the base executable to be changed. It seems the main issue is the fact that isabelle uses a non-standard text encoding. Do I understand correctly that the utf8_decoderimplemented in isabelle_encoding.ts is just transcoding the files into UTF8? Maybe this encoding could be upstreamed to vscode, or the extension could contribute a new encoding to the encodings list. Is there an open issue upstream about this?
Apart from the Isabelle encoding there are also Isabelle fonts: both need to
fit together exactly.
There are further fine points to fit the editor into the Isabelle system
environment, such that Isabelle settings and options have priority.
I can explain further details after the Isabelle2023 is finished, lets say in
approx. 2 weeks.
Presently, the time is for testing release candidates, including
Isabelle/VSCode (which I have not updated since Isabelle2022 so far).
See also
https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023
for the release train, which is progressing towards a single final release of
Isabelle with its many bundled tools. (There are no post-release patches, so
everything needs to be right in the end.)
Makarius
Email Gateway (Sep 12 2023 at 18:21):From: Makarius <makarius@sketis.net>
Now the Isabelle2023 release has required more than 2 weeks. We have
accumulated a bit too much complexity, but in the end everything should fit
together properly --- on all platforms.
Some weeks ago, I did make some attempts to rebuild our bundled version
VSCode, but failed: the cross-build for Windows on Linux stopped working
shortly after our version 1.70.1. It is unclear if this is accidental or
intentional: there is plenty of time to investigate, and nothing is "broken"
in the meantime, because the bundled version works fine (nobody has reported
problems so far).
Concerning the motivation(s) to patch VSCode, here is a list in decreasing
order of importance:
1) Support for Isabelle text encoding as a mapping from Latex-style names
to Unicode points.
2) Support for Isabelle fonts that fit precisely for the Isabelle text
encoding and use high-quality glyphs from LaTeX.
3) Robust system integration: Everything should work on the spot, without
self-assembly or tinkering.
4) Provide side-entries to access the bundled components of VSCode
separately: Electron / Chromium / Node.js (see also
https://files.sketis.net/Isabelle_Workshop_2022/Isabelle_2022_paper_7.pdf)
More will come over time, as Isabelle/VSCode becomes a more serious contender
of Isabelle/jEdit, not just an experiment on alternative PIDE front-ends.
Of course, almost everything could be done differently. The Isabelle tradition
and culture predates most other cultures that we see today, so things might
look unusual (I would say: usually better).
Often there are also violations of what is today considered "standard" or
"essential". For example, the well-known text book on addictive software
design (from 2014) https://www.nirandfar.com/hooked says, that the "IKEA
principle" of self-assembly is important to make users feel attached to
"their" product that they have struggled to put together themselves.
I've dismissed that already in 2009, even using the same name "IKEA principle"
as something to be avoided. In German, the counter-principle is called "AEG"
(Auspacken -- Einstecken -- Geht): it means everything works immediately out
of the box.
Makarius
Email Gateway (Sep 12 2023 at 18:28):From: Makarius <makarius@sketis.net>
Just another side-remark for the very start of this mailing list thread:
"compatible later version" is merely an unproven claim of the idea of
"semantic versioning" that is so strongly emphasized in the Node.js and VSCode
communities.
Unfortunately, this concept does not hold its promise!
I was very open to it initially (around 2017), when working with VSCode for
the first time. Later I have seen it fail often and routinely.
In Isabelle we do it differently (and better): There is exactly one version of
every contributing component, and that is tested over several months to ensure
that it really works (on all platforms). There are no implicit updates of
seemingly "compatible" components. (Both Docker and NixOS follow a similar
approach.)
Makarius
Email Gateway (Sep 12 2023 at 19:52):From: Makarius <makarius@sketis.net>
Another important detail:
* Treat file-extension .ML as Isabelle/ML instead of OCaml --- which is
actually .ml, but VSCode is case-insensitive here (maybe due to its Windows
mindset).
This kind of totally adhoc patch has occurred in jEdit quite often. VSCode has
now joined the club, and more such Isabelle-specific things are to be expected
in the future.
Makarius
Email Gateway (Sep 13 2023 at 12:09):From: Makarius <makarius@sketis.net>
On 12/09/2023 22:31, Mario Carneiro wrote:
There is a problem in this reasoning: The user may have an arbitrary unknown
version of VSCode, but the downloaded Isabelle version (or its VSCode
extension) needs to work with it. How? By magic foreknowledge at Isabelle
release time? Or by constantly running after VSCode updates after an Isabelle
release?By not depending so deeply on unstable features that the code breaks all the
time.
In other words: not being too ambitious about the overall quality of the result.
We used to follow the above approach over some decades with Isabelle, but in
the past 10-15 years ambitions have increased a lot.
We skip the running-after part, and thus free a lot of maintenance resources
for other areas. There is only one version of everything that is supported.
And that is not in conflict with other versions of the same components that
might already be installed for other reasons.It is in conflict though, with other extensions people might have installed.
For Isabelle/VSCode it is rather simple: there is no conflict with whatever
other VSCode version you might have. It is just a disjoint world on its own.
For some context/comparison, while I am undoubtedly on the "power user" end of
the spectrum, I apparently have 84 extensions installed, including 31
programming languages (yes, I installed each one deliberately due to some task
I was working on), 6 themes, and 7 ITP languages, of which Isabelle is one.
So are you using Isabelle on VSCode seriously?
I've heard rumors that a few Isabelle users have managed to use it
productively, although I find it hard to believe: Isabelle/VSCode is still a
small experiment, and not a proper Prover IDE yet.
Isabelle is far from the only language I use, and you can imagine why in such
a situation it is not so nice to be saying "yes but please use this version
of vscodium that doesn't support any of your other extensions, so that you can
live in the Isabelle world".
That is a misunderstanding. For using Isabelle, you merely need to use
Isabelle. E.g. Isabelle/jEdit or Isabelle/VSCode as front-end. There is no
overlap with other installations jEdit or VSCode.
In other words: the "operating system" underlying Isabelle is really just the
bare OS, not a pre-installed editor (Emacs, jEdit, VSCode, ...).
Listed as #4 it has rather low priority. Actually it had no priority when the
patch-business started. It was merely a nice corollary to have full
Chromium +
Node.js on all platforms in well-defined version. This will open
possibilities
for the future, e.g. for local Isabelle web applications that only need to
take a single browser version into account (not 20).I see you want to keep with the vendor lock-in effect.
I also don't like the predominance of the Chromium engine.
Over some decades, web browsers have promised "independence" that they never
delivered. In recent years, the situation has become particularly bad for
Firefox: Chromium has taken over a lot of its former territory.
For everyday web browsing, I now use both Firefox and Chromium, whichever
happens to work better. At some point, I might even have to retire Firefox.
For Isabelle, I don't want to see this browser non-compatibility problem at
all. If (or when) we do HTML things seriously, it will be for precisely one
browser engine: the one that is bundled with Isabelle.
Note that semantic versioning is a specific thing, just because a project has
version numbers doesn't mean it is using semantic versioning. Especially the
older projects, since semver only became popular around 2010 or so, so
anything older was probably already invested in its existing versioning system.
I encourage you to take a look at semver.org <http://semver.org>, it's a very
short and readable spec, but it is making a much more precise claim than
"things get better when numbers go up" which seemed to be the status quo from
2000's software. It is primarily about API compatibility, which makes it well
suited to ecosystems like npm modules.
I did take a close look and the "semver" specification around 2017 / 2018, and
gave these guys a huge bonus, assuming that reality fits to their promises.
This has failed. They don't hold up to our quality standards.
On Tue, Sep 12, 2023 at 3:52 PM Makarius <makarius@sketis.net
<mailto:makarius@sketis.net>> wrote:Another important detail:
* Treat file-extension .ML as Isabelle/ML instead of OCaml --- which is
actually .ml, but VSCode is case-insensitive here (maybe due to its Windows
mindset).I think it's more than just that - there are certainly Standard ML files and
OCaml files which use .ML extension. The fact is, file extensions are
hopelessly overloaded, so there isn't any choice but to pick some sensible
defaults and let the user make overrides if they have a special situation.
Now we are back to "IKEA" vs. "AEG". Isabelle follows the "AEG" approach.
Isabelle is also about being honest about technological reality and
side-conditions.
From the experience with VSCode in the past couple of years, I don't see
Isabelle returning into "extension space". That game is over.
Makarius
Email Gateway (Sep 13 2023 at 12:25):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I just wanted to add that I wrote thousands of lines Isabelle/HOL and
Isabelle/ML in VSCode and here my top 2 annoyances:
Jumping from one file to another one (e.g. using ctrl+click) and then
going back kills the syntax highlighting (until an arbitrary change to
the file is made; it then recovers).
Message formatting in the output panel is not working properly when
compared to jEdit (e.g. proof states).
But other than that, I'm much quicker in VSCode because I get to have
Vim keybindings :)
Kevin
Email Gateway (Sep 14 2023 at 00:16):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am not a VSCode user (I am mostly an Emacs dinosaur), but as a result of this thread I got the idea
to fire up Isabelle/VSCode. The first thing I noticed (to my dismay) was that the color scheme is completely
different from the Isabelle/JEdit color scheme, both for light and dark themes. Is there any good reason for
this? After a number of years of using Isabelle/JEdit, my brain is now hard-wired to recognize the subtle
color changes that indicate free variables and so on. Is there an easy way to load a file that sets
the color scheme used in the Isabelle/JEdit light theme? I don't really feel like converting a bunch
of hex RGB codes to decimal and entering them in the preferences window of VSCode.
The other thing I noticed is that when selecting "Document" display the syntax coloring only extended
by about one window's worth of code and it would not color the rest even when I scrolled down into it.
I should mention that I typically use Isabelle via remote desktop to a headless system, and I do observe
some glitches involving window repaint, but I have typically not regarded them as Isabelle's fault.
Email Gateway (Sep 14 2023 at 07:08):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
On 9/13/23 14:08, Makarius wrote:
I've heard rumors that a few Isabelle users have managed to use it
productively, although I find it hard to believe: Isabelle/VSCode is
still a small experiment, and not a proper Prover IDE yet.
I work with Isabelle/jEdit to work on having a "smt (cvc5)" tactic and I
use the LSP protocol for my own Isabelle development (so I have the bad
"Prover IDE" experience too). Here is my experience with Isabelle/jEdit:
It does not respect keybindings (on my alternative French keyboard,
the keybindings are those of the normal French keyboard…
inconsistently however). I know at least one other user who faced
the same issue in the past.
It freezes on a regular basis (several times a day). When frozen,
the autosave function does not work anymore.
It crashes regularly during freezing (more than once a day), losing
work each time (autosave does not work and keybindings for save do
not work and saving with the mouse does not work anymore)
Copy-paste does not work consistently (I resorted to press it 3
times and hope for each copying)
I have to use the mouse to find the windows (like the search window
that does not get the focus when covered by another window)
The current position in the buffers (like the output buffer) is not
saved and lost, so I have to search again for what I was currently
looking. And search does not work there (yes, there is something
called "search", but it is only a highlighting box that takes some
kind of regexp as input, making it useless to search for terms)
None of these issues is new, nor is a regression over the last Isabelle
version… and still this is now how I image the AEG principle at all.
Overall, my choice is between a bad "Prover IDE" experience and a bad
text-editor experience. I picked the former, as working around
limitations is possible.
Mathias
Isabelle is far from the only language I use, and you can imagine why
in such a situation it is not so nice to be saying "yes but please
use this version of vscodium that doesn't support any of your other
extensions, so that you can live in the Isabelle world".That is a misunderstanding. For using Isabelle, you merely need to use
Isabelle. E.g. Isabelle/jEdit or Isabelle/VSCode as front-end. There
is no overlap with other installations jEdit or VSCode.In other words: the "operating system" underlying Isabelle is really
just the bare OS, not a pre-installed editor (Emacs, jEdit, VSCode, ...).Listed as #4 it has rather low priority. Actually it had no
priority when the
patch-business started. It was merely a nice corollary to have full
Chromium +
Node.js on all platforms in well-defined version. This will open
possibilities
for the future, e.g. for local Isabelle web applications that
only need to
take a single browser version into account (not 20).I see you want to keep with the vendor lock-in effect.
I also don't like the predominance of the Chromium engine.
Over some decades, web browsers have promised "independence" that they
never delivered. In recent years, the situation has become
particularly bad for Firefox: Chromium has taken over a lot of its
former territory.For everyday web browsing, I now use both Firefox and Chromium,
whichever happens to work better. At some point, I might even have to
retire Firefox.For Isabelle, I don't want to see this browser non-compatibility
problem at all. If (or when) we do HTML things seriously, it will be
for precisely one browser engine: the one that is bundled with Isabelle.Note that semantic versioning is a specific thing, just because a
project has version numbers doesn't mean it is using semantic
versioning. Especially the older projects, since semver only became
popular around 2010 or so, so anything older was probably already
invested in its existing versioning system.I encourage you to take a look at semver.org <http://semver.org>,
it's a very short and readable spec, but it is making a much more
precise claim than "things get better when numbers go up" which
seemed to be the status quo from 2000's software. It is primarily
about API compatibility, which makes it well suited to ecosystems
like npm modules.I did take a close look and the "semver" specification around 2017 /
2018, and gave these guys a huge bonus, assuming that reality fits to
their promises.This has failed. They don't hold up to our quality standards.
>
On Tue, Sep 12, 2023 at 3:52 PM Makarius <makarius@sketis.net
<mailto:makarius@sketis.net>> wrote:
Another important detail:
* Treat file-extension .ML as Isabelle/ML instead of OCaml
--- which is
actually .ml, but VSCode is case-insensitive here (maybe due to
its Windows
mindset).I think it's more than just that - there are certainly Standard ML
files and OCaml files which use .ML extension. The fact is, file
extensions are hopelessly overloaded, so there isn't any choice but
to pick some sensible defaults and let the user make overrides if
they have a special situation.Now we are back to "IKEA" vs. "AEG". Isabelle follows the "AEG" approach.
Isabelle is also about being honest about technological reality and
side-conditions.From the experience with VSCode in the past couple of years, I don't
see Isabelle returning into "extension space". That game is over.Makarius
Email Gateway (Oct 02 2023 at 17:31):From: Makarius <makarius@sketis.net>
On 9/14/23 09:08, Mathias Fleury wrote:
I work with Isabelle/jEdit to work on having a "smt (cvc5)" tactic and I
use the LSP protocol for my own Isabelle development (so I have the bad
"Prover IDE" experience too). Here is my experience with Isabelle/jEdit:[1..6]
None of these issues is new, nor is a regression over the last Isabelle
version… and still this is now how I image the AEG principle at all.
That sounds all very bad. You have occasionally told me about a few of
these observations, but not the whole list.
There must be something very special in your OS setup that is preventing
the "AEG" experience. I probably need to see it first hand eventually.
Makarius
Email Gateway (Oct 02 2023 at 17:37):From: Makarius <makarius@sketis.net>
On 9/14/23 02:16, Eugene W. Stark wrote:
I am not a VSCode user (I am mostly an Emacs dinosaur), but as a result of this thread I got the idea
to fire up Isabelle/VSCode. The first thing I noticed (to my dismay) was that the color scheme is completely
different from the Isabelle/JEdit color scheme, both for light and dark themes. Is there any good reason for
this?
No, the main reason is just historical accidence. The jEdit text editor
had a very good "light" theme when the distinction of "light" vs. "dark"
did not exist. VSCode is quite different themes.
My plan is to unify this eventually:
* refine the traditional Isabelle/jEdit color scheme into something
that can be used as "light theme" for both Isabelle/jEdit and
Isabelle/VSCode
* find a VSCode "dark" scheme that can be turned into a uniform one
for both editors
That would be one more step away from the "experimental" status of
Isabelle/VSCode.
The other thing I noticed is that when selecting "Document" display the syntax coloring only extended
by about one window's worth of code and it would not color the rest even when I scrolled down into it.
I should mention that I typically use Isabelle via remote desktop to a headless system, and I do observe
some glitches involving window repaint, but I have typically not regarded them as Isabelle's fault.
I am unsure what you mean exactly. Note that scrolling events are not
exposed to VSCode extensions (at least that was the state some years
ago). Only actual cursor movement counts for the display engine.
(Maybe that is another motivation for funny patches to the VSCodium code
base, although it makes me feel uneasy already.)
Makarius
Email Gateway (Oct 04 2023 at 12:24):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Just to provide a record of what I was talking about, see the attached screenshot.
I got there by opening the theory file, selecting the "Preview" mode using an icon at the
upper right, and then scrolling down by one-half a view. You can see that the upper half
of the view is colored and the lower half is not. Clicking the mouse on the uncolored portion
does not cause any change.
Screenshot from 2023-10-04 08-16-56.png
Last updated: Apr 29 2024 at 04:18 UTC