1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7/* 8 * Indent Isabelle apply-style proofs. 9 * 2013 David Greenaway. 10 * 11 * Install by dropping this file (`proof-indent.bsh`) into the directory 12 * ` ~/.isabelle/jedit/macros/`. After restarting jEdit or rescanning 13 * macros in jEdit, the macro `proof-indent` shoud appear in the `Macros` 14 * menu. 15 * 16 * You can additionally add a key binding, for instance Command-Shift-I 17 * (for Indent), to the new macro `proof-indent` by going to 18 * `Plugins -> Plugin Options -> Global Options -> jEdit/Shortcuts` 19 */ 20 21import isabelle.*; 22import isabelle.jedit.*; 23 24/* Get the number of pending subgoals in the given state. */ 25int num_subgoals(Command.State state) 26{ 27 status_nodes = state.status(); 28 29 /* Find the "PROOF_STATE" node. */ 30 proof_state = null; 31 for (node_list = state.status(); 32 node_list.nonEmpty(); node_list = node_list.tail()) { 33 n = node_list.head(); 34 if (n.name().equals(Markup.PROOF_STATE())) { 35 proof_state = n; 36 break; 37 } 38 } 39 if (proof_state == null) 40 return -1; 41 42 /* Find the "subgoals" node. */ 43 for (state_nodes_list = proof_state.properties(); 44 state_nodes_list.nonEmpty(); state_nodes_list = state_nodes_list.tail()) { 45 n = state_nodes_list.head(); 46 if (n._1.equals(Markup.SUBGOALS())) { 47 return Integer.parseInt(n._2); 48 } 49 } 50 51 /* No node found. */ 52 return -1; 53} 54 55/* Pad the given string to have "n" spaces. */ 56String pad(String input, int n) 57{ 58 if (input.equals("")) 59 return ""; 60 char[] spaces = new char[n]; 61 Arrays.fill(spaces, ' '); 62 return new String(spaces) + input; 63} 64 65/* Determine if the given command should be indented. */ 66Boolean shouldIndent(Command cmd) 67{ 68 /* FIXME */ 69 return true; 70} 71 72/* Setup. */ 73model = PIDE.document_model(textArea.buffer).get(); 74snapshot = model.snapshot(); 75 76/* Setup array of pre-calculated indents. */ 77selectedLines = textArea.getSelectedLines(); 78int[] padding = new int[selectedLines.length]; 79Arrays.fill(padding, -1); 80 81/* 82 * Iterate over selected lines, calculating indents. 83 * 84 * We calculate all indents prior to actually touching anything so that 85 * Isabelle doesn't attempt to re-prove the lines we are trying to query at the 86 * same time. 87 */ 88for (i = 0; i < selectedLines.length; i++) { 89 line = selectedLines[i]; 90 lineStart = textArea.getLineStartOffset(line); 91 lineEnd = textArea.getLineEndOffset(line); 92 93 /* Fetch the Isabelle state for this line. */ 94 cmd_range = snapshot.node().command_iterator(lineStart - 1); 95 if (!cmd_range.hasNext()) 96 continue; 97 cmd = cmd_range.next()._1; 98 99 /* Get the number of subgoals of this line. */ 100 cmd_state = snapshot.state().command_states(snapshot.version(), cmd).productElement(0); 101 subgoals = num_subgoals(cmd_state); 102 if (shouldIndent(cmd) && subgoals > 0) { 103 padding[i] = subgoals + 1; 104 } 105} 106 107/* Actually perform the updates. */ 108buffer.beginCompoundEdit(); 109try { 110 for (i = selectedLines.length - 1; i >= 0; i--) { 111 line = selectedLines[i]; 112 lineStart = textArea.getLineStartOffset(line); 113 lineEnd = textArea.getLineEndOffset(line); 114 115 /* Skip lines that shouldn't be indented. */ 116 if (padding[i] < 0) 117 continue; 118 119 /* Pad out this line. */ 120 text = pad(textArea.getLineText(line).trim(), padding[i]) + "\n"; 121 122 /* Insert new line. */ 123 textArea.setSelectedText(new Selection.Range(lineStart, lineEnd), text); 124 } 125} finally { 126 buffer.endCompoundEdit(); 127} 128 129