Opened 16 years ago

Last modified 11 years ago

#251 new defect

Exception in editor startup

Reported by: David Aspinall Owned by: David Aspinall
Priority: critical Milestone:
Component: 1:pg-eclipse Keywords:
Cc:

Description

This is caused because a document can be initialised without setting all the fields we use, in particular, the prover field. 

java.lang.NullPointerException
	at ed.inf.proofgeneral.editor.ProofScriptEditor.init(ProofScriptEditor.java:133)
	at org.eclipse.ui.internal.EditorManager.createSite(EditorManager.java:799)

This either happens because the editor is initialised before init() is finished in the document provider, or because an error is preventing this method completing properly.

The best improvement might be to refactor to have a document class per-prover so that the nullary factory constructor can do full initialisation.

Change History (1)

comment:1 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.6

Milestone PG-Eclipse-1.0.6 deleted

Note: See TracTickets for help on using tickets.