|
|
@ -26,23 +26,55 @@ |
|
|
//============================================================================== |
|
|
//============================================================================== |
|
|
|
|
|
|
|
|
package userinterface; |
|
|
package userinterface; |
|
|
|
|
|
|
|
|
//Java Packages |
|
|
//Java Packages |
|
|
import java.util.*; |
|
|
|
|
|
|
|
|
import java.awt.BorderLayout; |
|
|
|
|
|
import java.awt.Component; |
|
|
|
|
|
import java.awt.Dimension; |
|
|
|
|
|
import java.awt.EventQueue; |
|
|
|
|
|
import java.awt.FlowLayout; |
|
|
|
|
|
import java.awt.Font; |
|
|
|
|
|
import java.awt.Toolkit; |
|
|
|
|
|
import java.awt.event.ActionEvent; |
|
|
|
|
|
import java.awt.event.InputEvent; |
|
|
|
|
|
import java.awt.event.KeyEvent; |
|
|
|
|
|
import java.io.File; |
|
|
|
|
|
import java.io.IOException; |
|
|
|
|
|
import java.net.URL; |
|
|
|
|
|
import java.util.ArrayList; |
|
|
import java.util.List; |
|
|
import java.util.List; |
|
|
import java.io.*; |
|
|
|
|
|
import java.net.*; |
|
|
|
|
|
import java.awt.*; |
|
|
|
|
|
import java.awt.event.*; |
|
|
|
|
|
|
|
|
|
|
|
import javax.swing.*; |
|
|
|
|
|
|
|
|
import javax.swing.AbstractAction; |
|
|
|
|
|
import javax.swing.Action; |
|
|
|
|
|
import javax.swing.ImageIcon; |
|
|
|
|
|
import javax.swing.JFileChooser; |
|
|
|
|
|
import javax.swing.JFrame; |
|
|
|
|
|
import javax.swing.JMenu; |
|
|
|
|
|
import javax.swing.JMenuBar; |
|
|
|
|
|
import javax.swing.JOptionPane; |
|
|
|
|
|
import javax.swing.JPanel; |
|
|
|
|
|
import javax.swing.JProgressBar; |
|
|
|
|
|
import javax.swing.JTabbedPane; |
|
|
|
|
|
import javax.swing.KeyStroke; |
|
|
|
|
|
import javax.swing.SwingUtilities; |
|
|
|
|
|
import javax.swing.UIManager; |
|
|
import javax.swing.event.ChangeEvent; |
|
|
import javax.swing.event.ChangeEvent; |
|
|
import javax.swing.event.ChangeListener; |
|
|
import javax.swing.event.ChangeListener; |
|
|
import javax.swing.plaf.*; |
|
|
|
|
|
import javax.swing.plaf.metal.*; |
|
|
|
|
|
|
|
|
import javax.swing.plaf.FontUIResource; |
|
|
|
|
|
import javax.swing.plaf.metal.MetalLookAndFeel; |
|
|
|
|
|
import javax.swing.plaf.metal.MetalTheme; |
|
|
|
|
|
|
|
|
|
|
|
import prism.Prism; |
|
|
//Prism Packages |
|
|
//Prism Packages |
|
|
import prism.*; |
|
|
|
|
|
import userinterface.util.*; |
|
|
|
|
|
|
|
|
import prism.PrismException; |
|
|
|
|
|
import prism.PrismFileLog; |
|
|
|
|
|
import prism.PrismLog; |
|
|
|
|
|
import userinterface.util.GUIComputationEvent; |
|
|
|
|
|
import userinterface.util.GUIEvent; |
|
|
|
|
|
import userinterface.util.GUIEventHandler; |
|
|
|
|
|
import userinterface.util.GUIException; |
|
|
|
|
|
import userinterface.util.GUIExitEvent; |
|
|
|
|
|
import userinterface.util.PresentationMetalTheme; |
|
|
|
|
|
|
|
|
/** PRISM Graphical User Interface |
|
|
/** PRISM Graphical User Interface |
|
|
* This class is the top level class for the PRISM GUI. It acts as a container |
|
|
* This class is the top level class for the PRISM GUI. It acts as a container |
|
|
@ -80,8 +112,7 @@ public class GUIPrism extends JFrame |
|
|
*/ |
|
|
*/ |
|
|
public static void main(String[] args) |
|
|
public static void main(String[] args) |
|
|
{ |
|
|
{ |
|
|
try |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
try { |
|
|
//Show the splash screen |
|
|
//Show the splash screen |
|
|
splash = new GUIPrismSplash("images/splash.png"); |
|
|
splash = new GUIPrismSplash("images/splash.png"); |
|
|
splash.display(); |
|
|
splash.display(); |
|
|
@ -89,19 +120,13 @@ public class GUIPrism extends JFrame |
|
|
gui.setVisible(true); |
|
|
gui.setVisible(true); |
|
|
EventQueue.invokeLater(new GUIPrism.SplashScreenCloser()); |
|
|
EventQueue.invokeLater(new GUIPrism.SplashScreenCloser()); |
|
|
gui.passCLArgs(args); |
|
|
gui.passCLArgs(args); |
|
|
} |
|
|
|
|
|
catch(GUIException e) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} catch (GUIException e) { |
|
|
System.err.println("Error: Could not load the PRISM GUI: " + e.getMessage()); |
|
|
System.err.println("Error: Could not load the PRISM GUI: " + e.getMessage()); |
|
|
System.exit(1); |
|
|
System.exit(1); |
|
|
} |
|
|
|
|
|
catch(PrismException e) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} catch (PrismException e) { |
|
|
System.err.println("Error: " + e.getMessage()); |
|
|
System.err.println("Error: " + e.getMessage()); |
|
|
System.exit(1); |
|
|
System.exit(1); |
|
|
} |
|
|
|
|
|
catch(jdd.JDD.CuddOutOfMemoryException e) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} catch (jdd.JDD.CuddOutOfMemoryException e) { |
|
|
System.err.println("Error: " + e.getMessage()); |
|
|
System.err.println("Error: " + e.getMessage()); |
|
|
System.exit(1); |
|
|
System.exit(1); |
|
|
} |
|
|
} |
|
|
@ -191,15 +216,12 @@ public class GUIPrism extends JFrame |
|
|
*/ |
|
|
*/ |
|
|
private void setupResources() throws GUIException |
|
|
private void setupResources() throws GUIException |
|
|
{ |
|
|
{ |
|
|
try |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
try { |
|
|
MetalTheme theme = new PresentationMetalTheme(0); |
|
|
MetalTheme theme = new PresentationMetalTheme(0); |
|
|
MetalLookAndFeel.setCurrentTheme(theme); |
|
|
MetalLookAndFeel.setCurrentTheme(theme); |
|
|
UIManager.setLookAndFeel(UIManager.getCrossPlatformLookAndFeelClassName()); |
|
|
UIManager.setLookAndFeel(UIManager.getCrossPlatformLookAndFeelClassName()); |
|
|
//UIManager.setLookAndFeel(UIManager.getSystemLookAndFeelClassName()); |
|
|
//UIManager.setLookAndFeel(UIManager.getSystemLookAndFeelClassName()); |
|
|
} |
|
|
|
|
|
catch(Exception e) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} catch (Exception e) { |
|
|
throw new GUIException("Failed to Initialise:\nLook and Feel Invalid"); |
|
|
throw new GUIException("Failed to Initialise:\nLook and Feel Invalid"); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
@ -209,7 +231,8 @@ public class GUIPrism extends JFrame |
|
|
// If current directory is the bin directory, go up one level (mainly for Windows version) |
|
|
// If current directory is the bin directory, go up one level (mainly for Windows version) |
|
|
try { |
|
|
try { |
|
|
currentDir = currentDir.getCanonicalFile(); |
|
|
currentDir = currentDir.getCanonicalFile(); |
|
|
if (currentDir.getName().equals("bin")) currentDir = currentDir.getParentFile(); |
|
|
|
|
|
|
|
|
if (currentDir.getName().equals("bin")) |
|
|
|
|
|
currentDir = currentDir.getParentFile(); |
|
|
} catch (IOException e) { |
|
|
} catch (IOException e) { |
|
|
currentDir = new File("."); |
|
|
currentDir = new File("."); |
|
|
} |
|
|
} |
|
|
@ -251,35 +274,31 @@ public class GUIPrism extends JFrame |
|
|
//options.addPanel(new GUIPrismOptionsPanel(prism)); |
|
|
//options.addPanel(new GUIPrismOptionsPanel(prism)); |
|
|
JPanel thePanel = new JPanel(); // panel to store tabs |
|
|
JPanel thePanel = new JPanel(); // panel to store tabs |
|
|
theTabs = new JTabbedPane(); |
|
|
theTabs = new JTabbedPane(); |
|
|
theTabs.addChangeListener(new ChangeListener() { |
|
|
|
|
|
public void stateChanged(ChangeEvent e) { |
|
|
|
|
|
|
|
|
theTabs.addChangeListener(new ChangeListener() |
|
|
|
|
|
{ |
|
|
|
|
|
public void stateChanged(ChangeEvent e) |
|
|
|
|
|
{ |
|
|
clipboardPlugin.pluginChanged(getFocussedPlugin()); |
|
|
clipboardPlugin.pluginChanged(getFocussedPlugin()); |
|
|
} |
|
|
} |
|
|
}); |
|
|
}); |
|
|
//Setup pluggable screens in here |
|
|
//Setup pluggable screens in here |
|
|
plugs = getPluginArray(this); |
|
|
plugs = getPluginArray(this); |
|
|
for(int i = 0; i < plugs.size(); i++) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
for (int i = 0; i < plugs.size(); i++) { |
|
|
GUIPlugin plug = (GUIPlugin) plugs.get(i); |
|
|
GUIPlugin plug = (GUIPlugin) plugs.get(i); |
|
|
if(plug.displaysTab()) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (plug.displaysTab()) { |
|
|
theTabs.addTab(plug.getTabText(), plug); |
|
|
theTabs.addTab(plug.getTabText(), plug); |
|
|
theTabs.setEnabledAt(theTabs.getComponentCount() - 1, plug.isEnabled()); |
|
|
theTabs.setEnabledAt(theTabs.getComponentCount() - 1, plug.isEnabled()); |
|
|
} |
|
|
} |
|
|
if(plug.getMenu() != null) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (plug.getMenu() != null) { |
|
|
menuBar.add(plug.getMenu()); |
|
|
menuBar.add(plug.getMenu()); |
|
|
} |
|
|
} |
|
|
if(plug.getToolBar() != null) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (plug.getToolBar() != null) { |
|
|
toolPanel.add(plug.getToolBar()); |
|
|
toolPanel.add(plug.getToolBar()); |
|
|
} |
|
|
} |
|
|
if(plug.getOptions() != null) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (plug.getOptions() != null) { |
|
|
options.addPanel(plug.getOptions()); |
|
|
options.addPanel(plug.getOptions()); |
|
|
} |
|
|
} |
|
|
if(plug instanceof userinterface.log.GUILog) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (plug instanceof userinterface.log.GUILog) { |
|
|
logPlug = (userinterface.log.GUILog) plug; |
|
|
logPlug = (userinterface.log.GUILog) plug; |
|
|
} |
|
|
} |
|
|
prism.getSettings().addSettingsListener(plug); |
|
|
prism.getSettings().addSettingsListener(plug); |
|
|
@ -328,7 +347,8 @@ public class GUIPrism extends JFrame |
|
|
fontIncrease.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_I)); |
|
|
fontIncrease.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_I)); |
|
|
fontIncrease.putValue(Action.NAME, "Increase font size"); |
|
|
fontIncrease.putValue(Action.NAME, "Increase font size"); |
|
|
fontIncrease.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFontIncrease.png")); |
|
|
fontIncrease.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFontIncrease.png")); |
|
|
fontIncrease.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_EQUALS, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask() | InputEvent.SHIFT_MASK)); |
|
|
|
|
|
|
|
|
fontIncrease.putValue(Action.ACCELERATOR_KEY, |
|
|
|
|
|
KeyStroke.getKeyStroke(KeyEvent.VK_EQUALS, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask() | InputEvent.SHIFT_MASK)); |
|
|
|
|
|
|
|
|
optionsMenu.add(fontIncrease); |
|
|
optionsMenu.add(fontIncrease); |
|
|
optionsMenu.setMnemonic('I'); |
|
|
optionsMenu.setMnemonic('I'); |
|
|
@ -403,10 +423,8 @@ public class GUIPrism extends JFrame |
|
|
public void adjustFont(int adjust) |
|
|
public void adjustFont(int adjust) |
|
|
{ |
|
|
{ |
|
|
Object[] objs = UIManager.getLookAndFeel().getDefaults().keySet().toArray(); |
|
|
Object[] objs = UIManager.getLookAndFeel().getDefaults().keySet().toArray(); |
|
|
for (int i = 0; i < objs.length; i++) |
|
|
|
|
|
{ |
|
|
|
|
|
if (objs[i].toString().toUpperCase().indexOf(".FONT") != -1) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
for (int i = 0; i < objs.length; i++) { |
|
|
|
|
|
if (objs[i].toString().toUpperCase().indexOf(".FONT") != -1) { |
|
|
Font font = UIManager.getFont(objs[i]); |
|
|
Font font = UIManager.getFont(objs[i]); |
|
|
font = font.deriveFont((float) (font.getSize() + adjust)); |
|
|
font = font.deriveFont((float) (font.getSize() + adjust)); |
|
|
UIManager.put(objs[i], new FontUIResource(font)); |
|
|
UIManager.put(objs[i], new FontUIResource(font)); |
|
|
@ -418,7 +436,6 @@ public class GUIPrism extends JFrame |
|
|
repaint(); |
|
|
repaint(); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
//EXITERS |
|
|
//EXITERS |
|
|
public void exit() |
|
|
public void exit() |
|
|
{ |
|
|
{ |
|
|
@ -452,7 +469,8 @@ public class GUIPrism extends JFrame |
|
|
} |
|
|
} |
|
|
}*/ |
|
|
}*/ |
|
|
|
|
|
|
|
|
if (doExit) System.exit(0); |
|
|
|
|
|
|
|
|
if (doExit) |
|
|
|
|
|
System.exit(0); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
//ACCESS METHODS |
|
|
//ACCESS METHODS |
|
|
@ -489,8 +507,7 @@ public class GUIPrism extends JFrame |
|
|
public static ImageIcon getIconFromImage(String file) |
|
|
public static ImageIcon getIconFromImage(String file) |
|
|
{ |
|
|
{ |
|
|
URL url = GUIPrism.class.getClassLoader().getResource("images/" + file); |
|
|
URL url = GUIPrism.class.getClassLoader().getResource("images/" + file); |
|
|
if (url == null) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (url == null) { |
|
|
System.out.println("Warning: Failed to load icon file \"" + file + "\""); |
|
|
System.out.println("Warning: Failed to load icon file \"" + file + "\""); |
|
|
return null; |
|
|
return null; |
|
|
} |
|
|
} |
|
|
@ -537,26 +554,17 @@ public class GUIPrism extends JFrame |
|
|
*/ |
|
|
*/ |
|
|
public boolean processGUIEvent(GUIEvent e) |
|
|
public boolean processGUIEvent(GUIEvent e) |
|
|
{ |
|
|
{ |
|
|
if(e instanceof GUIComputationEvent) |
|
|
|
|
|
{ |
|
|
|
|
|
if(e.getID() == GUIComputationEvent.COMPUTATION_START) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (e instanceof GUIComputationEvent) { |
|
|
|
|
|
if (e.getID() == GUIComputationEvent.COMPUTATION_START) { |
|
|
prismOptions.setEnabled(false); |
|
|
prismOptions.setEnabled(false); |
|
|
} |
|
|
|
|
|
else if(e.getID() == GUIComputationEvent.COMPUTATION_DONE) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} else if (e.getID() == GUIComputationEvent.COMPUTATION_DONE) { |
|
|
prismOptions.setEnabled(true); |
|
|
prismOptions.setEnabled(true); |
|
|
appendWarningsNoteToTaskBarText(prism.getMainLog()); |
|
|
appendWarningsNoteToTaskBarText(prism.getMainLog()); |
|
|
} |
|
|
|
|
|
else if(e.getID() == GUIComputationEvent.COMPUTATION_ERROR) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} else if (e.getID() == GUIComputationEvent.COMPUTATION_ERROR) { |
|
|
prismOptions.setEnabled(true); |
|
|
prismOptions.setEnabled(true); |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
else if (e instanceof GUIExitEvent) |
|
|
|
|
|
{ |
|
|
|
|
|
if(e.getID() == GUIExitEvent.CANCEL_EXIT) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
} else if (e instanceof GUIExitEvent) { |
|
|
|
|
|
if (e.getID() == GUIExitEvent.CANCEL_EXIT) { |
|
|
doExit = false; |
|
|
doExit = false; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
@ -570,15 +578,12 @@ public class GUIPrism extends JFrame |
|
|
*/ |
|
|
*/ |
|
|
public void enableTab(GUIPlugin tab, boolean enable) |
|
|
public void enableTab(GUIPlugin tab, boolean enable) |
|
|
{ |
|
|
{ |
|
|
for(int i = 0; i < theTabs.getComponentCount(); i++) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
for (int i = 0; i < theTabs.getComponentCount(); i++) { |
|
|
Component c = theTabs.getComponentAt(i); |
|
|
Component c = theTabs.getComponentAt(i); |
|
|
if(c instanceof GUIPlugin) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (c instanceof GUIPlugin) { |
|
|
GUIPlugin pl = (GUIPlugin) c; |
|
|
GUIPlugin pl = (GUIPlugin) c; |
|
|
|
|
|
|
|
|
if(pl == tab) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (pl == tab) { |
|
|
theTabs.setEnabledAt(i, enable); |
|
|
theTabs.setEnabledAt(i, enable); |
|
|
break; |
|
|
break; |
|
|
} |
|
|
} |
|
|
@ -599,11 +604,9 @@ public class GUIPrism extends JFrame |
|
|
*/ |
|
|
*/ |
|
|
public void showTab(GUIPlugin tab) |
|
|
public void showTab(GUIPlugin tab) |
|
|
{ |
|
|
{ |
|
|
for(int i=0; i<theTabs.getComponentCount(); i++) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
for (int i = 0; i < theTabs.getComponentCount(); i++) { |
|
|
Component c = theTabs.getComponentAt(i); |
|
|
Component c = theTabs.getComponentAt(i); |
|
|
if(c == tab) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (c == tab) { |
|
|
theTabs.setSelectedIndex(i); |
|
|
theTabs.setSelectedIndex(i); |
|
|
break; |
|
|
break; |
|
|
} |
|
|
} |
|
|
@ -613,8 +616,7 @@ public class GUIPrism extends JFrame |
|
|
/** This shows the GUIPlugin associated with the log. */ |
|
|
/** This shows the GUIPlugin associated with the log. */ |
|
|
public void showLogTab() |
|
|
public void showLogTab() |
|
|
{ |
|
|
{ |
|
|
if(logPlug != null) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (logPlug != null) { |
|
|
showTab(logPlug); |
|
|
showTab(logPlug); |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
@ -695,7 +697,8 @@ public class GUIPrism extends JFrame |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
public static GUIClipboard getClipboardPlugin() { |
|
|
|
|
|
|
|
|
public static GUIClipboard getClipboardPlugin() |
|
|
|
|
|
{ |
|
|
return clipboardPlugin; |
|
|
return clipboardPlugin; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |