Commit 09f80284 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge branch 'mulbrichFix1554' into 'master'

fixing 1554, glitch in the GUI

See merge request key/key!357
parents 9a2dbaee f9b7308f
......@@ -23,7 +23,11 @@ import net.miginfocom.swing.MigLayout;
import org.jetbrains.annotations.Nullable;
import javax.swing.*;
import javax.swing.event.DocumentEvent;
import javax.swing.event.DocumentListener;
import java.awt.*;
import java.util.Arrays;
import java.util.List;
/**
* Extension of {@link SimpleSettingsPanel} which uses {@link MigLayout} to
......@@ -179,7 +183,8 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
* @param <T>
* @return
*/
protected <T> JComboBox<T> addComboBox(String info, int selectionIndex,
protected <T> JComboBox<T> addComboBox(String title,
String info, int selectionIndex,
@Nullable Validator<T> validator, T... items) {
JComboBox<T> comboBox = new JComboBox<>(items);
comboBox.setSelectedIndex(selectionIndex);
......@@ -194,7 +199,7 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
}
});
if (info != null && !info.isEmpty()) {
pCenter.add(new JLabel());
pCenter.add(new JLabel(title));
pCenter.add(comboBox);
JLabel infoButton = createHelpLabel(info);
pCenter.add(infoButton, new CC().wrap());
......@@ -215,6 +220,14 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
addRowWithHelp(helpText, label, component);
}
protected JTextArea addTextArea(String title, String text, String info, final Validator<String> validator) {
JScrollPane field = createTextArea(text, validator);
addTitledComponent(title, field, info);
return (JTextArea) field.getViewport().getView();
}
/**
* @param title
* @param text
......@@ -228,6 +241,7 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
return field;
}
protected JTextField addTextField(String title, String text, String info, final Validator<String> validator,
JComponent additionalActions) {
JTextField field = createTextField(text, validator);
......@@ -253,6 +267,22 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
return field;
}
protected void addRadioButtons(String heading, Object[] alternatives, String description) {
addRadioButtons(heading, Arrays.asList(alternatives), description);
}
protected void addRadioButtons(String title, List<?> alternatives, String description) {
JPanel items = new JPanel(new GridLayout(alternatives.size(), 1));
ButtonGroup bg = new ButtonGroup();
for (Object alt : alternatives) {
JRadioButton radioButton = new JRadioButton(alt.toString());
radioButton.putClientProperty("object", alt);
bg.add(radioButton);
items.add(radioButton);
}
addTitledComponent(title, items, description);
}
/**
* Add a separator line with the given title.
*
......
......@@ -18,12 +18,14 @@ import de.uka.ilkd.key.gui.colors.ColorSettings;
import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid;
import de.uka.ilkd.key.gui.fonticons.IconFontSwing;
import org.jetbrains.annotations.Nullable;
import org.key_project.util.java.StringUtil;
import javax.swing.*;
import javax.swing.event.ChangeEvent;
import javax.swing.event.ChangeListener;
import javax.swing.event.DocumentEvent;
import javax.swing.event.DocumentListener;
import javax.swing.text.JTextComponent;
import java.awt.*;
import java.text.Format;
......@@ -60,10 +62,11 @@ public class SimpleSettingsPanel extends JPanel {
pNorth.add(lblHead);
pNorth.add(lblSubhead);
pNorth.add(new JSeparator());
add(pNorth, BorderLayout.NORTH);
add(pCenter, BorderLayout.CENTER);
JScrollPane scrollPane = new JScrollPane(pCenter);
scrollPane.getHorizontalScrollBar().setUnitIncrement(10);
scrollPane.getVerticalScrollBar().setUnitIncrement(10);
add(scrollPane, BorderLayout.CENTER);
}
public void setHeaderText(String text) {
......@@ -75,10 +78,14 @@ public class SimpleSettingsPanel extends JPanel {
}
protected void demarkComponentAsErrornous(JComponent component) {
component.setBackground(Color.white);//find color
Object col = component.getClientProperty("saved_background_color");
if (col instanceof Color) {
component.setBackground((Color) col);
}
}
protected void markComponentAsErrornous(JComponent component, String error) {
component.putClientProperty("saved_background_color", component.getBackground());
component.setBackground(COLOR_ERROR.get());
component.setToolTipText(error);
}
......@@ -98,6 +105,15 @@ public class SimpleSettingsPanel extends JPanel {
return checkBox;
}
protected JScrollPane createTextArea(String text, Validator<String> validator) {
JTextArea area = new JTextArea(text);
area.setRows(5);
area.getDocument().addDocumentListener(new DocumentValidatorAdapter(area, validator));
JScrollPane scrollArea = new JScrollPane(area);
return scrollArea;
}
protected JTextField createTextField(String text, final @Nullable Validator<String> validator) {
JTextField field = new JTextField(text);
field.getDocument().addDocumentListener(new DocumentValidatorAdapter(field, validator));
......@@ -124,8 +140,14 @@ public class SimpleSettingsPanel extends JPanel {
public static JLabel createHelpLabel(String s) {
if (s == null || s.isEmpty())
s = "";
else
s = "<html>" + s.replaceAll("\n", "<br>");
else {
String brokenLines = StringUtil.wrapLines(s);
s = "<html>" +
brokenLines.replace("<", "&lt;").
replace(">", "&gt;").
replace("\n", "<br>");
}
JLabel infoButton = new JLabel(
IconFontSwing.buildIcon(FontAwesomeSolid.QUESTION_CIRCLE, 16f));
infoButton.setToolTipText(s);
......@@ -157,10 +179,10 @@ public class SimpleSettingsPanel extends JPanel {
}
private class DocumentValidatorAdapter implements DocumentListener {
private final JTextField field;
private final JTextComponent field;
private final @Nullable Validator<String> validator;
private DocumentValidatorAdapter(JTextField field, @Nullable Validator<String> validator) {
private DocumentValidatorAdapter(JTextComponent field, @Nullable Validator<String> validator) {
this.field = field;
this.validator = validator;
}
......
......@@ -35,8 +35,8 @@ public class StandardUISettings extends SettingsPanel implements SettingsProvide
private final JCheckBox chkMinimizeInteraction;
private final JComboBox<String> spFontSizeTreeSequent;
private final JCheckBox chkEnsureSourceConsistency;
private final JTextField txtClutterRules;
private final JTextField txtClutterRuleSets;
private final JTextArea txtClutterRules;
private final JTextArea txtClutterRuleSets;
public StandardUISettings() {
setHeaderText(getDescription());
......@@ -59,15 +59,15 @@ public class StandardUISettings extends SettingsPanel implements SettingsProvide
chkShowWholeTacletCB =
addCheckBox("Show whole taclet", "Pretty-print whole Taclet including \n" +
"'name', 'find', 'varCond' and 'heuristics'", false, emptyValidator());
"'name', 'find', 'varCond' and 'heuristics'", false, emptyValidator());
chkShowUninstantiatedTaclet =
addCheckBox("Show uninstantiated taclet", "recommended for unexperienced users",
false, emptyValidator());
false, emptyValidator());
txtClutterRules = addTextField("Clutter rules", "", INFO_CLUTTER_RULE, emptyValidator());
txtClutterRuleSets =
addTextField("Clutter Rulesets", "", INFO_CLUTTER_RULESET, emptyValidator());
txtClutterRules = addTextArea("Clutter rules", "", INFO_CLUTTER_RULE, emptyValidator());
txtClutterRuleSets = addTextArea("Clutter Rulesets", "", INFO_CLUTTER_RULESET, emptyValidator());
chkPrettyPrint = addCheckBox("Pretty print terms", "", false, emptyValidator());
chkUseUnicode = addCheckBox("Use unicode", "", false, emptyValidator());
......@@ -96,8 +96,8 @@ public class StandardUISettings extends SettingsPanel implements SettingsProvide
GeneralSettings generalSettings = ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings();
txtClutterRules.setText(vs.clutterRules().value());
txtClutterRuleSets.setText(vs.clutterRuleSets().value());
txtClutterRules.setText(vs.clutterRules().value().replace(',', '\n'));
txtClutterRuleSets.setText(vs.clutterRuleSets().value().replace(',', '\n'));
spFontSizeGlobal.setValue(vs.getUIFontSizeFactor());
txtMaxTooltipLines.setValue(vs.getMaxTooltipLines());
......@@ -130,9 +130,8 @@ public class StandardUISettings extends SettingsPanel implements SettingsProvide
vs.setUIFontSizeFactor((Double) spFontSizeGlobal.getValue());
vs.setMaxTooltipLines((Integer) txtMaxTooltipLines.getValue());
vs.clutterRules().set(txtClutterRules.getText());
vs.clutterRuleSets().set(txtClutterRuleSets.getText());
vs.clutterRules().set(txtClutterRules.getText().replace('\n',','));
vs.clutterRuleSets().set(txtClutterRuleSets.getText().replace('\n',','));
vs.setShowWholeTaclet(chkShowWholeTacletCB.isSelected());
vs.setShowUninstantiatedTaclet(chkShowUninstantiatedTaclet.isSelected());
......
......@@ -35,12 +35,6 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin
public TacletOptionsSettings() {
setHeaderText(getDescription());
JScrollPane root = new JScrollPane();
root.getVerticalScrollBar().setUnitIncrement(10);
root.getHorizontalScrollBar().setUnitIncrement(10);
root.setViewportView(pCenter);
add(root, BorderLayout.CENTER);
pCenter.setLayout(new MigLayout(
new LC().fillX(),
new AC().fill().grow().gap("3mm")
......
......@@ -127,7 +127,7 @@ public class SMTSettingsProvider extends SettingsPanel implements SettingsProvid
}
private JComboBox<String> getProgressModeBox() {
return addComboBox(BUNDLE.getString(INFO_PROGRESS_MODE_BOX), 0,
return addComboBox("", BUNDLE.getString(INFO_PROGRESS_MODE_BOX), 0,
e -> settings.modeOfProgressDialog = progressModeBox.getSelectedIndex(),
getProgressMode(ProofIndependentSMTSettings.PROGRESS_MODE_USER),
getProgressMode(ProofIndependentSMTSettings.PROGRESS_MODE_CLOSE));
......
......@@ -3,32 +3,31 @@ PROGRESS_MODE_CLOSE=Close progress dialog after all solvers have finished
PROGRESS_MODE_CLOSE_FIRST=Close progress dialog after the first solver has finished
infoBound=Bitvector size for this type. Use a value larger than 0.
infoSaveToFilePanel=Activate this option to store the translations \
that are handed over to the externals solvers: \
1. Choose the folder.\
2. Specify the filename:\
\t%s: the solver's name\
\t%d: date\
\t%t: time\
\t%i: the goal's number\
\
Example: /home/translations/%d_%t_%i_%s.txt"\
\
that are handed over to the externals solvers: \n\
1. Choose the folder.\n\
2. Specify the filename:\n\
\t%s: the solver's name\n\
\t%d: date\n\
\t%t: time\n\
\t%i: the goal's number\n\
\n\
Example: /home/translations/%d_%t_%i_%s.txt"\n\
\n\
Remark: After every restart of KeY this option\
is deactivated.
infoProgressModeBox=1. Option: The progress dialog remains open after executing the solvers so that the user \
can decide whether he wants to accept the results.\
\
2. Option: The progress dialog is closed once the
external provers have done their work or the time limit\
infoProgressModeBox=1. Option: The progress dialog remains open after executing the solvers so that the user\
can decide whether he wants to accept the results.\n\
\n\
2. Option: The progress dialog is closed once the external provers have done their work or the time limit\
has been exceeded.
infoCheckForSupport=If this option is activated, each time before a solver is started\
it is checked whether the version of that solver is supported. If the version is not supported, a warning is\
presented in the progress dialog.
infoMaxProcesses=Maximal number or processes that are allowed to run concurrently
infoTimeoutField=Timeout for the external solvers in seconds. Fractions of a second are allowed. Example: 6.5
infoSolverName=There are two ways to make supported provers applicable for KeY:\
1. Specify the absolute path of the prover in the field 'Command'.\
2. Change the environment variable $PATH of your system, so that it\
infoSolverName=There are two ways to make supported provers applicable for KeY:\n\
1. Specify the absolute path of the prover in the field 'Command'.\n\
2. Change the environment variable $PATH of your system, so that it\n\
refers to the installed prover. In that case you must specify the name of the solver in 'Command'
infoSolverParameters=In this field you can specify which parameters are passed to the \
solver when the solver is started. Note that the default parameters are crucial for a stable run of the\
......@@ -36,7 +35,7 @@ infoSolverParameters=In this field you can specify which parameters are passed t
infoSolverCommand=The command for the solver.\
Either you specify the absolute path of your solver or just the command for starting it.\
In the latter case you have to modify the PATH-variable of your system.\
Please note that you also have to specify the filename extension\
Please note that you also have to specify the filename extension.\n\
For example: z3.exe
infoSolverSupport=For the KeY system only some particular versions of this solver \
have been tested. It is highly recommended to use those versions, because otherwise it is not guaranteed that\
......
......@@ -162,6 +162,67 @@ public final class StringUtil {
return string != null && substring != null ? string.contains(substring) : false;
}
/**
* Wrap lines in a string. It replaces ' ' by '\n' such that (in general)
* every line is at most {@code length} characters long. If there are no
* spaces within {@code length} characters, then the long strings will not
* be broken and lines may be longer.
*
* @param string the string to break. May contain spaces and newline
* characters
* @param length a positive number
* @return a string of the same length as the input in which some ' ' have
* been replaced by '\n'
*
* @author Mattias Ulbrich (under GPL)
*/
public static String wrapLines(String string, int length) {
assert length > 0;
StringBuilder sb = new StringBuilder(string);
int lastChange = -1;
int lastSpace = -1;
int nextSpace = string.indexOf(' ');
while(nextSpace >= 0) {
int nextNewLine = string.indexOf('\n', lastSpace + 1);
if(0 <= nextNewLine && nextNewLine < nextSpace) {
lastChange = lastSpace = nextNewLine;
} else if(nextSpace - lastChange >= length) {
// wrap needed!
if(lastChange == lastSpace) {
// but can't break any earlier.
sb.setCharAt(nextSpace, '\n');
lastChange = lastSpace = nextSpace;
} else {
sb.setCharAt(lastSpace, '\n');
lastChange = lastSpace;
}
} else {
lastSpace = nextSpace;
}
nextSpace = sb.indexOf(" ", lastSpace + 1);
}
return sb.toString();
}
/**
* Wrap lines in a string. It replaces ' ' by '\n' such that (in general)
* every line is at most 100 characters long. If there are no
* spaces within 100 characters, then the long strings will not
* be broken and lines may be longer.
*
* @param string the string to break. May contain spaces and newline
* characters
* @return a string of the same length as the input in which some ' ' have
* been replaced by '\n'
*
* @author Mattias Ulbrich (under GPL)
*/
public static String wrapLines(String string) {
return wrapLines(string, 100);
}
/**
* Converts the optional multi lined {@link String} in a single lined {@link String}
* by replacing all line breaks and tabs with a space.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment