Email Gateway (Aug 22 2022 at 09:04): Email Gateway (Aug 22 2022 at 09:04):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I just typed in Isabelle/jedit:
export_code foo in SML file "benchmarks/foo.sml"
The result is, that it created, in the current folder, the files:
be
benchmar
both containing the sml-code. Yep, I'm a slow typer but my machine is
also slow ;).
What probably happened here is that jedit re-processed the line
continuously, and generated all the files while I was still typing the
name.
How to avoid such strange things in jedit, except for trying to
high-speed typing, or adding a line containing only ".xxx" before the
export_code line while typing?
Best,
Peter
Email Gateway (Aug 22 2022 at 09:04):From: Makarius <makarius@sketis.net>
How about disabling "Continuous checking" in the Theory panel?
In some sense, the export_code command is still in a stateful TTY-oriented
mode. If TTY mode had been removed 2 years earlier, there would already
be a proper integration into the PIDE document model.
Side-remarks: the text editor is called "jEdit" with that spelling -- it
is a branding of that project.
The default Isabelle/PIDE implementation is called "Isabelle/jEdit".
Makarius
Email Gateway (Aug 22 2022 at 09:04):From: Lars Hupel <hupel@in.tum.de>
Just today I was thinking about that very issue, because I too find it annoying. So here are my two cents on how I envision a proper jEdit integration:
The command 'export_code' doesn't perform a side effect, but rather produces a special document result containing the generated code, which is then interpreted by jEdit. This could just be a button in the output panel. Clicking the button opens a regular jEdit text buffer with the generated code. In principle, the simplifier trace works in the same way.
Does that sound reasonable?
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:05):From: Makarius <makarius@sketis.net>
Yes, something like that has been in the pipeline for a long time. Maybe
I first mentioned it in winter 2012 when visiting TUM.
There are just the usual reasons why it is not done yet:
* Relatively low priority -- practical relevance is not exceedingly
high.
* Just too many historical problems and confusions in the department of
file input or output management with the document model, in contrast
to TTY mode behaviour.
Since TTY mode no longer exists after Isabelle2014, improvements are more
likely to happen eventually.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC