Email Gateway (Aug 19 2022 at 10:33): Email Gateway (Aug 19 2022 at 10:33):From: David Greenaway <david.greenaway@nicta.com.au>
Hi all,
In my spare time I constructed the attached script to attempt to
automatically indent apply-style proofs. It is written in BeanShell,
which was probably a mistake, but what's done is done. To use the
script, it should be sufficient to just drop it in:
~/.isabelle/jedit/macros/
and restart jEdit.
You can then select a block of proof script you want indented, and then
in the jEdit menus select "Macros" -> "proof-indent".
The script has its fair share of problems: multi-line statements are not
handled well, and there seems to be some problems in handling the first
line of proof script.
I am posting that script as-is hoping that somebody else might find it
useful in its current state, and to also ask for a little bit of help:
In particular, does anyone know how I can determine that first and last
characters of each command in the proof script? I am currently using
"snapshot.node().command_at(x)", which gives me the proof state
approximately at character "x" of the file, but doesn't appear to
provide me with the exact start/end of each statement that I desire.
If anyone could point me to the correct way of pulling this information
out of Isabelle (or some documentation), I would very much appreciate
it.
Thanks so much,
David
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
proof-indent.bsh
Email Gateway (Aug 19 2022 at 10:35):From: Fabian Immler <immler@in.tum.de>
Hi David,
Am 22.03.2013 um 01:48 schrieb David Greenaway <david.greenaway@nicta.com.au>:
In particular, does anyone know how I can determine that first and last
characters of each command in the proof script? I am currently using
"snapshot.node().command_at(x)", which gives me the proof state
approximately at character "x" of the file, but doesn't appear to
provide me with the exact start/end of each statement that I desire.
The second component appears to return the starting offset, and range()/proper_range() provide you with the length of the command (with or without trailing comments/whitespace):
cmd_start = snapshot.node().command_at(x).get();
cmd = cmd_start._1;
start = cmd_start._2;
range = cmd.proper_range();
end = start + range.stop;
If anyone could point me to the correct way of pulling this information
out of Isabelle (or some documentation), I would very much appreciate
it.
I think you have to browse the respective .scala source files. It also helps to experiment in the BeanShell console of jEdit.
Fabian
Last updated: Apr 25 2024 at 01:08 UTC