From 21776197bae9f3611d264e1c16e2a64a6c645da7 Mon Sep 17 00:00:00 2001 From: Tobias Date: Fri, 23 Feb 2024 21:51:16 +0100 Subject: [PATCH 1/9] remove old taclet options dialog and make "proof not loaded" header invisible when proof is loaded --- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 3 ++- .../key/gui/actions/ShowActiveTactletOptionsAction.java | 3 ++- .../de/uka/ilkd/key/gui/actions/TacletOptionsAction.java | 2 ++ .../uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java | 3 ++- .../uka/ilkd/key/gui/settings/TacletOptionsSettings.java | 8 +++++++- 5 files changed, 15 insertions(+), 4 deletions(-) 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..4e0163af49f 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 @@ -1027,7 +1027,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(); 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..cc41b976c0f 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 @@ -55,7 +55,8 @@ private void showActivatedChoices() { final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns); activeOptions.setEditable(false); Object[] toDisplay = - { activeOptions, "These options can be changed in Options->Taclet Options" }; + { 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..faabacc3b5f 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,8 @@ 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 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/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 9ffa6aee27c..92fb727c5b3 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 @@ -43,6 +43,10 @@ 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 lblHead2; + + public TacletOptionsSettings() { setHeaderText(getDescription()); pCenter.setLayout(new MigLayout(new LC().fillX(), new AC().fill().grow().gap("3mm"))); @@ -174,7 +178,7 @@ public static ChoiceEntry createChoiceEntry(String choice) { protected void layoutHead() { if (warnNoProof) { - JLabel lblHead2 = new JLabel("No Proof loaded. Taclet options may not be parsed."); + this.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); @@ -292,6 +296,8 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { warnNoProof = window.getMediator().getSelectedProof() == null; + // this makes the wrong lblhead2 invisible + this.lblHead2.setVisible(warnNoProof); setChoiceSettings(SettingsManager.getChoiceSettings(window)); return this; } From b93592bc0c65c078221283875d00a2abba1c1bb9 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 7 Mar 2024 14:46:18 +0100 Subject: [PATCH 2/9] better error message for destroyed configuration files --- key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 6dde2f9ba5e..491a5d8ee7f 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()); } } From 84078cc991aa704e1fae0769e612199f940b6fea Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 8 Mar 2024 10:52:02 +0100 Subject: [PATCH 3/9] no tooltip help --- .../ilkd/key/gui/settings/SimpleSettingsPanel.java | 14 ++++++++++++++ .../key/gui/settings/TacletOptionsSettings.java | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) 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..550361a6465 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 92fb727c5b3..2809e656b64 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 @@ -275,7 +275,7 @@ 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()); From 76585a949b2824efa394339a3af8a20bccbf0a6f Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 6 Aug 2024 14:09:01 +0200 Subject: [PATCH 4/9] refreshing the active settings dialogue --- build.gradle | 2 + .../java/de/uka/ilkd/key/nparser/KeyAst.java | 2 +- .../java/de/uka/ilkd/key/gui/MainWindow.java | 2 +- .../key/gui/actions/SettingsTreeModel.java | 21 ++--- .../gui/actions/ShowActiveSettingsAction.java | 46 ++++++----- .../ShowActiveTactletOptionsAction.java | 80 +++++++++---------- .../key/gui/settings/SimpleSettingsPanel.java | 2 +- 7 files changed, 83 insertions(+), 72 deletions(-) diff --git a/build.gradle b/build.gradle index 0cace069f6c..f46b3c74247 100644 --- a/build.gradle +++ b/build.gradle @@ -321,6 +321,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 491a5d8ee7f..5668ecac47e 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 @@ -157,7 +157,7 @@ public Configuration asConfiguration() { return (Configuration) res.get(0); else throw new RuntimeException("Error in configuration. Source: " - + ctx.start.getTokenSource().getSourceName()); + + 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 4e0163af49f..5199961da28 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,7 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(this, selected)); - proof.add(new ShowActiveTactletOptionsAction(this, selected)); + proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); proof.add(showActiveSettingsAction); proof.add(new ShowProofStatistics(this, selected)); proof.add(new ShowKnownTypesAction(this, selected)); 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..1d51d6895e6 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) { @@ -52,7 +51,8 @@ private void generateTree() { // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - proofSettingsNode.add(generateTableNode("Taclets", choiceSettings)); + tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); + proofSettingsNode.add(tacletOptionsItem); Settings strategySettings = proofSettings.getStrategySettings(); proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); @@ -115,6 +115,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 +131,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 +146,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 +159,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..bbc3e484b77 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,6 +32,10 @@ public ShowActiveSettingsAction(MainWindow mainWindow) { @Override public void actionPerformed(ActionEvent e) { + showDialog(); + } + + private ViewSettingsDialog showDialog() { ProofSettings settings = (getMediator().getSelectedProof() == null) ? ProofSettings.DEFAULT_SETTINGS : getMediator().getSelectedProof().getSettings(); @@ -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 cc41b976c0f..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,61 +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->Show Settings->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/settings/SimpleSettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java index 550361a6465..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 @@ -194,7 +194,7 @@ public static JLabel createHelpTextLabel(String s) { if (s == null || s.isEmpty()) { s = ""; } - if(s.contains("\n")){ + if (s.contains("\n")) { s = s.substring(0, s.indexOf('\n')); } From 8304e292a086a5449e2c3648d52ad9711deb8bdb Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 6 Aug 2024 16:34:51 +0200 Subject: [PATCH 5/9] taclet option settings dialog refactored --- .../gui/settings/TacletOptionsSettings.java | 109 ++++++++++++------ 1 file changed, 73 insertions(+), 36 deletions(-) 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 2809e656b64..319a57df3ff 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,6 +15,7 @@ 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; @@ -192,7 +193,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) { @@ -200,47 +202,52 @@ protected void addCategory(String cat) { ChoiceEntry selectedChoice = findChoice(choices, category2Choice.get(cat)); String explanation = getExplanation(cat); - addTitleRow(cat); + JLabel title = createTitleRow(cat, selectedChoice); + JPanel selectPanel = new JPanel(new MigLayout(new LC().fillX(), new AC().fill().grow())); ButtonGroup btnGroup = new ButtonGroup(); for (ChoiceEntry c : choices) { - JRadioButton btn = addRadioButton(c, btnGroup); + JRadioButton btn = mkRadioButton(c, btnGroup); if (c.equals(selectedChoice)) { btn.setSelected(true); } - btn.addActionListener(new ChoiceSettingsSetter(cat, c.choice)); + btn.addActionListener(new ChoiceSettingsSetter(title, cat, c)); + selectPanel.add(btn, new CC().newline()); } - 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; } @NonNull - private JPanel createCollapsibleTitlePane(String titleText, JComponent child) { + 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 @@ -248,20 +255,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) { @@ -278,14 +288,20 @@ private JRadioButton addRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { 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()); + return lbl; + } + + private static String createCatTitleText(String cat, ChoiceEntry entry) { + // strip the leading "cat:" from "cat:value" + return cat + (entry == null ? "" + : " (set to '" + + entry.choice.substring(cat.length() + 1) + "')"); } @Override @@ -466,17 +482,38 @@ 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)); + 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; } } } From 514d2a1560cfafe4461c00e9a48cac0e886c3abc Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 13 Aug 2024 19:10:00 +0200 Subject: [PATCH 6/9] fix proof tab --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 3 +- .../key/gui/actions/SettingsTreeModel.java | 40 +++++++++++-------- .../gui/actions/ShowActiveSettingsAction.java | 2 +- .../key/gui/settings/SettingsManager.java | 2 +- 4 files changed, 28 insertions(+), 19 deletions(-) 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 5199961da28..08972da1a3b 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,8 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(this, selected)); - proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); + // 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)); 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 1d51d6895e6..8b31a9f0814 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 @@ -45,23 +45,29 @@ 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(); - 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)); + 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."); + "Proof-Independent Settings", "These are the proof independent settings."); root.add(independentSettingsNode); Settings generalSettings = independentSettings.getGeneralSettings(); @@ -75,7 +81,9 @@ 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)); } 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 bbc3e484b77..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 @@ -37,7 +37,7 @@ public void actionPerformed(ActionEvent e) { 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); 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)); } From 30bd5329407d8ce94a9465d43dfd0e4b2df29cf8 Mon Sep 17 00:00:00 2001 From: Tobias Date: Fri, 16 Aug 2024 16:46:59 +0200 Subject: [PATCH 7/9] disable taclet option settings when no proof is loaded --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 6 +-- .../gui/settings/TacletOptionsSettings.java | 41 +++++++++++-------- 2 files changed, 27 insertions(+), 20 deletions(-) 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 08972da1a3b..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,8 +1015,9 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(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)); + // 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)); @@ -1040,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/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 319a57df3ff..dc1f9881658 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 @@ -45,7 +45,7 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin private boolean warnNoProof = true; // to make the "No Proof Loaded" header invisible when a proof is loaded - private JLabel lblHead2; + private JLabel noProofLoadedHeader; public TacletOptionsSettings() { @@ -178,12 +178,10 @@ public static ChoiceEntry createChoiceEntry(String choice) { } protected void layoutHead() { - if (warnNoProof) { - this.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()); @@ -204,14 +202,17 @@ protected void addCategory(String cat) { JLabel title = createTitleRow(cat, selectedChoice); JPanel selectPanel = new JPanel(new MigLayout(new LC().fillX(), new AC().fill().grow())); - ButtonGroup btnGroup = new ButtonGroup(); - for (ChoiceEntry c : choices) { - JRadioButton btn = mkRadioButton(c, btnGroup); - if (c.equals(selectedChoice)) { - btn.setSelected(true); + + 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(title, cat, c)); - selectPanel.add(btn, new CC().newline()); } selectPanel.add(mkExplanation(explanation), new CC().pad(0, 20, 0, 0).newline()); @@ -297,7 +298,13 @@ private JLabel createTitleRow(String cat, ChoiceEntry entry) { return lbl; } - private static String createCatTitleText(String cat, ChoiceEntry entry) { + private String createCatTitleText(String cat, ChoiceEntry entry) { + // TODO: magic to say what is set in the current proof + // 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 '" + @@ -312,8 +319,8 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { warnNoProof = window.getMediator().getSelectedProof() == null; - // this makes the wrong lblhead2 invisible - this.lblHead2.setVisible(warnNoProof); + // this makes the header invisible + this.noProofLoadedHeader.setVisible(warnNoProof); setChoiceSettings(SettingsManager.getChoiceSettings(window)); return this; } From 4b682347726456e1aecc2cb218a5e42498e4b842 Mon Sep 17 00:00:00 2001 From: Tobias Date: Sat, 17 Aug 2024 01:46:14 +0200 Subject: [PATCH 8/9] show a warning when the taclet options differ from the currently loaded proof --- .../key/gui/actions/SettingsTreeModel.java | 10 +++-- .../ilkd/key/gui/settings/SettingsDialog.java | 1 + .../gui/settings/TacletOptionsSettings.java | 40 ++++++++++++++++++- 3 files changed, 45 insertions(+), 6 deletions(-) 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 8b31a9f0814..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 @@ -47,11 +47,12 @@ private void generateTree() { if (proofSettings == null) { OptionContentNode proofSettingsNode = - generateOptionContentNode("Proof Settings", "There is currently no proof loaded!"); + generateOptionContentNode("Proof Settings", "There is currently no proof loaded!"); root.add(proofSettingsNode); } else { OptionContentNode proofSettingsNode = - generateOptionContentNode("Proof Settings", "These are the proof dependent settings."); + generateOptionContentNode("Proof Settings", + "These are the proof dependent settings."); root.add(proofSettingsNode); // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); @@ -67,7 +68,7 @@ private void generateTree() { } OptionContentNode independentSettingsNode = generateOptionContentNode( - "Proof-Independent Settings", "These are the proof independent settings."); + "Proof-Independent Settings", "These are the proof independent settings."); root.add(independentSettingsNode); Settings generalSettings = independentSettings.getGeneralSettings(); @@ -81,7 +82,8 @@ private void generateTree() { Settings viewSettings = independentSettings.getViewSettings(); independentSettingsNode.add(generateTableNode("View", viewSettings)); Settings termLabelSettings = independentSettings.getTermLabelSettings(); - // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the previous line, + // 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)); } 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/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index dc1f9881658..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 @@ -19,6 +19,7 @@ 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; @@ -47,6 +48,8 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin // to make the "No Proof Loaded" header invisible when a proof is loaded private JLabel noProofLoadedHeader; + private Proof loadedProof = null; + public TacletOptionsSettings() { setHeaderText(getDescription()); @@ -295,11 +298,14 @@ private JRadioButton mkRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { private JLabel createTitleRow(String cat, ChoiceEntry entry) { JLabel lbl = new JLabel(createCatTitleText(cat, entry)); lbl.setFont(lbl.getFont().deriveFont(14f)); + + // 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) { - // TODO: magic to say what is set in the current proof // if no proof is loaded, we do not want to display current settings if (warnNoProof) { return cat; @@ -311,6 +317,34 @@ private String createCatTitleText(String cat, ChoiceEntry entry) { 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 public String getDescription() { return "Taclet Options"; @@ -318,7 +352,8 @@ 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)); @@ -503,6 +538,7 @@ public ChoiceSettingsSetter(JLabel title, String cat, ChoiceEntry choice) { public void actionPerformed(ActionEvent e) { category2Choice.put(category, choice.choice); title.setText(createCatTitleText(category, choice)); + checkForDifferingOptions(title, category, choice); title.repaint(); } } From 8f4ee86e046f23dfee5bf8e25b21ea1b4f268675 Mon Sep 17 00:00:00 2001 From: Tobias Date: Sun, 18 Aug 2024 14:35:06 +0200 Subject: [PATCH 9/9] mark TacletOptionsAction as deprecated --- .../java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java | 1 + 1 file changed, 1 insertion(+) 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 faabacc3b5f..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 @@ -13,6 +13,7 @@ // This class is not used anymore as taclet options should be set through the general settings // dialog +@Deprecated public class TacletOptionsAction extends MainWindowAction { /**