Browse Source

GUI text editor bug.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@670 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
commit
ceb6d89a6b
  1. 2
      prism/src/userinterface/model/GUITextModelEditor.java

2
prism/src/userinterface/model/GUITextModelEditor.java

@ -703,6 +703,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen
public int computeDocumentOffset(int line, int column) throws BadLocationException
{
if (line < 0 || column < 0) throw new BadLocationException("Negative line/col", -1);
Element lineElement = editor.getDocument().getDefaultRootElement().
getElement(line-1);

Loading…
Cancel
Save