|
@@ -25,6 +25,7 @@ public class OptionsDialog extends JDialog {
|
|
|
private JComboBox<String> display;
|
|
|
private JButton speichern;
|
|
|
private JComboBox<String> run;
|
|
|
+ private JComboBox<String> collapse;
|
|
|
private JTextField fSize;
|
|
|
private int tempFSize = 12;
|
|
|
|
|
@@ -32,6 +33,7 @@ public class OptionsDialog extends JDialog {
|
|
|
{
|
|
|
public int layoutDisplaySelection = 0;
|
|
|
public int runStepsSelection = 0;
|
|
|
+ public int autoCollapse = 0;
|
|
|
public int fontSize = 12;
|
|
|
}
|
|
|
|
|
@@ -40,7 +42,7 @@ public class OptionsDialog extends JDialog {
|
|
|
OptionsDialog()
|
|
|
{
|
|
|
setTitle( "Preferences" );
|
|
|
- setLayout( new GridLayout( 4, 2 ) );
|
|
|
+ setLayout( new GridLayout( 5, 2 ) );
|
|
|
add( new JLabel( "Display layouts:" ) );
|
|
|
String[] displayValues = { "All", "Only current" };
|
|
|
display = new JComboBox<String>( displayValues );
|
|
@@ -49,6 +51,10 @@ public class OptionsDialog extends JDialog {
|
|
|
String[] runValues = { "All", "Only expanded" };
|
|
|
run = new JComboBox<String>( runValues );
|
|
|
add( run );
|
|
|
+ add( new JLabel( "Automatically collapse pseudocode:" ) );
|
|
|
+ String[] collapseValues = { "No", "Yes" };
|
|
|
+ collapse = new JComboBox<String>( collapseValues );
|
|
|
+ add( collapse );
|
|
|
add( new JLabel( "Font size:" ) );
|
|
|
fSize = new JTextField( "12" );
|
|
|
add( fSize );
|
|
@@ -67,10 +73,12 @@ public class OptionsDialog extends JDialog {
|
|
|
try {
|
|
|
boolean change = options.layoutDisplaySelection != display.getSelectedIndex() ||
|
|
|
options.runStepsSelection != run.getSelectedIndex() ||
|
|
|
- tempFSize != options.fontSize;
|
|
|
+ tempFSize != options.fontSize ||
|
|
|
+ options.autoCollapse != collapse.getSelectedIndex();
|
|
|
options.layoutDisplaySelection = display.getSelectedIndex();
|
|
|
options.runStepsSelection = run.getSelectedIndex();
|
|
|
options.fontSize = tempFSize;
|
|
|
+ options.autoCollapse = collapse.getSelectedIndex();
|
|
|
if( change )
|
|
|
{
|
|
|
for( ActionListener l : listeners )
|
|
@@ -93,6 +101,11 @@ public class OptionsDialog extends JDialog {
|
|
|
setLocation( Toolkit.getDefaultToolkit().getScreenSize().width / 2 - getWidth() / 2, Toolkit.getDefaultToolkit().getScreenSize().height / 2 - getHeight() / 2 );
|
|
|
}
|
|
|
|
|
|
+ public int getAutoCollapseOption()
|
|
|
+ {
|
|
|
+ return options.autoCollapse;
|
|
|
+ }
|
|
|
+
|
|
|
public int getLayerDisplayOption()
|
|
|
{
|
|
|
return options.layoutDisplaySelection;
|