s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Auto format 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7370 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
6d32987de0
commit
63c53729fe
1 changed files with 218 additions and 261 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 145
      prism/src/userinterface/properties/GUIGraphHandler.java

145
prism/src/userinterface/properties/GUIGraphHandler.java
View File

@ -83,9 +83,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
private JMenu zoomMenu, exportMenu, importMenu;
private GUIPrismFileFilter imagesFilter[], xmlFilter[], matlabFilter[],
OpenDocumentChartFilter[], OpenDocumentSpreadsheetFilter[],
CSVFilter[], GNUFilter[], DATFilter[];
private GUIPrismFileFilter imagesFilter[], xmlFilter[], matlabFilter[], OpenDocumentChartFilter[], OpenDocumentSpreadsheetFilter[], CSVFilter[],
GNUFilter[], DATFilter[];
private PrintRequestAttributeSet attributes;
@ -262,8 +261,6 @@ public class GUIGraphHandler extends JPanel implements MouseListener
exportXML.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png"));
exportXML.putValue(Action.LONG_DESCRIPTION, "Export graph as a PRISM graph file.");
exportImageJPG = new AbstractAction()
{
public void actionPerformed(ActionEvent e)
@ -314,12 +311,9 @@ public class GUIGraphHandler extends JPanel implements MouseListener
return;
Graph mgm = models.get(theTabs.getSelectedIndex());
try
{
try {
mgm.exportToMatlab(plug.getChooserFile());
}
catch(IOException ex)
{
} catch (IOException ex) {
plug.error("Could not export Matlab file:\n" + ex.getMessage());
}
}
@ -331,7 +325,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
exportOpenDocumentChart = new AbstractAction()
{
public void actionPerformed(ActionEvent e) {
public void actionPerformed(ActionEvent e)
{
/* if (plug.showSaveFileDialog(OpenDocumentChartFilter, OpenDocumentChartFilter[0]) != JFileChooser.APPROVE_OPTION)
return;
GraphView mgv = (GraphView)views.get(
@ -351,7 +346,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
exportOpenDocumentSpreadsheet = new AbstractAction()
{
public void actionPerformed(ActionEvent e) {
public void actionPerformed(ActionEvent e)
{
/*if (plug.showSaveFileDialog(OpenDocumentSpreadsheetFilter, OpenDocumentSpreadsheetFilter[0]) != JFileChooser.APPROVE_OPTION)
return;
GraphView mgv = (GraphView)views.get(
@ -394,9 +390,7 @@ public class GUIGraphHandler extends JPanel implements MouseListener
{
public void actionPerformed(ActionEvent e)
{
Graph mgm = models.get(
theTabs.getSelectedIndex()
);
Graph mgm = models.get(theTabs.getSelectedIndex());
if (plug.showSaveFileDialog(GNUFilter, GNUFilter[0]) != JFileChooser.APPROVE_OPTION)
return;
@ -422,16 +416,11 @@ public class GUIGraphHandler extends JPanel implements MouseListener
{
public void actionPerformed(ActionEvent e)
{
Graph graph = models.get(
theTabs.getSelectedIndex()
);
Graph graph = models.get(theTabs.getSelectedIndex());
if (!graph.getDisplaySettings().getBackgroundColor().equals(Color.white))
{
if (plug.questionYesNo(
"Your graph has a coloured background, this background will show up on the \n"+
"printout. Would you like to make the current background colour white?") == 0)
{
if (!graph.getDisplaySettings().getBackgroundColor().equals(Color.white)) {
if (plug.questionYesNo("Your graph has a coloured background, this background will show up on the \n"
+ "printout. Would you like to make the current background colour white?") == 0) {
graph.getDisplaySettings().setBackgroundColor(Color.white);
}
}
@ -497,72 +486,49 @@ public class GUIGraphHandler extends JPanel implements MouseListener
public void saveImage(GUIImageExportDialog imageDialog)
{
if (!imageDialog.isCancelled())
{
if (!imageDialog.isCancelled()) {
Graph graph = getModel(theTabs.getSelectedIndex());
/* If background is not white, and it will show up, then lets warn everyone. */
if (!graph.getDisplaySettings().getBackgroundColor().equals(Color.white) && (imageDialog.getImageType() != GUIImageExportDialog.PNG || !imageDialog.getAlpha()))
{
if (plug.questionYesNo(
"Your graph has a coloured background, this background will show up on the \n"+
"exported image. Would you like to make the current background colour white?") == 0)
{
if (!graph.getDisplaySettings().getBackgroundColor().equals(Color.white)
&& (imageDialog.getImageType() != GUIImageExportDialog.PNG || !imageDialog.getAlpha())) {
if (plug.questionYesNo("Your graph has a coloured background, this background will show up on the \n"
+ "exported image. Would you like to make the current background colour white?") == 0) {
graph.getDisplaySettings().setBackgroundColor(Color.white);
}
}
if (imageDialog.getImageType() == GUIImageExportDialog.JPEG)
{
if (imageDialog.getImageType() == GUIImageExportDialog.JPEG) {
if (plug.showSaveFileDialog(imagesFilter, imagesFilter[1]) != JFileChooser.APPROVE_OPTION)
return;
try
{
try {
graph.exportToJPEG(plug.getChooserFile(), imageDialog.getExportWidth(), imageDialog.getExportHeight());
}
catch (GraphException ex)
{
} catch (GraphException ex) {
plug.error("Could not export JPEG file:\n" + ex.getMessage());
}
catch (IOException ex)
{
} catch (IOException ex) {
plug.error("Could not export JPEG file:\n" + ex.getMessage());
}
}
else if (imageDialog.getImageType() == GUIImageExportDialog.PNG)
{
} else if (imageDialog.getImageType() == GUIImageExportDialog.PNG) {
if (plug.showSaveFileDialog(imagesFilter, imagesFilter[0]) != JFileChooser.APPROVE_OPTION)
return;
try
{
try {
graph.exportToPNG(plug.getChooserFile(), imageDialog.getExportWidth(), imageDialog.getExportHeight(), imageDialog.getAlpha());
}
catch (GraphException ex)
{
} catch (GraphException ex) {
plug.error("Could not export PNG file:\n" + ex.getMessage());
}
catch (IOException ex)
{
} catch (IOException ex) {
plug.error("Could not export PNG file:\n" + ex.getMessage());
}
}
else if (imageDialog.getImageType() == GUIImageExportDialog.EPS)
{
} else if (imageDialog.getImageType() == GUIImageExportDialog.EPS) {
if (plug.showSaveFileDialog(imagesFilter, imagesFilter[2]) != JFileChooser.APPROVE_OPTION)
return;
try
{
try {
graph.exportToEPS(plug.getChooserFile(), imageDialog.getExportWidth(), imageDialog.getExportHeight());
}
catch (GraphException ex)
{
} catch (GraphException ex) {
plug.error("Could not export EPS file:\n" + ex.getMessage());
}
catch (IOException ex)
{
} catch (IOException ex) {
plug.error("Could not export EPS file:\n" + ex.getMessage());
}
}
@ -587,7 +553,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
menu.add(exportXML);
menu.add(exportImagePNG);
menu.add(exportImageEPS);
menu.add(exportImageJPG);menu.add(exportMatlab);
menu.add(exportImageJPG);
menu.add(exportMatlab);
menu.add(exportOpenDocumentChart);
menu.add(exportOpenDocumentSpreadsheet);
menu.add(exportCSV);
@ -615,13 +582,11 @@ public class GUIGraphHandler extends JPanel implements MouseListener
boolean nameNew;
int counter = 1;
while (true)
{
while (true) {
name = "Graph " + (counter);
nameNew = true;
for(int i = 0; i < theTabs.getComponentCount(); i++)
{
for (int i = 0; i < theTabs.getComponentCount(); i++) {
if (theTabs.getTitleAt(i).equals(name))
nameNew = false;
}
@ -660,10 +625,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
public void jumpToGraph(Graph m)
{
for(int i = 0; i < models.size(); i++)
{
if(m == models.get(i))
{
for (int i = 0; i < models.size(); i++) {
if (m == models.get(i)) {
theTabs.setSelectedComponent(m);
break;
}
@ -677,10 +640,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
public Graph getModel(String tabHeader)
{
for(int i = 0; i < theTabs.getComponentCount(); i++)
{
if(theTabs.getTitleAt(i).equals(tabHeader))
{
for (int i = 0; i < theTabs.getComponentCount(); i++) {
if (theTabs.getTitleAt(i).equals(tabHeader)) {
return getModel(i);
}
}
@ -700,8 +661,7 @@ public class GUIGraphHandler extends JPanel implements MouseListener
// User right clicked on a tab
public void mousePressed(MouseEvent e)
{
if(e.isPopupTrigger())
{
if (e.isPopupTrigger()) {
popUpTriggered(e);
}
}
@ -718,8 +678,7 @@ public class GUIGraphHandler extends JPanel implements MouseListener
public void mouseReleased(MouseEvent e)
{
if(e.isPopupTrigger())
{
if (e.isPopupTrigger()) {
popUpTriggered(e);
}
}
@ -728,11 +687,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
{
if (e.getSource() == theTabs)//just show the background popup
{
int index = theTabs.indexAtLocation(e.getX(), e.getY());
if (index != -1)
{
if (index != -1) {
graphOptions.setEnabled(true);
zoomMenu.setEnabled(true);
@ -745,9 +701,7 @@ public class GUIGraphHandler extends JPanel implements MouseListener
theTabs.setSelectedIndex(index);
this.graphMenu.show(theTabs, e.getX(), e.getY());
}
else
{
} else {
graphOptions.setEnabled(false);
zoomMenu.setEnabled(false);
@ -762,10 +716,8 @@ public class GUIGraphHandler extends JPanel implements MouseListener
return;
}
for(int i = 0; i < models.size(); i++)
{
if (e.getSource() == models.get(i))
{
for (int i = 0; i < models.size(); i++) {
if (e.getSource() == models.get(i)) {
graphOptions.setEnabled(true);
zoomMenu.setEnabled(true);
@ -790,7 +742,12 @@ public class GUIGraphHandler extends JPanel implements MouseListener
// don't implement these for tabs
//public void mouseClicked(MouseEvent e) { }
public void mouseEntered(MouseEvent e) { }
public void mouseExited(MouseEvent e) { }
public void mouseEntered(MouseEvent e)
{
}
public void mouseExited(MouseEvent e)
{
}
}
Write Preview
Loading…
Cancel
Save