search

andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

IllegalArgumentException when editing Theory file #11

Closed andriusvelykis closed 11 years ago

andriusvelykis commented 11 years ago

Appears sporadically

java.lang.IllegalArgumentException: Argument not valid
    at org.eclipse.swt.SWT.error(SWT.java:4342)
    at org.eclipse.swt.SWT.error(SWT.java:4276)
    at org.eclipse.swt.SWT.error(SWT.java:4247)
    at org.eclipse.swt.custom.StyledText.setStyleRanges(StyledText.java:9709)
    at org.eclipse.swt.custom.StyledText.replaceStyleRanges(StyledText.java:7726)
    at org.eclipse.jface.text.TextViewer.addPresentation(TextViewer.java:4845)
    at org.eclipse.jface.text.TextViewer.changeTextPresentation(TextViewer.java:4924)
    at org.eclipse.jface.text.presentation.PresentationReconciler.applyTextRegionCollection(PresentationReconciler.java:582)
    at org.eclipse.jface.text.presentation.PresentationReconciler.processDamage(PresentationReconciler.java:571)
    at org.eclipse.jface.text.presentation.PresentationReconciler.access$3(PresentationReconciler.java:567)
    at org.eclipse.jface.text.presentation.PresentationReconciler$InternalListener.textChanged(PresentationReconciler.java:227)
    at org.eclipse.jface.text.TextViewer.updateTextListeners(TextViewer.java:2830)
    at org.eclipse.jface.text.TextViewer.invalidateTextPresentation(TextViewer.java:3478)
    at isabelle.eclipse.ui.editors.TheoryEditor$State$$anonfun$refreshView$1.apply$mcV$sp(TheoryEditor.scala:305)
    at isabelle.eclipse.ui.util.JobUtil$$anon$1.runInUIThread(JobUtil.scala:19)
    at org.eclipse.ui.progress.UIJob$1.run(UIJob.java:95)
    at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
    at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)
    at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:3944)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3621)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1022)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:916)
    at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:86)
    at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:587)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:542)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
    at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:124)
    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:353)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:180)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:629)
    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:584)
    at org.eclipse.equinox.launcher.Main.run(Main.java:1438)
    at org.eclipse.equinox.launcher.Main.main(Main.java:1414)
andriusvelykis commented 11 years ago

Have not encountered the issue since upgrade to Isabelle 2013 and associated rework of Editor/Prover Output.

Assuming this got fixed by that upgrade, since the problem was reported for earlier version and was intermittent.

andriusvelykis commented 11 years ago

As reported in #80, the problem is still around. Reopening.

andriusvelykis commented 11 years ago

The issue seems to be caused by bad output in ITokenScanners for Isabelle markups. If the tokens are overlapping, their style ranges also overlap resulting in the reported exception.

Added additional normalisation for ITokenScanners in 29760cf3b22fcef3ef47dfac0d747f79bcd58a44, which ensures no tokens are overlapping.

Since I cannot reproduce the issue consistently, closing the report, assuming this fixed it. If the problem still persists, reopen.