[isabelle] jEdit Automatic Proof Indentation



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.
/*
 * Indent Isabelle apply-style proofs.
 *
 * 2013 David Greenaway.
 */

import isabelle.*;
import isabelle.jedit.*;

/* Get the number of pending subgoals in the given state. */
int num_subgoals(Command.State state)
{
    status_nodes = cmd_state.status();

    /* Find the "PROOF_STATE" node. */
    proof_state = null;
    for (node_list = cmd_state.status();
            node_list.nonEmpty(); node_list = node_list.tail()) {
        n = node_list.head();
        if (n.name().equals(Markup.PROOF_STATE())) {
            proof_state = n;
            break;
        }
    }
    if (proof_state == null)
      return -1;

    /* Find the "subgoals" node. */
    for (state_nodes_list = proof_state.properties();
            state_nodes_list.nonEmpty(); state_nodes_list = state_nodes_list.tail()) {
        n = state_nodes_list.head();
        if (n._1.equals(Markup.SUBGOALS())) {
            return Integer.parseInt(n._2);
        }
    }

    /* No node found. */
    return -1;
}

/* Pad the given string to have "n" spaces. */
String pad(String input, int n)
{
    if (input.equals(""))
        return "";
  char[] spaces = new char[n];
  Arrays.fill(spaces, ' ');
  return new String(spaces) + input;
}

/* Determine if the given command should be indented. */
Boolean shouldIndent(Command cmd)
{
    if (!cmd.is_command())
        return false;
    if (cmd.is_undefined())
        return false;
    if (cmd.is_unparsed())
        return false;
    if (cmd.is_unfinished())
        return false;
    return cmd.name().equals("apply");
}

/* Setup. */
model = PIDE.document_model(textArea.buffer).get();
model.full_perspective();
snapshot = model.snapshot();

/* Setup array of pre-calculated indents. */
selectedLines = textArea.getSelectedLines();
int[] padding = new int[selectedLines.length];
Arrays.fill(padding, -1);

/*
 * Iterate over selected lines, calculating indents.
 *
 * We calculate all indents prior to actually touching anything so that
 * Isabelle doesn't attempt to re-prove the lines we are trying to query at the
 * same time.
 */
for (i = 0; i < selectedLines.length; i++) {
    line = selectedLines[i];
    lineStart = textArea.getLineStartOffset(line);
    lineEnd = textArea.getLineEndOffset(line);

    /* Fetch the Isabelle state for this line. */
    cmd_opt = snapshot.node().command_at(lineStart - 1);
    if (cmd_opt.isEmpty())
        continue;

    /* Get the number of subgoals of this line. */
    cmd = cmd_opt.get()._1;
    cmd_state = snapshot.state().command_state(snapshot.version(), cmd);
    subgoals = num_subgoals(cmd_state);
    if (shouldIndent(cmd) && subgoals > 0) {
        padding[i] = subgoals + 1;
    }
}

/* Actually perform the updates. */
buffer.beginCompoundEdit();
try {
    for (i = selectedLines.length - 1; i >= 0; i--) {
        line = selectedLines[i];
        lineStart = textArea.getLineStartOffset(line);
        lineEnd = textArea.getLineEndOffset(line);

        /* Skip lines that shouldn't be indented. */
        if (padding[i] < 0)
            continue;

        /* Pad out this line. */
        text = pad(textArea.getLineText(line).trim(), padding[i]) + "\n";

        /* Insert new line. */
        textArea.setSelectedText(new Selection.Range(lineStart, lineEnd), text);
    }
} finally {
    buffer.endCompoundEdit();
}



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