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