From: Xingyuan Zhang <xingyuanzhang@126.com>
Dear Isabelle Users,
We I started the scala interpreter using:
isabelle scala
from the Cygwin-Termin.bat under Isabelle/VS Code, the Backspace key did not work. When I typed Backspace to remove the character just typed in, it shows something like:
?[K
And all the arrow keys did not work neither.
I will be very grateful if anybody can give some help.
Xingyuan
From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
Hi Xingyuan,
If I recall correctly, this is actually a more general problem with the Scala interpreter, independent of Isabelle, and reproducible under Linux and macOS as well. I think the work around is to prefix execution with rlwrap. I was never clear why the Scala devs did not fix this upstream, but maybe they have and my recollections are out of date.
Thanks,
Matt
From: Makarius <makarius@sketis.net>
Does it mean that you are using the VSCode terminal to run
Isabelle2020/Cygwin-Terminal.bat ? Does that contuinue in the VSCode window,
or open a different console window?
Note that "isabelle scala" merely invokes the regular "scala" tool with some
additions to the environment. The Scala guys are using jline-2.14.6 for the
command-line interaction. That always had problems with various Windows
terminals, as far as I can remember.
It does work reliably on Linux and macOS, though --- I often use it for
low-level Isabelle/Scala experiments.
For high-level Isabelle/Scala/PIDE experiments, I usually use the portable
Console/Scala plugin in Isabelle/jEdit: that can even interrupt Scala
execution properly. In contrast, console SIGINT does not work properly on
Windows at all.
Makarius
From: Xingyuan Zhang <xingyuanzhang@126.com>
At 2020-05-09 19:19:17, "Makarius" <makarius@sketis.net> wrote:
On 08/05/2020 06:41, Xingyuan Zhang wrote:
Does it mean that you are using the VSCode terminal to run
Isabelle2020/Cygwin-Terminal.bat ? Does that contuinue in the VSCode window,
or open a different console window?
Yes. I am using the VSCode terminal to run Isabelle2020/Cygwin-Terminal.bat. It does not open a different console window, and is working in the same terminal window, but the shell is changed from Windows's PS shell to a bash of Cygwin.
Note that "isabelle scala" merely invokes the regular "scala" tool with some
additions to the environment. The Scala guys are using jline-2.14.6 for the
command-line interaction. That always had problems with various Windows
terminals, as far as I can remember.It does work reliably on Linux and macOS, though --- I often use it for
low-level Isabelle/Scala experiments.
I want to do similar things, but preferably in Isabelle/VS Code, because I like it's lightweight.
Unfortunately, the Backspace and arrow keys does not work under Windows/Cygwin.
I hope the problem can be solved by some simple configuration change. But I can not find any hint on this issue.
Last updated: Nov 21 2024 at 12:39 UTC