diff --git a/build.gradle b/build.gradle index 6df46bffc01..61364ce00d4 100644 --- a/build.gradle +++ b/build.gradle @@ -334,6 +334,8 @@ subprojects { targetExclude 'build/**' // allows us to use spotless:off / spotless:on to keep pre-formatted sections + // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on" + // that must be used instead. toggleOffOn() removeUnusedImports() diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index ca24ef495c8..9eb702a8327 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -156,7 +156,8 @@ public Configuration asConfiguration() { if (!res.isEmpty()) return (Configuration) res.get(0); else - throw new RuntimeException(); + throw new RuntimeException("Error in configuration. Source: " + + ctx.start.getTokenSource().getSourceName()); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index e25b78cf31f..9ca06df9927 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1015,7 +1015,9 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(this, selected)); - proof.add(new ShowActiveTactletOptionsAction(this, selected)); + // We merge the old window to view the active taclet options with the window for all active + // settings + // proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); proof.add(showActiveSettingsAction); proof.add(new ShowProofStatistics(this, selected)); proof.add(new ShowKnownTypesAction(this, selected)); @@ -1027,7 +1029,8 @@ private JMenu createOptionsMenu() { options.setMnemonic(KeyEvent.VK_O); options.add(SettingsManager.getActionShowSettings(this)); - options.add(new TacletOptionsAction(this)); + // remove since taclet options should only be set through the general settings dialog + // options.add(new TacletOptionsAction(this)); options.add(new SMTOptionsAction(this)); // options.add(setupSpeclangMenu()); // legacy since only JML supported options.addSeparator(); @@ -1038,7 +1041,6 @@ private JMenu createOptionsMenu() { options.add(new JCheckBoxMenuItem(new EnsureSourceConsistencyToggleAction(this))); return options; - } private JMenu createHelpMenu() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java index c3d39655ee0..2478d14958a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java @@ -3,12 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions; +import java.util.Arrays; import java.util.Map.Entry; import java.util.Properties; -import javax.swing.JComponent; -import javax.swing.JScrollPane; -import javax.swing.JTable; -import javax.swing.JTextArea; +import javax.swing.*; import javax.swing.table.DefaultTableModel; import javax.swing.tree.DefaultMutableTreeNode; import javax.swing.tree.DefaultTreeModel; @@ -34,6 +32,7 @@ public class SettingsTreeModel extends DefaultTreeModel { private final ProofSettings proofSettings; private final ProofIndependentSettings independentSettings; + private OptionContentNode tacletOptionsItem; public SettingsTreeModel(ProofSettings proofSettings, ProofIndependentSettings independentSettings) { @@ -46,19 +45,27 @@ public SettingsTreeModel(ProofSettings proofSettings, private void generateTree() { DefaultMutableTreeNode root = (DefaultMutableTreeNode) this.getRoot(); - OptionContentNode proofSettingsNode = - generateOptionContentNode("Proof Settings", "These are the proof dependent settings."); - root.add(proofSettingsNode); - - // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); - ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - proofSettingsNode.add(generateTableNode("Taclets", choiceSettings)); - - Settings strategySettings = proofSettings.getStrategySettings(); - proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); - - Settings smtSettings = proofSettings.getSMTSettings(); - proofSettingsNode.add(generateTableNode("SMT", smtSettings)); + if (proofSettings == null) { + OptionContentNode proofSettingsNode = + generateOptionContentNode("Proof Settings", "There is currently no proof loaded!"); + root.add(proofSettingsNode); + } else { + OptionContentNode proofSettingsNode = + generateOptionContentNode("Proof Settings", + "These are the proof dependent settings."); + root.add(proofSettingsNode); + + // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); + ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); + tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); + proofSettingsNode.add(tacletOptionsItem); + + Settings strategySettings = proofSettings.getStrategySettings(); + proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); + + Settings smtSettings = proofSettings.getSMTSettings(); + proofSettingsNode.add(generateTableNode("SMT", smtSettings)); + } OptionContentNode independentSettingsNode = generateOptionContentNode( "Proof-Independent Settings", "These are the proof independent settings."); @@ -75,7 +82,10 @@ private void generateTree() { Settings viewSettings = independentSettings.getViewSettings(); independentSettingsNode.add(generateTableNode("View", viewSettings)); Settings termLabelSettings = independentSettings.getTermLabelSettings(); - proofSettingsNode.add(generateTableNode("Term Labels", termLabelSettings)); + // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the + // previous line, + // it should really be added to the independentSettingsNode + independentSettingsNode.add(generateTableNode("Term Labels", termLabelSettings)); } @@ -115,6 +125,7 @@ private JComponent generateScrollPane(String text) { JTextArea ta = new JTextArea(5, 20); ta.append(text); ta.setEditable(false); + ta.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); JScrollPane scrollpane = new JScrollPane(ta); return scrollpane; } @@ -130,6 +141,8 @@ private JComponent generateJTable(Properties properties) { i++; } + Arrays.sort(data, (a, b) -> a[0].toString().compareToIgnoreCase(b[0].toString())); + JTable table = new JTable(); DefaultTableModel tableModel = new DefaultTableModel() { @@ -143,9 +156,8 @@ public boolean isCellEditable(int row, int column) { }; tableModel.setDataVector(data, columnNames); - table.setModel(tableModel); - + table.setRowHeight(table.getRowHeight() + 10); JScrollPane scrollpane = new JScrollPane(table); return scrollpane; @@ -157,6 +169,7 @@ private OptionContentNode generateOptionContentNode(String title, String text) { return new OptionContentNode(title, generateScrollPane(text)); } - - + public OptionContentNode getTacletOptionsItem() { + return tacletOptionsItem; + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java index e32b368b999..40d266773b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java @@ -22,9 +22,6 @@ */ public class ShowActiveSettingsAction extends MainWindowAction { - /** - * - */ private static final long serialVersionUID = -3038735283059371442L; public ShowActiveSettingsAction(MainWindow mainWindow) { @@ -35,8 +32,12 @@ public ShowActiveSettingsAction(MainWindow mainWindow) { @Override public void actionPerformed(ActionEvent e) { + showDialog(); + } + + private ViewSettingsDialog showDialog() { ProofSettings settings = - (getMediator().getSelectedProof() == null) ? ProofSettings.DEFAULT_SETTINGS + (getMediator().getSelectedProof() == null) ? null : getMediator().getSelectedProof().getSettings(); SettingsTreeModel model = new SettingsTreeModel(settings, ProofIndependentSettings.DEFAULT_INSTANCE); @@ -44,6 +45,14 @@ public void actionPerformed(ActionEvent e) { dialog.setTitle("All active settings"); dialog.setLocationRelativeTo(mainWindow); dialog.setVisible(true); + return dialog; + } + + public void showAndFocusTacletOptions() { + ViewSettingsDialog dialog = showDialog(); + SettingsTreeModel model = (SettingsTreeModel) dialog.optionTree.getModel(); + OptionContentNode item = model.getTacletOptionsItem(); + dialog.getOptionTree().setSelectionPath(new TreePath(item.getPath())); } /** @@ -57,31 +66,33 @@ private class ViewSettingsDialog extends JDialog { public ViewSettingsDialog(TreeModel model, JComponent startComponent) { super(mainWindow); - this.getContentPane().setLayout(new BoxLayout(getContentPane(), BoxLayout.Y_AXIS)); - Box box = Box.createHorizontalBox(); - box.add(getSplitPane()); - this.getContentPane().add(box); - this.getContentPane().add(Box.createVerticalStrut(5)); - box = Box.createHorizontalBox(); - box.add(Box.createHorizontalStrut(5)); + Container cp = this.getContentPane(); + cp.setLayout(new BorderLayout()); + cp.add(getSplitPane(), BorderLayout.CENTER); + JButton okButton = new JButton("OK"); okButton.addActionListener(e -> dispose()); setDefaultCloseOperation(DISPOSE_ON_CLOSE); - box.add(okButton); - box.add(Box.createHorizontalStrut(5)); - this.getContentPane().add(box); + JPanel buttons = new JPanel(new FlowLayout()); + buttons.add(okButton); + cp.add(buttons, BorderLayout.SOUTH); + + JLabel announce = + new JLabel("This shows the active settings for the current proof.
" + + "To change settings for future proofs, use Options > Show Settings."); + announce.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); + cp.add(announce, BorderLayout.NORTH); + this.getOptionTree().setModel(model); getSplitPane().setRightComponent(startComponent); this.getOptionTree().getParent().setMinimumSize(getOptionTree().getPreferredSize()); - this.getContentPane().setPreferredSize(computePreferredSize(model)); + cp.setPreferredSize(computePreferredSize(model)); this.setDefaultCloseOperation(DISPOSE_ON_CLOSE); setIconImage(IconFactory.keyLogo()); this.pack(); this.setLocationRelativeTo(MainWindow.getInstance()); - - getRootPane().registerKeyboardAction((e) -> dispose(), KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_IN_FOCUSED_WINDOW); getRootPane().setDefaultButton(okButton); @@ -127,15 +138,14 @@ private JTree getOptionTree() { } } }); + optionTree.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); } return optionTree; } private JSplitPane getSplitPane() { if (splitPane == null) { - splitPane = new JSplitPane(); - splitPane.setAlignmentX(LEFT_ALIGNMENT); splitPane.setLeftComponent(new JScrollPane(getOptionTree())); splitPane.setRightComponent(getOptionPanel()); // splitPane.setResizeWeight(0.2); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java index 7ca4d776f79..46a724e3a02 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java @@ -4,60 +4,57 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; -import javax.swing.JOptionPane; -import javax.swing.JTextArea; -import javax.swing.text.JTextComponent; import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; -import de.uka.ilkd.key.proof.Proof; +/** + * Action to show a dialog with the taclet options valid for the currently + * selected proof. + * + * Now defers to the "Show Active Settings" action to show the taclet options. + */ public class ShowActiveTactletOptionsAction extends MainWindowAction { - /** - * - */ private static final long serialVersionUID = -7012564698194718532L; + private final ShowActiveSettingsAction action; - private final Proof proof; - - public ShowActiveTactletOptionsAction(MainWindow mainWindow, Proof proof) { + public ShowActiveTactletOptionsAction(MainWindow mainWindow, ShowActiveSettingsAction action) { super(mainWindow); setName("Show Active Taclet Options"); - - getMediator().enableWhenProofLoaded(this); - - this.proof = proof; + this.action = action; } @Override public void actionPerformed(ActionEvent e) { - showActivatedChoices(); + action.showAndFocusTacletOptions(); } - private void showActivatedChoices() { - Proof currentProof = proof == null ? getMediator().getSelectedProof() : proof; - if (currentProof == null) { - mainWindow.notify(new GeneralInformationEvent("No Options available.", - "If you wish to see Taclet Options " + "for a proof you have to load one first")); - } else { - StringBuilder message = new StringBuilder("Active Taclet Options:\n"); - int rows = 0; - int columns = 0; - for (final String choice : currentProof.getSettings().getChoiceSettings() - .getDefaultChoices().values()) { - message.append(choice).append("\n"); - rows++; - if (columns < choice.length()) { - columns = choice.length(); - } - } - final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns); - activeOptions.setEditable(false); - Object[] toDisplay = - { activeOptions, "These options can be changed in Options->Taclet Options" }; - JOptionPane.showMessageDialog(mainWindow, toDisplay, - "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE); - } - } + // @formatter:off + +// private void showActivatedChoices() { +// Proof currentProof = proof == null ? getMediator().getSelectedProof() : proof; +// if (currentProof == null) { +// mainWindow.notify(new GeneralInformationEvent("No Options available.", +// "If you wish to see Taclet Options " + "for a proof you have to load one first")); +// } else { +// StringBuilder message = new StringBuilder("Active Taclet Options:\n"); +// int rows = 0; +// int columns = 0; +// for (final String choice : currentProof.getSettings().getChoiceSettings() +// .getDefaultChoices().values()) { +// message.append(choice).append("\n"); +// rows++; +// if (columns < choice.length()) { +// columns = choice.length(); +// } +// } +// final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns); +// activeOptions.setEditable(false); +// Object[] toDisplay = +// { activeOptions, +// "These options can be changed in Options->Show Settings->Taclet Options" }; +// JOptionPane.showMessageDialog(mainWindow, toDisplay, +// "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE); +// } +// } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java index ffe05fd5e5d..215114b6d7e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java @@ -11,6 +11,9 @@ import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; import de.uka.ilkd.key.settings.ProofSettings; +// This class is not used anymore as taclet options should be set through the general settings +// dialog +@Deprecated public class TacletOptionsAction extends MainWindowAction { /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java index 1151dd47db8..b54d9b00823 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java @@ -108,7 +108,8 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings { defineDefault(SaveBundleAction.class, KeyEvent.VK_B, SHORTCUT_KEY_MASK); defineDefault(SaveFileAction.class, KeyEvent.VK_S, SHORTCUT_KEY_MASK); defineDefault(SettingsManager.ShowSettingsAction.class, KeyEvent.VK_N, SHORTCUT_KEY_MASK); - defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK); + // remove as the old menu should not be accessible anymore + // defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK); defineDefault(OpenFileAction.class, KeyEvent.VK_O, SHORTCUT_KEY_MASK); defineDefault(SearchInSequentAction.class, KeyEvent.VK_F, SHORTCUT_KEY_MASK); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java index c5a4f69b4af..e17eee82592 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java @@ -78,6 +78,7 @@ SettingsUi getUi() { private List apply() { List exc = new LinkedList<>(); apply(providers, exc); + return exc; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java index d0d0b1ef541..91bb112e251 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java @@ -158,7 +158,7 @@ public boolean remove(SettingsProvider o) { public static class ShowSettingsAction extends MainWindowAction { public ShowSettingsAction(MainWindow mainWindow) { super(mainWindow); - setName("Show Settings"); + setName("Settings"); setIcon(IconFactory.editFile(16)); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java index 64de412bda9..828b8852f0c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java @@ -190,6 +190,20 @@ public static JLabel createHelpLabel(String s) { return infoButton; } + public static JLabel createHelpTextLabel(String s) { + if (s == null || s.isEmpty()) { + s = ""; + } + if (s.contains("\n")) { + s = s.substring(0, s.indexOf('\n')); + } + + JLabel infoButton = new JLabel(s); + infoButton.setFont(infoButton.getFont().deriveFont(10f)); + infoButton.setBackground(Color.orange); + return infoButton; + } + public static JButton createHelpButton(Runnable callback) { var infoButton = new JButton(IconFontSwing.buildIcon(FontAwesomeSolid.QUESTION_CIRCLE, 16f)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 619716431e9..791f4e663a3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -15,9 +15,11 @@ import java.util.List; import java.util.stream.Collectors; import javax.swing.*; +import javax.swing.plaf.ColorUIResource; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ChoiceSettings; import de.uka.ilkd.key.settings.ProofSettings; @@ -43,6 +45,12 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin private ChoiceSettings settings; private boolean warnNoProof = true; + // to make the "No Proof Loaded" header invisible when a proof is loaded + private JLabel noProofLoadedHeader; + + private Proof loadedProof = null; + + public TacletOptionsSettings() { setHeaderText(getDescription()); pCenter.setLayout(new MigLayout(new LC().fillX(), new AC().fill().grow().gap("3mm"))); @@ -173,12 +181,10 @@ public static ChoiceEntry createChoiceEntry(String choice) { } protected void layoutHead() { - if (warnNoProof) { - JLabel lblHead2 = new JLabel("No Proof loaded. Taclet options may not be parsed."); - lblHead2.setIcon(IconFactory.WARNING_INCOMPLETE.get()); - lblHead2.setFont(lblHead2.getFont().deriveFont(14f)); - pNorth.add(lblHead2); - } + this.noProofLoadedHeader = new JLabel("No Proof loaded. Taclet options may not be parsed."); + noProofLoadedHeader.setIcon(IconFactory.WARNING_INCOMPLETE.get()); + noProofLoadedHeader.setFont(noProofLoadedHeader.getFont().deriveFont(14f)); + pNorth.add(noProofLoadedHeader); JLabel lblHead2 = new JLabel("Taclet options will take effect only on new proofs."); lblHead2.setIcon(IconFactory.WARNING_INCOMPLETE.get()); @@ -188,7 +194,8 @@ protected void layoutHead() { protected void layoutChoiceSelector() { pCenter.removeAll(); - category2Choice.keySet().stream().sorted().forEach(this::addCategory); + category2Choice.keySet().stream().sorted(String::compareToIgnoreCase) + .forEach(this::addCategory); } protected void addCategory(String cat) { @@ -196,46 +203,55 @@ protected void addCategory(String cat) { ChoiceEntry selectedChoice = findChoice(choices, category2Choice.get(cat)); String explanation = getExplanation(cat); - addTitleRow(cat); - ButtonGroup btnGroup = new ButtonGroup(); - for (ChoiceEntry c : choices) { - JRadioButton btn = addRadioButton(c, btnGroup); - if (c.equals(selectedChoice)) { - btn.setSelected(true); + JLabel title = createTitleRow(cat, selectedChoice); + JPanel selectPanel = new JPanel(new MigLayout(new LC().fillX(), new AC().fill().grow())); + + if (!warnNoProof) { + ButtonGroup btnGroup = new ButtonGroup(); + for (ChoiceEntry c : choices) { + JRadioButton btn = mkRadioButton(c, btnGroup); + if (c.equals(selectedChoice)) { + btn.setSelected(true); + } + btn.addActionListener(new ChoiceSettingsSetter(title, cat, c)); + selectPanel.add(btn, new CC().newline()); } - btn.addActionListener(new ChoiceSettingsSetter(cat, c.choice)); } - addExplanation(explanation); + selectPanel.add(mkExplanation(explanation), new CC().pad(0, 20, 0, 0).newline()); + + JPanel catEntry = createCollapsableTitlePane(title, selectPanel); + pCenter.add(catEntry, new CC().newline()); } - protected void addExplanation(String explanation) { - JTextArea explanationArea = new JTextArea(); + protected JComponent mkExplanation(String explanation) { + JTextArea explanationArea = new JTextArea() { + @Override + public void setBackground(Color bg) { + super.setBackground(bg); + } + }; explanationArea.setEditable(false); explanationArea.setLineWrap(true); explanationArea.setWrapStyleWord(true); - explanationArea.setText(explanation); + explanationArea.setText(explanation.trim()); explanationArea.setCaretPosition(0); - explanationArea.setBackground(getBackground()); - JPanel p = createCollapsibleTitlePane("Info", explanationArea); - pCenter.add(p, new CC().span().newline()); + explanationArea.setBackground(toNonUIColor(getBackground())); + return explanationArea; } - private @NonNull JPanel createCollapsibleTitlePane(String titleText, JComponent child) { + @NonNull + private JPanel createCollapsableTitlePane(JComponent title, JComponent child) { JPanel p = new JPanel(new BorderLayout()); - JPanel north = new JPanel(new BorderLayout()); - - p.setBorder(BorderFactory.createLineBorder(Color.black)); - JButton title = new JButton(titleText); - title.setContentAreaFilled(false); - title.setBorderPainted(false); - north.add(title, BorderLayout.WEST); + JPanel north = new JPanel(new FlowLayout(FlowLayout.LEFT)); + JLabel more = new JLabel(IconFactory.TREE_NODE_RETRACTED.get()); + north.add(more); + north.add(title); p.add(north, BorderLayout.NORTH); p.add(child); - child.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); + // child.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); child.setVisible(false); - title.setIcon(IconFactory.TREE_NODE_RETRACTED.get()); - title.addMouseListener(new MouseAdapter() { + var mouse = new MouseAdapter() { private boolean opened = false; @Override @@ -243,20 +259,23 @@ public void mouseClicked(MouseEvent e) { opened = !opened; child.setVisible(opened); if (opened) { - title.setIcon(IconFactory.TREE_NODE_EXPANDED.get()); + more.setIcon(IconFactory.TREE_NODE_EXPANDED.get()); } else { - title.setIcon(IconFactory.TREE_NODE_RETRACTED.get()); + more.setIcon(IconFactory.TREE_NODE_RETRACTED.get()); } } - }); + }; + + title.addMouseListener(mouse); + more.addMouseListener(mouse); + return p; } - private JRadioButton addRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { + private JRadioButton mkRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { Box b = new Box(BoxLayout.X_AXIS); JRadioButton button = new JRadioButton(c.choice); btnGroup.add(button); - // add(new JLabel(c.choice)); b.add(button); if (c.incomplete) { @@ -270,17 +289,60 @@ private JRadioButton addRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { b.add(lbl); } if (c.information != null) { - JLabel lbl = SettingsPanel.createHelpLabel(c.information); + JLabel lbl = SettingsPanel.createHelpTextLabel(c.information); b.add(lbl); } - pCenter.add(b, new CC().newline()); return button; } - private void addTitleRow(String cat) { - JLabel lbl = new JLabel(cat); + private JLabel createTitleRow(String cat, ChoiceEntry entry) { + JLabel lbl = new JLabel(createCatTitleText(cat, entry)); lbl.setFont(lbl.getFont().deriveFont(14f)); - pCenter.add(lbl, new CC().span().newline()); + + // we want to display a warning if the current choice differs from the loaded proof + checkForDifferingOptions(lbl, cat, entry); + + return lbl; + } + + private String createCatTitleText(String cat, ChoiceEntry entry) { + // if no proof is loaded, we do not want to display current settings + if (warnNoProof) { + return cat; + } + + // strip the leading "cat:" from "cat:value" + return cat + (entry == null ? "" + : " (set to '" + + entry.choice.substring(cat.length() + 1) + "')"); + } + + /** + * Checks if the current choice {@code entry} differs from the loaded proof and sets the icon to + * show a warning if necessary. + * + * @param lbl The label to set the icon on + * @param cat The category of the choice + * @param entry The current choice + */ + private void checkForDifferingOptions(JLabel lbl, String cat, ChoiceEntry entry) { + if (loadedProof != null) { + String choiceOfLoadedProof = + loadedProof.getSettings().getChoiceSettings().getDefaultChoices().get(cat); + boolean choiceDiffers = entry != null && !entry.choice.equals(choiceOfLoadedProof); + if (choiceDiffers) { + lbl.setIcon(IconFactory.WARNING_INCOMPLETE.get()); + lbl.setHorizontalTextPosition(JLabel.LEFT); + lbl.setIconTextGap(10); + lbl.setToolTipText( + "The current choice of this option differs from the loaded proof.
" + + "The loaded proof uses: " + choiceOfLoadedProof + ""); + + } else { + lbl.setIcon(null); + lbl.setToolTipText(null); + } + } } @Override @@ -290,7 +352,10 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { - warnNoProof = window.getMediator().getSelectedProof() == null; + loadedProof = window.getMediator().getSelectedProof(); + warnNoProof = loadedProof == null; + // this makes the header invisible + this.noProofLoadedHeader.setVisible(warnNoProof); setChoiceSettings(SettingsManager.getChoiceSettings(window)); return this; } @@ -459,17 +524,39 @@ public String toString() { } private class ChoiceSettingsSetter implements ActionListener { + private final JLabel title; private final String category; - private final String options; + private final ChoiceEntry choice; - public ChoiceSettingsSetter(String cat, String choice) { - category = cat; - options = choice; + public ChoiceSettingsSetter(JLabel title, String cat, ChoiceEntry choice) { + this.title = title; + this.category = cat; + this.choice = choice; } @Override public void actionPerformed(ActionEvent e) { - category2Choice.put(category, options); + category2Choice.put(category, choice.choice); + title.setText(createCatTitleText(category, choice)); + checkForDifferingOptions(title, category, choice); + title.repaint(); + } + } + + /** + * Converts a color to a non-UI color. + * + * There is a call to "SwingUtilities.updateComponentTreeUI(comp);" somewhere which resets all + * resources to original colors. To override, we have to convert the color to a non-UI color. + * + * @param color The color to convert. + * @return The non-UI color. + */ + private static Color toNonUIColor(Color color) { + if (color instanceof ColorUIResource) { + return new Color(color.getRGB(), true); + } else { + return color; } } }