Browse Source

Bug fix for updateAutoParse(): from prism-games.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10826 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
commit
3347d55d0a
  1. 5
      prism/src/userinterface/model/GUIMultiModelHandler.java

5
prism/src/userinterface/model/GUIMultiModelHandler.java

@ -929,6 +929,9 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
*/ */
public synchronized void updateAutoParse() public synchronized void updateAutoParse()
{ {
// Store existing status
boolean autoParseOld = autoParse;
// Is auto-parse switched on? // Is auto-parse switched on?
autoParse = theModel.getPrism().getSettings().getBoolean(PrismSettings.MODEL_AUTO_PARSE); autoParse = theModel.getPrism().getSettings().getBoolean(PrismSettings.MODEL_AUTO_PARSE);
@ -943,7 +946,7 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener
} }
// If the flag has just been switched ON, do a parse... // If the flag has just been switched ON, do a parse...
if (autoParse) {
if (!autoParseOld && autoParse) {
tree.makeNotUpToDate(); tree.makeNotUpToDate();
theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE)); theModel.notifyEventListeners(new GUIModelEvent(GUIModelEvent.MODIFIED_SINCE_SAVE));
if (!parsing) { if (!parsing) {

Loading…
Cancel
Save