Email Gateway (Feb 12 2025 at 21:44): Email Gateway (Feb 12 2025 at 21:44):From: Makarius <makarius@sketis.net>
On 12/02/2025 22:23, Moritz Roos (via cl-isabelle-users Mailing List) wrote:
3. (Tested on Mac:) Shouldn't autocomplete prioritize a basically perfect match?
If writing "\or" one gets the following suggestions
\<^oracle_name>
\<^oracle_name><>
a_
o_
\or
This is the same both in Jedit and in Vscode.
In Jedit this isn't that big of a deal, because it will remember that one used
\or last time.
It is only annoying in Vscode because of:4. (Tested on Mac:) Isabelle/vscode doesn't seem to remember the last
autocompletes. It always gives the same output, ranking the perfect match \or
last.
(I am answering this part under a suitable subject.)
The completion mechanism in Isabelle/PIDE has a long history and has arrived
at a local optimum. Changing that would need to revisit many old questions,
and decision points in various directions.
It is indeed vital to have a proper completion history, as seen in
Isabelle/jEdit (this is the proper name and spelling of that product).
I can't say anything about Isabelle/VSCode right now, because I did not have
any time testing this experimental side-branch of Isabelle/PIDE.
Makarius
Email Gateway (Feb 13 2025 at 00:30):From: Moritz Roos <cl-isabelle-users@lists.cam.ac.uk>
I just found another odd thing:
in Isabelle/VSCode the autocomplete didn't seem to work if one had typed
an even number of characters after the backslash like "\al" for
"\alpha" etc. (works for "\a" and "alp" etc)
This seems to have been partly fixed, but is still the case with e.g.
the word "sledgehammer".
-Moritz
Am 12.02.2025 um 22:44 schrieb Makarius:
On 12/02/2025 22:23, Moritz Roos (via cl-isabelle-users Mailing List)
wrote:3. (Tested on Mac:) Shouldn't autocomplete prioritize a basically
perfect match?
If writing "\or" one gets the following suggestions
\<^oracle_name>
\<^oracle_name><>
a_
o_
\or
This is the same both in Jedit and in Vscode.
In Jedit this isn't that big of a deal, because it will remember that
one used \or last time.
It is only annoying in Vscode because of:4. (Tested on Mac:) Isabelle/vscode doesn't seem to remember the
last autocompletes. It always gives the same output, ranking the
perfect match \or last.(I am answering this part under a suitable subject.)
The completion mechanism in Isabelle/PIDE has a long history and has
arrived at a local optimum. Changing that would need to revisit many
old questions, and decision points in various directions.It is indeed vital to have a proper completion history, as seen in
Isabelle/jEdit (this is the proper name and spelling of that product).I can't say anything about Isabelle/VSCode right now, because I did
not have any time testing this experimental side-branch of Isabelle/PIDE.Makarius
Last updated: Mar 09 2025 at 12:28 UTC