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

Update proof perspective (an Internal Error Occurred) #79

Closed leouk closed 11 years ago

leouk commented 11 years ago

When trying to load a theory (outside the project) to see some older results it loaded the file and all was well. I then closed the file and went back to my development. In there I got errors when trying to proofs.

I tried to "unload" the theory outside the project (clicked the STOP button on theories view) and nothing happened. I just closed the file.

Then when back at my theory it wouldn't go forward on verifying the proof script. The PP proofs also got repeated (instead of having many attempts).

Inspecting the error log I got NPE:

java.lang.NullPointerException
    at org.eclipse.jface.text.JFaceTextUtil.getPartialTopIndex(JFaceTextUtil.java:150)
    at org.eclipse.jface.text.JFaceTextUtil.getVisibleModelLines(JFaceTextUtil.java:176)
    at isabelle.eclipse.ui.editors.DocumentPerspectiveTracker$class.isabelle$eclipse$ui$editors$DocumentPerspectiveTracker$$visibleRange(DocumentPerspectiveTracker.scala:82)
    at isabelle.eclipse.ui.editors.DocumentPerspectiveTracker$$anonfun$updateActivePerspective$1.apply$mcV$sp(DocumentPerspectiveTracker.scala:74)
    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:3946)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3623)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1053)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:942)
    at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:86)
    at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:588)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:543)
    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:57)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:601)
    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)