Re: [isabelle] jEdit Automatic Proof Indentation



Hi David,


Am 22.03.2013 um 01:48 schrieb David Greenaway <david.greenaway at 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.