-
Notifications
You must be signed in to change notification settings - Fork 105
/
proof-indent.bsh
132 lines (114 loc) · 3.68 KB
/
proof-indent.bsh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
/*
* Indent Isabelle apply-style proofs.
* 2013 David Greenaway.
*
* Install by dropping this file (`proof-indent.bsh`) into the directory
* ` ~/.isabelle/jedit/macros/`. After restarting jEdit or rescanning
* macros in jEdit, the macro `proof-indent` shoud appear in the `Macros`
* menu.
*
* You can additionally add a key binding, for instance Command-Shift-I
* (for Indent), to the new macro `proof-indent` by going to
* `Plugins -> Plugin Options -> Global Options -> jEdit/Shortcuts`
*/
import isabelle.*;
import isabelle.jedit.*;
/* Get the number of pending subgoals in the given state. */
int num_subgoals(Command.State state)
{
status_nodes = state.status();
/* Find the "PROOF_STATE" node. */
proof_state = null;
for (node_list = 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)
{
/* FIXME */
return true;
}
/* Setup. */
model = PIDE.document_model(textArea.buffer).get();
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_range = snapshot.node().command_iterator(lineStart - 1);
if (!cmd_range.hasNext())
continue;
cmd = cmd_range.next()._1;
/* Get the number of subgoals of this line. */
cmd_state = snapshot.state().command_states(snapshot.version(), cmd).productElement(0);
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();
}