From 286278d9e859431e9bea5366834f64193f1a6992 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Wed, 6 Sep 2023 10:57:55 +1000 Subject: [PATCH] misc: goto-error jEdit macro: update for 2023 Signed-off-by: Rafal Kolanski --- misc/jedit/macros/goto-error.bsh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/misc/jedit/macros/goto-error.bsh b/misc/jedit/macros/goto-error.bsh index d727d5dfb..3fc260c0d 100644 --- a/misc/jedit/macros/goto-error.bsh +++ b/misc/jedit/macros/goto-error.bsh @@ -25,8 +25,8 @@ import isabelle.jedit.*; msg(s) { Macros.message(view, s); } // isabelle setup -model = Document_Model.get(textArea.getBuffer()); -snapshot = model.get().snapshot(); +model = Document_Model.get_model(textArea.getBuffer()); +snapshot = Document_Model.snapshot(model.get()); class FirstError { public int first_error_pos = -1;