Skip to content
Permalink
Browse files

Some refactoring concerning model state change listeners; also haltin…

…g the "m_" prefix used in some of the refactored classes.
  • Loading branch information...
quaeler committed Oct 6, 2019
1 parent 7569e6d commit 0d32f2873e767a7b08afe398435a64db5bc342e9
@@ -67,8 +67,8 @@
import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationConstants;
import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationDefaults;
import org.lamport.tla.toolbox.tool.tlc.launch.TLCModelLaunchDelegate;
import org.lamport.tla.toolbox.tool.tlc.model.AbstractModelStateChangeListener;
import org.lamport.tla.toolbox.tool.tlc.model.Model;
import org.lamport.tla.toolbox.tool.tlc.model.Model.StateChangeListener.ChangeEvent.State;
import org.lamport.tla.toolbox.tool.tlc.model.TLCModelFactory;
import org.lamport.tla.toolbox.tool.tlc.output.data.TLCModelLaunchDataProvider;
import org.lamport.tla.toolbox.tool.tlc.output.source.TLCOutputSourceRegistry;
@@ -120,74 +120,7 @@
*/
// helper to resolve semantic matches of words
private SemanticHelper helper;
private final Model.StateChangeListener modelStateListener = new Model.StateChangeListener() {
private State m_lastState = State.NOT_RUNNING;

@Override
public boolean handleChange(final ChangeEvent event) {
if (event.getState().in(State.NOT_RUNNING, State.RUNNING)) {
final State lastStateCopy = m_lastState;
UIHelper.runUIAsync(() -> {
for (int i = 0; i < getPageCount(); i++) {
final Object object = pages.get(i);
if (object instanceof BasicFormPage) {
final BasicFormPage bfp = (BasicFormPage) object;
bfp.refresh();
}
}
if (event.getState().in(State.RUNNING)) {
// Switch to Result Page (put on top) of model editor stack. A user wants to see
// the status of a model run she has just started.
final IPreferenceStore ips = TLCUIActivator.getDefault().getPreferenceStore();
final boolean eceInItsOwnTab = ips
.getBoolean(IModelEditorPreferenceConstants.I_MODEL_EDITOR_SHOW_ECE_AS_TAB);

if (!eceInItsOwnTab || !modelIsConfiguredWithNoBehaviorSpec()) {
showResultPage();
}
} else if (event.getState().in(State.NOT_RUNNING)) {
// Model checking finished, lets open state graph if any.
if (event.getModel().hasStateGraphDump()) {
try {
addOrUpdateStateGraphEditor(event.getModel().getStateGraphDump());
} catch (CoreException e) {
TLCUIActivator.getDefault().logError("Error initializing editor", e);
}
}

if (lastStateCopy.in(State.RUNNING, State.REMOTE_RUNNING)) {
final IPreferenceStore ips = TLCUIActivator.getDefault().getPreferenceStore();
final boolean eceInItsOwnTab = ips
.getBoolean(IModelEditorPreferenceConstants.I_MODEL_EDITOR_SHOW_ECE_AS_TAB);

if (eceInItsOwnTab && modelIsConfiguredWithNoBehaviorSpec()) {
setActivePage(EvaluateConstantExpressionPage.ID);
}
}

// MAK 01/2018: Re-validate the page because running the model removes or sets
// problem markers (Model#setMarkers) which are presented to the user by
// ModelEditor#handleProblemMarkers. If we don't re-validate once a model is
// done running, the user visible presentation resulting from an earlier run of
// handleProblemMarkers gets stale.
// This behavior can be triggered by creating a spec (note commented EXTENDS):
// \* EXTENDS Integers
// VARIABLE s
// Spec == s = 0 /\ [][s'=s]_s
// and a model that defines the invariant (s >= 0). Upon the first launch of
// the model, the ModelEditor correctly marks the invariant due to the operator
// >= being not defined. Uncommenting EXTENDS, saving the spec and rerunning
// the model would incorrectly not remove the marker on the invariant.
UIHelper.runUISync(validateRunable);
}
});
}

m_lastState = event.getState();

return false;
}
};
private ModelStateListener modelStateListener = new ModelStateListener();

/**
* This runnable is responsible for the validation of the pages.
@@ -209,7 +142,7 @@ public boolean handleChange(final ChangeEvent event) {
*/
private CTabFolder2Listener listener = new CloseModuleTabListener();

private final Map<Integer, Closeable> m_indexCloseableMap;
private final Map<Integer, Closeable> indexCloseableMap;

// array of pages to add
private BasicFormPage[] pagesToAdd;
@@ -266,11 +199,16 @@ public IResource getModel() {
navigationHistory.markLocation((IEditorPart) event.getSelectedPage());
};

