001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.gui.se.pane;
017
018 import java.awt.BorderLayout;
019 import java.awt.Dimension;
020 import java.awt.event.ActionEvent;
021 import java.awt.event.ActionListener;
022 import java.io.IOException;
023 import java.util.ArrayList;
024 import java.util.Iterator;
025 import java.util.List;
026
027 import javax.swing.BorderFactory;
028 import javax.swing.ButtonGroup;
029 import javax.swing.JButton;
030 import javax.swing.JCheckBox;
031 import javax.swing.JComponent;
032 import javax.swing.JDialog;
033 import javax.swing.JFrame;
034 import javax.swing.JOptionPane;
035 import javax.swing.JPanel;
036 import javax.swing.JRadioButton;
037 import javax.swing.JTabbedPane;
038 import javax.swing.JTextArea;
039 import javax.swing.JTextField;
040 import javax.swing.border.CompoundBorder;
041 import javax.swing.border.EmptyBorder;
042
043 import org.qedeq.base.io.Parameters;
044 import org.qedeq.base.trace.Trace;
045 import org.qedeq.gui.se.util.GuiHelper;
046 import org.qedeq.kernel.bo.logic.model.FourDynamicModel;
047 import org.qedeq.kernel.bo.logic.model.SixDynamicModel;
048 import org.qedeq.kernel.bo.logic.model.ThreeDynamicModel;
049 import org.qedeq.kernel.bo.logic.model.UnaryDynamicModel;
050 import org.qedeq.kernel.bo.module.PluginBo;
051 import org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPlugin;
052 import org.qedeq.kernel.bo.service.latex.Qedeq2LatexPlugin;
053 import org.qedeq.kernel.bo.service.logic.SimpleProofFinderPlugin;
054 import org.qedeq.kernel.bo.service.unicode.Qedeq2UnicodeTextPlugin;
055 import org.qedeq.kernel.bo.service.unicode.Qedeq2Utf8Plugin;
056 import org.qedeq.kernel.se.common.Plugin;
057
058 import com.jgoodies.forms.builder.ButtonBarBuilder;
059 import com.jgoodies.forms.builder.DefaultFormBuilder;
060 import com.jgoodies.forms.layout.FormLayout;
061
062 /**
063 * Configures the plugin parameters.
064 *
065 * @author Michael Meyling
066 */
067
068 public class PluginPreferencesDialog extends JDialog {
069
070 /** This class. */
071 private static final Class CLASS = PluginPreferencesDialog.class;
072
073 /** Text field for default language of QEDEQ to UTF-8 show plugin. */
074 private JTextField qedeq2Utf8ShowLanguageTF;
075
076 /** Checkbox for info parameter of QEDEQ to UTF-8 show plugin. */
077 private JCheckBox qedeq2Utf8ShowInfoCB;
078
079 /** Text field for maximum column of QEDEQ to UTF-8 show plugin. */
080 private JTextField qedeq2Utf8ShowMaximumColumnTF;
081
082 /** Checkbox for info parameter of QEDEQ to LaTeX plugin. */
083 private JCheckBox qedeq2LatexInfoCB;
084
085 /** Checkbox for brief parameter of QEDEQ to LaTeX plugin. */
086 private JCheckBox qedeq2LatexBriefCB;
087
088 /** Checkbox for info parameter of QEDEQ to UTF-8 plugin. */
089 private JCheckBox qedeq2Utf8InfoCB;
090
091 /** Text field for maximum column of QEDEQ to UTF-8 plugin. */
092 private JTextField qedeq2Utf8MaximumColumnTF;
093
094 /** Checkbox for brief parameter of QEDEQ to UTF-8 plugin. */
095 private JCheckBox qedeq2Utf8BriefCB;
096
097 /** Plugin for converting QEDEQ modules into LaTeX. */
098 private final Qedeq2LatexPlugin qedeq2latex;
099
100 /** Plugin for converting QEDEQ modules into UTF-8 text. */
101 private final Qedeq2Utf8Plugin qedeq2utf8;
102
103 /** Plugin for showing QEDEQ modules as UTF-8 text. */
104 private final Qedeq2UnicodeTextPlugin qedeq2utf8Show;
105
106 /** Plugin for finding simple propositional calculus proofs. */
107 private final SimpleProofFinderPlugin proofFinder;
108
109 // LATER 20101222 m31: remove if not used for a long time
110 // /** Plugin for checking formulas with the help of a static model. */
111 // private HeuristicCheckerPlugin heuristicChecker;
112
113 // /** Class string for static model. */
114 // private String heuristicCheckerModel = "";
115
116 /** Plugin for checking formulas with the help of a dynamically calculated static model. */
117 private DynamicHeuristicCheckerPlugin dynamicHeuristicChecker;
118
119 /** Class string for dynamic static model. */
120 private String dynamicHeuristicCheckerModel = "";
121
122 /** Text field for maximum proof length of proof finder plugin. */
123 private JTextField proofFinderMaximumProofLengthTF;
124
125 /** Text field for number of additional propositional variables for substitution. */
126 private JTextField proofFinderExtraVarsTF;
127
128 /** Text field for number for order of substitution. */
129 private JTextField proofFinderPropositionVariableOrderTF;
130
131 /** Text field for number for weight of substitution. */
132 private JTextField proofFinderPropositionVariableWeightTF;
133
134 /** Text field for number for order of substitution. */
135 private JTextField proofFinderPartFormulaOrderTF;
136
137 /** Text field for number for weight of substitution. */
138 private JTextField proofFinderPartFormulaWeightTF;
139
140 /** Text field for number for order of substitution. */
141 private JTextField proofFinderDisjunctionOrderTF;
142
143 /** Text field for number for weight of substitution. */
144 private JTextField proofFinderDisjunctionWeightTF;
145
146 /** Text field for number for order of substitution. */
147 private JTextField proofFinderImplicationOrderTF;
148
149 /** Text field for number for weight of substitution. */
150 private JTextField proofFinderImplicationWeightTF;
151
152 /** Text field for number for order of substitution. */
153 private JTextField proofFinderNegationOrderTF;
154
155 /** Text field for number for weight of substitution. */
156 private JTextField proofFinderNegationWeightTF;
157
158 /** Text field for number for order of substitution. */
159 private JTextField proofFinderConjunctionOrderTF;
160
161 /** Text field for number for weight of substitution. */
162 private JTextField proofFinderConjunctionWeightTF;
163
164 /** Text field for number for order of substitution. */
165 private JTextField proofFinderEquivalenceOrderTF;
166
167 /** Text field for number for weight of substitution. */
168 private JTextField proofFinderEquivalenceWeightTF;
169
170 /** Text field for number of new proof lines before a new log entry. */
171 private JTextField proofFinderLogFrequenceTF;
172
173 /** Text field for sequence of formula numbers we want to skip. */
174 private JTextField proofFinderSkipFormulasTF;
175
176 /** Here are the tabs. */
177 private JTabbedPane tabbedPane;
178
179 /** Here are the creators of class {@link PluginGuiPreferencesCreator}. */
180 private List creators;
181
182 /**
183 * Creates new Panel.
184 *
185 * @param parent Parent frame.
186 */
187 public PluginPreferencesDialog(final JFrame parent) {
188 super(parent, "Plugin Preferences");
189 final String method = "Constructor";
190 Trace.begin(CLASS, this, method);
191 try {
192 qedeq2latex = new Qedeq2LatexPlugin();
193 qedeq2utf8 = new Qedeq2Utf8Plugin();
194 qedeq2utf8Show = new Qedeq2UnicodeTextPlugin();
195 // LATER 20101222 m31: remove if not used for a long time
196 // heuristicChecker = new HeuristicCheckerPlugin();
197 dynamicHeuristicChecker = new DynamicHeuristicCheckerPlugin();
198 proofFinder = new SimpleProofFinderPlugin();
199 creators = new ArrayList();
200 setModal(true);
201 setDefaultCloseOperation(DISPOSE_ON_CLOSE);
202 setupView();
203 updateView();
204 } catch (RuntimeException e) {
205 Trace.fatal(CLASS, this, "Initalization of PreferencesDialog failed.", method, e);
206 throw e;
207 } finally {
208 Trace.end(CLASS, this, method);
209 }
210 }
211
212 /**
213 * Assembles the GUI components of the panel.
214 */
215 public final void setupView() {
216 final JPanel content = new JPanel(new BorderLayout());
217 getContentPane().add(content);
218
219 tabbedPane = new JTabbedPane();
220 tabbedPane.setOpaque(false);
221 creators.add(qedeq2Utf8ShowConfig(qedeq2utf8Show));
222 creators.add(qedeq2LatexConfig(qedeq2latex));
223 creators.add(qedeq2Utf8Config(qedeq2utf8));
224 // creators.add(heuristicCheckerConfig(heuristicChecker));
225 creators.add(dynamicHeuristicCheckerConfig(dynamicHeuristicChecker));
226 creators.add(proofFinderConfig(proofFinder));
227 final Iterator iter = creators.iterator();
228 while (iter.hasNext()) {
229 PluginGuiPreferencesCreator creator = (PluginGuiPreferencesCreator) iter.next();
230 tabbedPane.addTab(creator.getName(), creator.create(QedeqGuiConfig.getInstance()
231 .getPluginEntries(creator.getPlugin())));
232 }
233
234 // tabbedPane.setBorder(GuiHelper.getEmptyBorder());
235 tabbedPane.setBorder(new CompoundBorder(new EmptyBorder(0, 10, 10, 10),
236 tabbedPane.getBorder()));
237 content.add(tabbedPane, BorderLayout.CENTER);
238
239 content.add(GuiHelper.addSpaceAndAlignRight(buildButtonPanel()), BorderLayout.SOUTH);
240
241 // let the container calculate the ideal size
242 this.pack();
243
244 final Dimension screenSize = java.awt.Toolkit.getDefaultToolkit().getScreenSize();
245 int width = getWidth();
246 if (2 * width < screenSize.width) {
247 width = 2 * width;
248 }
249 setBounds((screenSize.width - getWidth()) / 2, (screenSize.height - getHeight()) / 2,
250 width, getHeight());
251 }
252
253 /**
254 * Assembles settings for {@link Qedeq2LatexPlugin}.
255 *
256 * @param plugin The transformation plugin.
257 * @return Created panel.
258 */
259 private PluginGuiPreferencesCreator qedeq2LatexConfig(final PluginBo plugin) {
260 return new PluginGuiPreferencesCreator(plugin) {
261 JComponent create(final Parameters parameters) {
262 FormLayout layout = new FormLayout(
263 "left:pref, 5dlu, fill:pref:grow"); // columns
264
265 DefaultFormBuilder builder = new DefaultFormBuilder(layout);
266 builder.setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
267 builder.getPanel().setOpaque(false);
268
269 qedeq2LatexInfoCB = new JCheckBox(" Also write reference labels (makes it easier for authors)",
270 parameters.getBoolean("info"));
271 builder.append(qedeq2LatexInfoCB);
272
273 builder.nextLine();
274 qedeq2LatexBriefCB = new JCheckBox(" Leave out main text entries. Creates a very brief document.",
275 parameters.getBoolean("brief"));
276 builder.append(qedeq2LatexBriefCB);
277
278 return GuiHelper.addSpaceAndTitle(builder.getPanel(), plugin.getPluginDescription());
279 }
280 };
281 }
282
283 /**
284 * Assembles settings for {@link Qedeq2Utf8Plugin}.
285 *
286 * @param plugin The transformation plugin.
287 * @return Created panel.
288 */
289 private PluginGuiPreferencesCreator qedeq2Utf8Config(final PluginBo plugin) {
290 return new PluginGuiPreferencesCreator(plugin) {
291 JComponent create(final Parameters parameters) {
292 FormLayout layout = new FormLayout(
293 "left:pref, 5dlu, fill:50dlu, fill:pref:grow"); // columns
294
295 DefaultFormBuilder builder = new DefaultFormBuilder(layout);
296 builder.setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
297 builder.getPanel().setOpaque(false);
298
299 qedeq2Utf8InfoCB = new JCheckBox(" Also write reference labels (makes it easier for authors)",
300 parameters.getBoolean("info"));
301 builder.append(qedeq2Utf8InfoCB, 4);
302
303 builder.nextLine();
304 builder.append("Maximum row length");
305 qedeq2Utf8MaximumColumnTF = new JTextField(parameters.getString(
306 "maximumColumn"));
307 qedeq2Utf8MaximumColumnTF.setToolTipText("After this character number the line is broken."
308 + "0 means no break at all.");
309 builder.append(qedeq2Utf8MaximumColumnTF);
310
311 builder.nextLine();
312 qedeq2Utf8BriefCB = new JCheckBox(" Leave out main text entries. Creates a very brief document.",
313 parameters.getBoolean("brief"));
314 builder.append(qedeq2Utf8BriefCB);
315
316 return GuiHelper.addSpaceAndTitle(builder.getPanel(), plugin.getPluginDescription());
317 }
318 };
319 }
320
321 /**
322 * Assembles settings for {@link Qedeq2Utf8TextPlugin}.
323 *
324 * @param plugin The transformation plugin.
325 * @return Created panel.
326 */
327 private PluginGuiPreferencesCreator qedeq2Utf8ShowConfig(final PluginBo plugin) {
328 return new PluginGuiPreferencesCreator(plugin) {
329 JComponent create(final Parameters parameters) {
330 FormLayout layout = new FormLayout(
331 "left:pref, 5dlu, fill:50dlu, fill:pref:grow"); // columns
332
333 DefaultFormBuilder builder = new DefaultFormBuilder(layout);
334 builder.setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
335 builder.getPanel().setOpaque(false);
336
337 builder.append("Default language");
338 qedeq2Utf8ShowLanguageTF = new JTextField(parameters.getString(
339 "language"));
340 qedeq2Utf8ShowLanguageTF.setToolTipText("Default language for showing module contents.");
341 builder.append(qedeq2Utf8ShowLanguageTF);
342
343 builder.nextLine();
344 qedeq2Utf8ShowInfoCB = new JCheckBox(" Also write reference labels (makes it easier for authors)",
345 parameters.getBoolean("info"));
346 builder.append(qedeq2Utf8ShowInfoCB, 4);
347
348 builder.nextLine();
349 builder.append("Maximum row length");
350 qedeq2Utf8ShowMaximumColumnTF = new JTextField(parameters.getString(
351 "maximumColumn"));
352 qedeq2Utf8ShowMaximumColumnTF.setToolTipText("After this character number the line is broken."
353 + "0 means no break at all.");
354 builder.append(qedeq2Utf8ShowMaximumColumnTF);
355
356 return GuiHelper.addSpaceAndTitle(builder.getPanel(), plugin.getPluginDescription());
357 }
358 };
359 }
360
361 // LATER 20101222 m31: remove if not used for a long time
362 // /**
363 // * Assembles settings for {@link HeuristicCheckerPlugin}.
364 // *
365 // * @param plugin The transformation plugin.
366 // * @return Created panel.
367 // */
368 // private PluginGuiPreferencesCreator heuristicCheckerConfig(final PluginBo plugin) {
369 // return new PluginGuiPreferencesCreator(plugin) {
370 // JComponent create(final Parameters parameters) {
371 // FormLayout layout = new FormLayout(
372 // "left:pref, 5dlu, fill:pref:grow", // columns
373 // "top:pref:grow, top:pref:grow, top:pref:grow"); // rows
374 //
375 // DefaultFormBuilder builder = new DefaultFormBuilder(layout);
376 // builder.setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
377 // builder.getPanel().setOpaque(false);
378 //
379 // final ThreeModel three = new ThreeModel();
380 // final UnaryModel unary = new UnaryModel();
381 // heuristicCheckerModel = QedeqGuiConfig.getInstance()
382 // .getPluginKeyValue(plugin, "model", three.getClass().getName());
383 // final ActionListener modelSelectionListener = new ActionListener() {
384 // public void actionPerformed(final ActionEvent e) {
385 // heuristicCheckerModel = e.getActionCommand();
386 // }
387 // };
388 //
389 // final ButtonGroup heuristicCheckerModelBG = new ButtonGroup();
390 //
391 // final JRadioButton heuristicCheckerUnaryModelRB = new JRadioButton("Unary Model");
392 // if (heuristicCheckerModel.equals(unary.getClass().getName())) {
393 // heuristicCheckerUnaryModelRB.setSelected(true);
394 // }
395 // heuristicCheckerUnaryModelRB.setActionCommand(unary.getClass().getName());
396 // heuristicCheckerUnaryModelRB.addActionListener(modelSelectionListener);
397 // heuristicCheckerModelBG.add(heuristicCheckerUnaryModelRB);
398 //
399 // final JRadioButton heuristicCheckerThreeModelRB = new JRadioButton("Three Model");
400 // if (heuristicCheckerModel.equals(three.getClass().getName())) {
401 // heuristicCheckerThreeModelRB.setSelected(true);
402 // }
403 // heuristicCheckerThreeModelRB.setActionCommand(three.getClass().getName());
404 // heuristicCheckerThreeModelRB.addActionListener(modelSelectionListener);
405 // heuristicCheckerModelBG.add(heuristicCheckerThreeModelRB);
406 //
407 // builder.append(heuristicCheckerUnaryModelRB);
408 // JTextArea description = new JTextArea(unary.getDescription());
409 // description.setEditable(false);
410 // description.setLineWrap(true);
411 // description.setWrapStyleWord(true);
412 // builder.append(description);
413 //
414 // builder.append(heuristicCheckerThreeModelRB);
415 // description = new JTextArea(three.getDescription());
416 // description.setEditable(false);
417 // description.setLineWrap(true);
418 // description.setWrapStyleWord(true);
419 // builder.append(description);
420 //
421 // return GuiHelper.addSpaceAndTitle(builder.getPanel(), plugin.getPluginDescription());
422 // }
423 // };
424 // }
425
426 /**
427 * Assembles settings for {@link DynamicHeuristicCheckerPlugin}.
428 *
429 * @param plugin The transformation plugin.
430 * @return Created panel.
431 */
432 private PluginGuiPreferencesCreator dynamicHeuristicCheckerConfig(final PluginBo plugin) {
433 return new PluginGuiPreferencesCreator(plugin) {
434 JComponent create(final Parameters parameters) {
435 FormLayout layout = new FormLayout(
436 "left:pref, 5dlu, fill:pref:grow", // columns
437 "top:pref:grow, top:pref:grow, top:pref:grow"); // rows
438
439 DefaultFormBuilder builder = new DefaultFormBuilder(layout);
440 builder.setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
441 builder.getPanel().setOpaque(false);
442
443 final ThreeDynamicModel modelThree = new ThreeDynamicModel();
444 final FourDynamicModel modelFour = new FourDynamicModel();
445 final SixDynamicModel modelSix = new SixDynamicModel();
446
447 final ButtonGroup dynamicHeuristicCheckerModelBG = new ButtonGroup();
448
449 final UnaryDynamicModel modelOne = new UnaryDynamicModel();
450 dynamicHeuristicCheckerModel = parameters.getString(
451 "model");
452 final ActionListener modelSelectionListener = new ActionListener() {
453 public void actionPerformed(final ActionEvent e) {
454 dynamicHeuristicCheckerModel = e.getActionCommand();
455 }
456 };
457
458 // model with one element
459 {
460 final JRadioButton dynamicHeuristicCheckerOneModelRB = new JRadioButton("One");
461 if (dynamicHeuristicCheckerModel.equals(modelOne.getClass().getName())) {
462 dynamicHeuristicCheckerOneModelRB.setSelected(true);
463 }
464 dynamicHeuristicCheckerOneModelRB.setActionCommand(modelOne.getClass().getName());
465 dynamicHeuristicCheckerOneModelRB.addActionListener(modelSelectionListener);
466 dynamicHeuristicCheckerModelBG.add(dynamicHeuristicCheckerOneModelRB);
467 builder.append(dynamicHeuristicCheckerOneModelRB);
468 builder.append(getDescription(modelOne.getDescription()));
469 }
470
471 // model with three elements
472 {
473 final JRadioButton dynamicHeuristicCheckerThreeModelRB = new JRadioButton("Three");
474 if (dynamicHeuristicCheckerModel.equals(modelThree.getClass().getName())) {
475 dynamicHeuristicCheckerThreeModelRB.setSelected(true);
476 }
477 dynamicHeuristicCheckerThreeModelRB.setActionCommand(modelThree.getClass().getName());
478 dynamicHeuristicCheckerThreeModelRB.addActionListener(modelSelectionListener);
479 dynamicHeuristicCheckerModelBG.add(dynamicHeuristicCheckerThreeModelRB);
480 builder.append(dynamicHeuristicCheckerThreeModelRB);
481 builder.append(getDescription(modelThree.getDescription()));
482 }
483
484 // model with four elements
485 {
486 final JRadioButton dynamicHeuristicCheckerFourModelRB = new JRadioButton("Four");
487 if (dynamicHeuristicCheckerModel.equals(modelFour.getClass().getName())) {
488 dynamicHeuristicCheckerFourModelRB.setSelected(true);
489 }
490 dynamicHeuristicCheckerFourModelRB.setActionCommand(modelFour.getClass().getName());
491 dynamicHeuristicCheckerFourModelRB.addActionListener(modelSelectionListener);
492 dynamicHeuristicCheckerModelBG.add(dynamicHeuristicCheckerFourModelRB);
493 builder.append(dynamicHeuristicCheckerFourModelRB);
494 builder.append(getDescription(modelFour.getDescription()));
495 }
496
497 // model with five elements
498 {
499 final JRadioButton dynamicHeuristicCheckerSixModelRB = new JRadioButton("Six");
500 if (dynamicHeuristicCheckerModel.equals(modelSix.getClass().getName())) {
501 dynamicHeuristicCheckerSixModelRB.setSelected(true);
502 }
503 dynamicHeuristicCheckerSixModelRB.setActionCommand(modelSix.getClass().getName());
504 dynamicHeuristicCheckerSixModelRB.addActionListener(modelSelectionListener);
505 dynamicHeuristicCheckerModelBG.add(dynamicHeuristicCheckerSixModelRB);
506 builder.append(dynamicHeuristicCheckerSixModelRB);
507 builder.append(getDescription(modelSix.getDescription()));
508 }
509
510 return GuiHelper.addSpaceAndTitle(builder.getPanel(), plugin.getPluginDescription());
511 }
512 };
513 }
514
515 /**
516 * Assembles settings for {@link ProofFinderPlugin}.
517 *
518 * @param plugin The transformation plugin.
519 * @return Created panel.
520 */
521 private PluginGuiPreferencesCreator proofFinderConfig(final PluginBo plugin) {
522 return new PluginGuiPreferencesCreator(plugin) {
523 JComponent create(final Parameters parameters) {
524 FormLayout layout = new FormLayout(
525 "left:pref, 5dlu, fill:50dlu, 5dlu, fill:50dlu, fill:pref:grow"); // columns
526
527 DefaultFormBuilder builder = new DefaultFormBuilder(layout);
528 builder.setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
529 builder.getPanel().setOpaque(false);
530
531 builder.append("Maximum proof lines");
532 proofFinderMaximumProofLengthTF = new JTextField(parameters.getString(
533 "maximumProofLines"));
534 proofFinderMaximumProofLengthTF.setToolTipText("After this proof line number we abandom."
535 + " the search. This is not the maximum proof line length of the final proof but the"
536 + " but the maximum number of all generated proof lines.");
537 builder.append(proofFinderMaximumProofLengthTF);
538 builder.nextLine();
539
540 builder.append("Log frequence");
541 proofFinderLogFrequenceTF = new JTextField(parameters.getString(
542 "logFrequence"));
543 proofFinderLogFrequenceTF.setToolTipText("After this number of new proof lines we"
544 + " create a logging output.");
545 builder.append(proofFinderLogFrequenceTF);
546 builder.nextLine();
547
548 builder.append("Skip formulas");
549 proofFinderSkipFormulasTF = new JTextField(parameters.getString(
550 "skipFormulas"));
551 proofFinderSkipFormulasTF.setToolTipText("Skip these list of formula numbers (see log output)."
552 + " This a comma separated list of numbers.");
553 builder.append(proofFinderSkipFormulasTF);
554 builder.nextLine();
555
556 proofFinderExtraVarsTF = new JTextField(parameters.getString(
557 "extraVars"));
558 builder.append("Extra proposition variables");
559 builder.append(proofFinderExtraVarsTF);
560 proofFinderExtraVarsTF.setToolTipText("We use these number of extra proposition variables"
561 + " beside the ones we have in our initial formulas and the goal formula.");
562 builder.nextLine();
563
564 builder.appendSeparator();
565 builder.append("Operator");
566 builder.append("Order");
567 builder.append("Weight");
568 builder.nextLine();
569
570 builder.append("Proposition variable");
571 proofFinderPropositionVariableOrderTF = new JTextField(parameters.getString(
572 "propositionVariableOrder"));
573 builder.append(proofFinderPropositionVariableOrderTF);
574 proofFinderPropositionVariableWeightTF = new JTextField(parameters.getString(
575 "propositionVariableWeight"));
576 builder.append(proofFinderPropositionVariableWeightTF);
577 builder.nextLine();
578
579 builder.append("Part formula");
580 proofFinderPartFormulaOrderTF = new JTextField(parameters.getString(
581 "partFormulaOrder"));
582 builder.append(proofFinderPartFormulaOrderTF);
583 proofFinderPartFormulaWeightTF = new JTextField(parameters.getString(
584 "partFormulaWeight"));
585 builder.append(proofFinderPartFormulaWeightTF);
586 builder.nextLine();
587
588 builder.append("Disjunction");
589 proofFinderDisjunctionOrderTF = new JTextField(parameters.getString(
590 "disjunctionOrder"));
591 builder.append(proofFinderDisjunctionOrderTF);
592 proofFinderDisjunctionWeightTF = new JTextField(parameters.getString(
593 "disjunctionWeight"));
594 builder.append(proofFinderDisjunctionWeightTF);
595 builder.nextLine();
596
597 builder.append("Implication");
598 proofFinderImplicationOrderTF = new JTextField(parameters.getString(
599 "implicationOrder"));
600 builder.append(proofFinderImplicationOrderTF);
601 proofFinderImplicationWeightTF = new JTextField(parameters.getString(
602 "implicationWeight"));
603 builder.append(proofFinderImplicationWeightTF);
604 builder.nextLine();
605
606 builder.append("Negation");
607 proofFinderNegationOrderTF = new JTextField(parameters.getString(
608 "negationOrder"));
609 builder.append(proofFinderNegationOrderTF);
610 proofFinderNegationWeightTF = new JTextField(parameters.getString(
611 "negationWeight"));
612 builder.append(proofFinderNegationWeightTF);
613 builder.nextLine();
614
615 builder.append("Conjunction");
616 proofFinderConjunctionOrderTF = new JTextField(parameters.getString(
617 "conjunctionOrder"));
618 builder.append(proofFinderConjunctionOrderTF);
619 proofFinderConjunctionWeightTF = new JTextField(parameters.getString(
620 "conjunctionWeight"));
621 builder.append(proofFinderConjunctionWeightTF);
622 builder.nextLine();
623
624 builder.append("Equivalence");
625 proofFinderEquivalenceOrderTF = new JTextField(parameters.getString(
626 "equivalenceOrder"));
627 builder.append(proofFinderEquivalenceOrderTF);
628 proofFinderEquivalenceWeightTF = new JTextField(parameters.getString(
629 "equivalenceWeight"));
630 builder.append(proofFinderEquivalenceWeightTF);
631 builder.nextLine();
632
633 return GuiHelper.addSpaceAndTitle(builder.getPanel(), plugin.getPluginDescription());
634 }
635 };
636 }
637
638 private JTextArea getDescription(final String text) {
639 JTextArea description = new JTextArea(text);
640 description.setEditable(false);
641 description.setLineWrap(true);
642 description.setWrapStyleWord(true);
643 return description;
644 }
645
646 /**
647 * Create button panel with "OK" and "Cancel".
648 *
649 * @return Button panel.
650 */
651 private JPanel buildButtonPanel() {
652 ButtonBarBuilder bbuilder = ButtonBarBuilder.createLeftToRightBuilder();
653
654 JButton def = new JButton("Default");
655 def.addActionListener(new ActionListener() {
656 public void actionPerformed(final ActionEvent actionEvent) {
657 final int i = tabbedPane.getSelectedIndex();
658 PluginGuiPreferencesCreator creator = (PluginGuiPreferencesCreator) creators.get(i);
659 tabbedPane.setComponentAt(i, creator.createDefault());
660 }
661 });
662 def.setToolTipText("Reset to default values for plugin currently displayed.");
663
664 JButton ok = new JButton("OK");
665 ok.addActionListener(new ActionListener() {
666 public void actionPerformed(final ActionEvent actionEvent) {
667 PluginPreferencesDialog.this.save();
668 PluginPreferencesDialog.this.dispose();
669 }
670 });
671
672 JButton cancel = new JButton("Cancel");
673 cancel.addActionListener(new ActionListener() {
674 public void actionPerformed(final ActionEvent actionEvent) {
675 PluginPreferencesDialog.this.dispose();
676 }
677 });
678 bbuilder.addGriddedButtons(new JButton[]{def});
679 bbuilder.addUnrelatedGap();
680 bbuilder.addUnrelatedGap();
681 bbuilder.addGriddedButtons(new JButton[]{cancel, ok});
682
683 final JPanel buttons = bbuilder.getPanel();
684 return buttons;
685 }
686
687 /**
688 * Update from model.
689 */
690 public void updateView() {
691 invalidate();
692 repaint();
693 }
694
695 void save() {
696 try {
697 {
698 final Plugin plugin = qedeq2utf8Show;
699 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "language",
700 qedeq2Utf8ShowLanguageTF.getText());
701 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "info", qedeq2Utf8ShowInfoCB.isSelected());
702 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "maximumColumn",
703 qedeq2Utf8ShowMaximumColumnTF.getText());
704 }
705 {
706 final Plugin plugin = qedeq2latex;
707 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "info", qedeq2LatexInfoCB.isSelected());
708 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "brief", qedeq2LatexBriefCB.isSelected());
709 }
710 {
711 final Plugin plugin = qedeq2utf8;
712 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "info", qedeq2Utf8InfoCB.isSelected());
713 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "maximumColumn",
714 qedeq2Utf8MaximumColumnTF.getText());
715 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "brief", qedeq2Utf8BriefCB.isSelected());
716 }
717 // LATER 20101222 m31: remove if not used for a long time
718 // {
719 // final Plugin plugin = heuristicChecker;
720 // QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "model", heuristicCheckerModel);
721 // }
722 {
723 final Plugin plugin = dynamicHeuristicChecker;
724 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "model", dynamicHeuristicCheckerModel);
725 }
726 {
727 final Plugin plugin = proofFinder;
728 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "maximumProofLines",
729 proofFinderMaximumProofLengthTF.getText());
730 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "logFrequence",
731 proofFinderLogFrequenceTF.getText());
732 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "skipFormulas",
733 proofFinderSkipFormulasTF.getText());
734 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "extraVars",
735 proofFinderExtraVarsTF.getText());
736 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "propositionVariableOrder",
737 proofFinderPropositionVariableOrderTF.getText());
738 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "propositionVariableWeight",
739 proofFinderPropositionVariableWeightTF.getText());
740 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "partFormulaOrder",
741 proofFinderPartFormulaOrderTF.getText());
742 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "partFormulaWeight",
743 proofFinderPartFormulaWeightTF.getText());
744 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "disjunctionOrder",
745 proofFinderDisjunctionOrderTF.getText());
746 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "disjunctionWeight",
747 proofFinderDisjunctionWeightTF.getText());
748 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "implicationOrder",
749 proofFinderImplicationOrderTF.getText());
750 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "implicationWeight",
751 proofFinderImplicationWeightTF.getText());
752 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "negationOrder",
753 proofFinderNegationOrderTF.getText());
754 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "negationWeight",
755 proofFinderNegationWeightTF.getText());
756 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "conjunctionOrder",
757 proofFinderConjunctionOrderTF.getText());
758 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "conjunctionWeight",
759 proofFinderConjunctionWeightTF.getText());
760 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "equivalenceOrder",
761 proofFinderEquivalenceOrderTF.getText());
762 QedeqGuiConfig.getInstance().setPluginKeyValue(plugin, "equivalenceWeight",
763 proofFinderEquivalenceWeightTF.getText());
764 }
765 } catch (RuntimeException e) {
766 Trace.fatal(CLASS, this, "save", "couldn't save preferences", e);
767 JOptionPane.showMessageDialog(this, e.toString(), "Error",
768 JOptionPane.ERROR_MESSAGE);
769 }
770 try {
771 QedeqGuiConfig.getInstance().store();
772 } catch (IOException e) {
773 Trace.fatal(CLASS, this, "save", "couldn't save preferences", e);
774 JOptionPane.showMessageDialog(this, "Couldn't save preferences", "Error", JOptionPane.ERROR_MESSAGE);
775 }
776 }
777
778 /**
779 * This class is a basic creator for tabbed content.
780 */
781 private abstract class PluginGuiPreferencesCreator {
782
783 /** We work for this plugin. */
784 private final PluginBo plugin;
785
786 /**
787 * Constructor.
788 *
789 * @param plugin Plugin we work for.
790 */
791 PluginGuiPreferencesCreator(final PluginBo plugin) {
792 this.plugin = plugin;
793 }
794
795 /**
796 * Get plugin we work for.
797 *
798 * @return Plugin.
799 */
800 public PluginBo getPlugin() {
801 return plugin;
802 }
803
804 /**
805 * Get plugin action name.
806 *
807 * @return Plugin action name.
808 */
809 public String getName() {
810 return plugin.getPluginActionName();
811 }
812
813 /**
814 * Get default plugin values.
815 *
816 * @return Default values.
817 */
818 private Parameters getDefaultPluginValues() {
819 final Parameters parameters = new Parameters();
820 plugin.setDefaultValuesForEmptyPluginParameters(parameters);
821 return parameters;
822 }
823
824 JComponent createDefault() {
825 return create(getDefaultPluginValues());
826 }
827
828 abstract JComponent create(Parameters parameters);
829
830 }
831
832 }
|