*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] jEdit Automatic Proof Indentation*From*: David Greenaway <david.greenaway at nicta.com.au>*Date*: Fri, 22 Mar 2013 11:48:09 +1100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121010 Thunderbird/16.0.1

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(); }

**Follow-Ups**:**Re: [isabelle] jEdit Automatic Proof Indentation***From:*Fabian Immler

- Previous by Date: Re: [isabelle] Isabelle/jEdit: can anybody else reproduce
- Next by Date: [isabelle] union-find based unification
- Previous by Thread: [isabelle] Fwd: SMT 2013 Call For Papers
- Next by Thread: Re: [isabelle] jEdit Automatic Proof Indentation
- Cl-isabelle-users March 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list