/*
 * 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)
 */

/*
 * Jump to first Isabelle error in text area (if available).
 *
 * by Rafal Kolanski (2015)
 *
 * Install by dropping this file (`goto-error.bsh`) into the directory
 * ` ~/.isabelle/jedit/macros/`. After restarting jEdit or rescanning
 * macros in jEdit, the macro `goto-error` shoud appear in the `Macros`
 * menu.
 *
 * You can additionally add a key binding the new macro by going to
 * `Plugins -> Plugin Options -> Global Options -> jEdit/Shortcuts`
 */

import isabelle.*;
import isabelle.jedit.*;

// utils
msg(s) { Macros.message(view, s); }

// isabelle setup
model = Document_Model.get(textArea.getBuffer());
snapshot = model.get().snapshot();

class FirstError {
    public int first_error_pos = -1;

    boolean handle(cmd, offset, markup) {

        if (markup.name().equals("error_message")) {
            first_error_pos = offset;
            return false;
        }
        return true;
    }
    void after() {
        if (first_error_pos >= 0) {
            textArea.setCaretPosition(first_error_pos);
        } else {
            msg("No errors detected in theory " + model.get().node_name() + " (at present).");
        }
    }
}

class MsgError {
    boolean handle(cmd, offset, markup) {
        if (markup.name().equals("error_message")) {
            int line = textArea.getLineOfOffset(offset);
            int col = offset - textArea.getLineStartOffset(line);
            msg(markup.name() + "\n" + offset + "(l " + line + ", c " + col +
                ") : " + cmd.source());
        }
        return true;
    }
    void after() {
        return;
    }
}

// TODO: end when past a specific line
command_markup_scanner(int startLine, handler) {
    boolean keep_going = true;

    cmd_range = snapshot.node().command_iterator(startLine);

    while (cmd_range.hasNext() && keep_going) {
        cmdn = cmd_range.next(); // (command, offset)
        cmd = cmdn._1;

        // figure out line and column of where command begins
        cmd_offset = cmdn._2;

        // get all results generated by command
        cmd_results = snapshot.state().command_results(snapshot.version(), cmd);

        i = cmd_results.iterator();
        while (i.hasNext() && keep_going) {
            // results are keyed by an int of some kind (_1) which we don't need
            m = i.next()._2.markup();

            // identify error messages
            keep_going = handler.handle(cmd, cmd_offset, m);
        }
    }
    handler.after();
}

// command_markup_scanner(0, new MsgError()); // debugging

command_markup_scanner(0, new FirstError());

return;