Browse Source

Fix: Allow -javamaxmem to be passed to the GUI (xprism) too.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10488 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
commit
3abbac6491
  1. 29
      prism/src/userinterface/GUIPrism.java

29
prism/src/userinterface/GUIPrism.java

@ -28,15 +28,18 @@
package userinterface; package userinterface;
//Java Packages //Java Packages
import java.util.*; import java.util.*;
import java.util.List;
import java.io.*; import java.io.*;
import java.net.*; import java.net.*;
import java.awt.*; import java.awt.*;
import java.awt.event.*; import java.awt.event.*;
import javax.swing.*; import javax.swing.*;
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.*;
import javax.swing.plaf.metal.*; import javax.swing.plaf.metal.*;
//Prism Packages //Prism Packages
import prism.*; import prism.*;
import userinterface.util.*; import userinterface.util.*;
@ -376,15 +379,23 @@ public class GUIPrism extends JFrame
pack(); pack();
} }
public void passCLArgs(String args[])
{
// just before we get started, pass any command-line args to all plugins
for(int i = 0; i < plugs.size(); i++)
{
GUIPlugin plug = (GUIPlugin)plugs.get(i);
plug.takeCLArgs(args);
}
}
public void passCLArgs(String args[])
{
// just before we get started, pass any command-line args to all plugins
// we first remove the -javamaxmem argument, if present
List<String> argsCopy = new ArrayList<String>();
for (int i = 0; i < args.length; i++) {
if (args[i].equals("-javamaxmem")) {
i++;
} else {
argsCopy.add(args[i]);
}
}
for (int i = 0; i < plugs.size(); i++) {
GUIPlugin plug = (GUIPlugin) plugs.get(i);
plug.takeCLArgs(argsCopy.toArray(new String[0]));
}
}
/** /**
* Adjust the main font for the GUI (+1 = one size up, -1 = one size down) * Adjust the main font for the GUI (+1 = one size up, -1 = one size down)

Loading…
Cancel
Save