adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

misc: goto-error jEdit macro: update for 2023 

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2023-09-06 10:57:55 +10:00 committed by Gerwin Klein
parent eeae2af478
commit 286278d9e8
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
misc/jedit/macros/goto-error.bsh
View File

@ -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;