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