private final IPropertyChangeListener m_preferenceChangeListener = (event) -> {
private final IPropertyChangeListener preferenceChangeListener = (event) -> {
if (IModelEditorPreferenceConstants.I_MODEL_EDITOR_SHOW_ECE_AS_TAB.equals(event.getProperty())) {
final boolean eceAsTab = ((Boolean) event.getNewValue()).booleanValue();
final Pair<Integer, FormPage> pair = getLastFormPage();
final String id = pair.getRight().getId();

// No results page open, so don't show the ECE page, slash, affect the results page to show the ECE section
if (!ResultPage.ID.equals(id) && !EvaluateConstantExpressionPage.ID.equals(id)) {
return;
}

if (eceAsTab) {
if (!EvaluateConstantExpressionPage.ID.equals(id)) {
@@ -309,7 +247,7 @@ public IResource getModel() {
*/
public ModelEditor() {
helper = new SemanticHelper();
m_indexCloseableMap = new HashMap<>();
indexCloseableMap = new HashMap<>();
}

/**
@@ -368,12 +306,12 @@ public void init(IEditorSite site, IEditorInput input) throws PartInitException
pages.add(new ResultPage(this));
if (eceInItsOwnTab) {
pages.add(new EvaluateConstantExpressionPage(this));
}

pagesToAdd = pages.toArray(new BasicFormPage[pages.size()]);
}

pagesToAdd = pages.toArray(new BasicFormPage[pages.size()]);
}

ips.addPropertyChangeListener(m_preferenceChangeListener);
ips.addPropertyChangeListener(preferenceChangeListener);


// setContentDescription(path.toString());
@@ -436,7 +374,7 @@ public String getIdForEditorAtIndex(final int index) {
public void dispose() {
removePageChangedListener(pageChangedListener);

TLCUIActivator.getDefault().getPreferenceStore().removePropertyChangeListener(m_preferenceChangeListener);
TLCUIActivator.getDefault().getPreferenceStore().removePropertyChangeListener(preferenceChangeListener);

// TLCUIActivator.getDefault().logDebug("entering ModelEditor#dispose()");
// remove the listeners
@@ -646,7 +584,7 @@ protected void addPages()
if (pagesToAdd[i] instanceof Closeable) {
item.setShowClose(true);

m_indexCloseableMap.put(new Integer(i), (Closeable)pagesToAdd[i]);
indexCloseableMap.put(new Integer(i), (Closeable)pagesToAdd[i]);
}
}

@@ -1269,9 +1207,9 @@ public void handleProblemMarkers(boolean switchToErrorPage)
}

public void setActivePage(int index) {
if(pages != null) {
super.setActivePage(index);
}
if ((pages != null) && (getCurrentPage() != index)) {
super.setActivePage(index);
}
}

/**
@@ -1329,7 +1267,7 @@ public ITextEditor getSavedModuleEditor(String moduleName)
}
return null;
}

/**
* Show the result page of the editor
*/
@@ -1453,7 +1391,7 @@ public void updateOpenTabsState(final int newValue) {
}

/**
* Invoke this to save the model.
* Invoke this to save the model via a workspace job.
*/
public void saveModel() {
final Job job = new WorkspaceJob("Saving updated model...") {
@@ -1486,7 +1424,7 @@ public void addOrShowAdvancedTLCOptionsPage() {
if (setActivePage(AdvancedTLCOptionsPage.ID) == null) {
try {
int pageIndex = 1;
final String id = getIdForEditorAtIndex(1);
final String id = getIdForEditorAtIndex(pageIndex);

if (AdvancedModelPage.ID.equals(id)) {
pageIndex++;
@@ -1503,7 +1441,7 @@ public void addOrShowAdvancedTLCOptionsPage() {
}
}
}

/**
* Overrides the method in {@link FormEditor}. Calls this method in the superclass
* and then makes some changes if the input is a tla file.
@@ -1551,14 +1489,14 @@ public void addPage(int index, IEditorPart editor, IEditorInput input) throws Pa

final int tabCount = tabFolder.getItemCount();
for (int i = tabCount - 2; i >= index; i--) {
final Closeable c = m_indexCloseableMap.remove(new Integer(i));
final Closeable c = indexCloseableMap.remove(new Integer(i));

if (c != null) {
m_indexCloseableMap.put(new Integer(i + 1), c);
indexCloseableMap.put(new Integer(i + 1), c);
}
}

m_indexCloseableMap.put(new Integer(index), (Closeable)editor);
indexCloseableMap.put(new Integer(index), (Closeable)editor);
}
}

@@ -1594,14 +1532,14 @@ public void close(CTabFolderEvent event) {
// man-years wasted writing and dealing with you..
// event.item is already disposed by the time we get notified so we can't use its data holder which is
// what is being used to hold the editor part by our super-superclass... kwality
final Closeable c = m_indexCloseableMap.remove(new Integer(index));
final Closeable c = indexCloseableMap.remove(new Integer(index));
if (c != null) {
final int tabCount = tabFolder.getItemCount();
for (int i = index; i <= tabCount; i++) {
final Closeable remaining = m_indexCloseableMap.remove(new Integer(i));
final Closeable remaining = indexCloseableMap.remove(new Integer(i));

if (remaining != null) {
m_indexCloseableMap.put(new Integer(i - 1), remaining);
indexCloseableMap.put(new Integer(i - 1), remaining);
}
}

@@ -1706,4 +1644,74 @@ public void run() {
}
}
}


private class ModelStateListener extends AbstractModelStateChangeListener {
private State lastState = State.NOT_RUNNING;

@Override
public boolean handleChange(final ChangeEvent event) {
if (event.getState().in(State.NOT_RUNNING, State.RUNNING)) {
final State lastStateCopy = lastState;
UIHelper.runUIAsync(() -> {
for (int i = 0; i < getPageCount(); i++) {
final Object object = pages.get(i);
if (object instanceof BasicFormPage) {
final BasicFormPage bfp = (BasicFormPage) object;
bfp.refresh();
}
}
if (event.getState().in(State.RUNNING)) {
// Switch to Result Page (put on top) of model editor stack. A user wants to see
// the status of a model run she has just started.
final IPreferenceStore ips = TLCUIActivator.getDefault().getPreferenceStore();
final boolean eceInItsOwnTab = ips
.getBoolean(IModelEditorPreferenceConstants.I_MODEL_EDITOR_SHOW_ECE_AS_TAB);

if (!eceInItsOwnTab || !modelIsConfiguredWithNoBehaviorSpec()) {
showResultPage();
}
} else if (event.getState().in(State.NOT_RUNNING)) {
// Model checking finished, lets open state graph if any.
if (event.getModel().hasStateGraphDump()) {
try {
addOrUpdateStateGraphEditor(event.getModel().getStateGraphDump());
} catch (CoreException e) {
TLCUIActivator.getDefault().logError("Error initializing editor", e);
}
}

if (lastStateCopy.in(State.RUNNING, State.REMOTE_RUNNING)) {
final IPreferenceStore ips = TLCUIActivator.getDefault().getPreferenceStore();
final boolean eceInItsOwnTab = ips
.getBoolean(IModelEditorPreferenceConstants.I_MODEL_EDITOR_SHOW_ECE_AS_TAB);

if (eceInItsOwnTab && modelIsConfiguredWithNoBehaviorSpec()) {
setActivePage(EvaluateConstantExpressionPage.ID);
}
}

// MAK 01/2018: Re-validate the page because running the model removes or sets
// problem markers (Model#setMarkers) which are presented to the user by
// ModelEditor#handleProblemMarkers. If we don't re-validate once a model is
// done running, the user visible presentation resulting from an earlier run of
// handleProblemMarkers gets stale.
// This behavior can be triggered by creating a spec (note commented EXTENDS):
// \* EXTENDS Integers
// VARIABLE s
// Spec == s = 0 /\ [][s'=s]_s
// and a model that defines the invariant (s >= 0). Upon the first launch of
// the model, the ModelEditor correctly marks the invariant due to the operator
// >= being not defined. Uncommenting EXTENDS, saving the spec and rerunning
// the model would incorrectly not remove the marker on the invariant.
UIHelper.runUISync(validateRunable);
}
});
}

lastState = event.getState();

return false;
}
}
}
@@ -1281,9 +1281,11 @@ public void updateWorkersAndMemory(final int workerCount, final int memoryPercen

public void setWorkerAndMemoryEnable(final boolean enableWorker, final boolean enableMaxHeap) {
workers.getDisplay().asyncExec(() -> {
saveDefaultConfigurationButton.setEnabled(enableWorker);
workers.setEnabled(enableWorker);
maxHeapSize.setEnabled(enableMaxHeap);
if (!saveDefaultConfigurationButton.isDisposed()) {
saveDefaultConfigurationButton.setEnabled(enableWorker);
workers.setEnabled(enableWorker);
maxHeapSize.setEnabled(enableMaxHeap);
}
});
}

0 comments on commit 0d32f28

Please sign in to comment.
You can’t perform that action at this time.