1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7/*
8 * Jump to first Isabelle error in text area (if available).
9 *
10 * by Rafal Kolanski (2015)
11 *
12 * Install by dropping this file (`goto-error.bsh`) into the directory
13 * ` ~/.isabelle/jedit/macros/`. After restarting jEdit or rescanning
14 * macros in jEdit, the macro `goto-error` shoud appear in the `Macros`
15 * menu.
16 *
17 * You can additionally add a key binding the new macro by going to
18 * `Plugins -> Plugin Options -> Global Options -> jEdit/Shortcuts`
19 */
20
21import isabelle.*;
22import isabelle.jedit.*;
23
24// utils
25msg(s) { Macros.message(view, s); }
26
27// isabelle setup
28model = Document_Model.get(textArea.getBuffer());
29snapshot = model.get().snapshot();
30
31class FirstError {
32    public int first_error_pos = -1;
33
34    boolean handle(cmd, offset, markup) {
35
36        if (markup.name().equals("error_message")) {
37            first_error_pos = offset;
38            return false;
39        }
40        return true;
41    }
42    void after() {
43        if (first_error_pos >= 0) {
44            textArea.setCaretPosition(first_error_pos);
45        } else {
46            textArea.setCaretPosition(textArea.getBufferLength());
47        }
48    }
49}
50
51class MsgError {
52    boolean handle(cmd, offset, markup) {
53        if (markup.name().equals("error_message")) {
54            int line = textArea.getLineOfOffset(offset);
55            int col = offset - textArea.getLineStartOffset(line);
56            msg(markup.name() + "\n" + offset + "(l " + line + ", c " + col +
57                ") : " + cmd.source());
58        }
59        return true;
60    }
61    void after() {
62        return;
63    }
64}
65
66command_markup_scanner(int startLine, handler) {
67    boolean keep_going = true;
68
69    cmd_range = snapshot.node().command_iterator(startLine);
70
71    while (cmd_range.hasNext() && keep_going) {
72        cmdn = cmd_range.next(); // (command, offset)
73        cmd = cmdn._1;
74
75        // figure out line and column of where command begins
76        cmd_offset = cmdn._2;
77
78        // get all results generated by command
79        cmd_results = snapshot.state().command_results(snapshot.version(), cmd);
80
81        i = cmd_results.iterator();
82        while (i.hasNext() && keep_going) {
83            // results are keyed by an int of some kind (_1) which we don't need
84            m = i.next()._2.markup();
85
86            // identify error messages
87            keep_going = handler.handle(cmd, cmd_offset, m);
88        }
89    }
90    handler.after();
91}
92
93// command_markup_scanner(0, new MsgError()); // debugging
94
95command_markup_scanner(0, new FirstError());
96
97return;
98
99