[isabelle] Updated goto-error script for Isabelle (jumps to first error in theory file)



Hello,

In our group, we use a jEdit macro that jumps to the first error of a
theory file. In large theory files, it's hard to click on the right spot
on the theory overview, and it's much easier to twitch some key
combination the moment you see red in the progress bar.

Larry is a big fan, and always pokes me when some update causes
breakage. He suggested I disseminate it more widely.

The attached version is updated to work on Isabelle 2017 and the dev
version as of about a week ago. Place in ~/.isabelle/jedit/macros then
do Macros->Rescan Macros, or restart jEdit.

We typically bind it to a key combination and have a hard time living
without it.

Let me know if you have any questions.

Sincerely,

Rafal Kolanski
/*
 * 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;



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.