Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question about "isabelle scala"


view this post on Zulip Email Gateway (Aug 23 2022 at 09:05):

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

view this post on Zulip Email Gateway (Aug 23 2022 at 09:05):

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

view this post on Zulip Email Gateway (Aug 23 2022 at 09:06):

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

view this post on Zulip Email Gateway (Aug 23 2022 at 09:07):

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: Apr 19 2024 at 04:17 UTC