From 6961bf6648c3000389c0e4378510e31f88f5ba80 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@nicta.com.au>
Date: Tue, 29 May 2018 16:20:56 +1000
Subject: [PATCH] misc: goto-error jEdit macro: handle errors, fix string
 compare

When updating to Isabelle 2017 the non-error case was neglected and gave
a stack dump rather than a sane message. This has now been addressed.

Apparently the Beanshell scripting environment in jEdit prior to 5.5.0
accepted '==' as string comparison. In 5.5.0 it is no longer accepted,
and requires .equals() as in normal Java.
---
 misc/jedit/macros/goto-error.bsh | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/misc/jedit/macros/goto-error.bsh b/misc/jedit/macros/goto-error.bsh
index b724b791c..0e7313ae5 100644
--- a/misc/jedit/macros/goto-error.bsh
+++ b/misc/jedit/macros/goto-error.bsh
@@ -37,7 +37,7 @@ class FirstError {
 
     boolean handle(cmd, offset, markup) {
 
-        if (markup.name() == "error_message") {
+        if (markup.name().equals("error_message")) {
             first_error_pos = offset;
             return false;
         }
@@ -47,14 +47,14 @@ class FirstError {
         if (first_error_pos >= 0) {
             textArea.setCaretPosition(first_error_pos);
         } else {
-            msg("No errors detected in theory " + model.node_name() + " (at present).");
+            msg("No errors detected in theory " + model.get().node_name() + " (at present).");
         }
     }
 }
 
 class MsgError {
     boolean handle(cmd, offset, markup) {
-        if (markup.name() == "error_message") {
+        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 +
@@ -67,7 +67,6 @@ class MsgError {
     }
 }
 
-// TODO: end when past a specific line
 command_markup_scanner(int startLine, handler) {
     boolean keep_going = true;