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.control;
017
018 import java.util.ArrayList;
019
020 import javax.swing.Action;
021 import javax.swing.JFrame;
022 import javax.swing.JMenuItem;
023 import javax.swing.JOptionPane;
024
025 import org.qedeq.gui.se.tree.NothingSelectedException;
026 import org.qedeq.gui.se.tree.QedeqTreeCtrl;
027 import org.qedeq.gui.se.util.DataDictionary;
028 import org.qedeq.gui.se.util.GuiHelper;
029 import org.qedeq.gui.se.util.MenuHelper;
030 import org.qedeq.kernel.bo.KernelContext;
031 import org.qedeq.kernel.bo.common.QedeqBo;
032 import org.qedeq.kernel.se.common.Plugin;
033
034
035 /**
036 * Controller for a the GUI application.
037 *
038 * A Controller, which represents the classes connecting the model and the view, and is used to
039 * communicate between classes in the model and view.
040 * Connects the models and the views. Handles program flow.
041 *
042 * LATER mime 20070605: encapsulate actions that need another thread
043 * for later java versions: use Executor framework
044 *
045 * @author Michael Meyling
046 */
047 public class QedeqController {
048
049 /** Tree controller. */
050 private QedeqTreeCtrl treeCtrl;
051
052 /** About action. */
053 private final Action aboutAction;
054
055 /** Help action. */
056 private final Action helpAction;
057
058 /** Exit action. */
059 private final Action exitAction;
060
061 /** Add QEDEQ module from web. */
062 private final Action addAction;
063
064 /** Add QEDEQ module from local file. */
065 private final Action addFileAction;
066
067 /** Remove all QEDEQ modules from memory. */
068 private final Action removeAllAction;
069
070 /** Remove all QEDEQ modules from local buffer. */
071 private final Action removeLocalBufferAction;
072
073 /** Remove all selected QEDEQ modules from memory. */
074 private final Action removeModuleAction;
075
076 /** Add all modules from <a href="http://www.qedeq.org/">Hilbert II</a> webpage. */
077 private final Action addAllModulesFromQedeqAction;
078
079 /** Show all service processes. */
080 private final Action processViewAction;
081
082 /** Terminate all service processes. */
083 private final Action terminateAllAction;
084
085 /** Check if QEDEQ modules are well formed. */
086 private final Action checkWellFormedAction;
087
088 /** Check if QEDEQ modules are fully and correctly formally proved. */
089 private final Action checkFormallyProvedAction;
090
091 /** Remove all plugin results for QEDEQ module. */
092 private final Action removePluginResultsAction;
093
094 /** Show preferences window. */
095 private final Action preferencesAction;
096
097 /** Show plugin preferences window. */
098 private final Action pluginPreferencesAction;
099
100 /** Show parser window. */
101 private final Action latexParserAction;
102
103 /** Show parser window. */
104 private final Action textParserAction;
105
106 /** Show parser window. */
107 private final Action proofTextParserAction;
108
109 /** List of already wanted QEDEQ modules.*/
110 private final ArrayList moduleHistory;
111
112 /** Reference to main frame. */
113 private final JFrame main;
114
115 /** Maximum number of entries in history. */
116 static final int MAXIMUM_MODULE_HISTORY = 20; // LATER 20070606: put into properties
117
118 /**
119 * Constructor.
120 *
121 * @param main Reference to main frame.
122 */
123 public QedeqController(final JFrame main) {
124 this.main = main;
125 aboutAction = new AboutAction(this);
126 helpAction = new HelpAction(this);
127 preferencesAction = new PreferencesAction(this);
128 pluginPreferencesAction = new PluginPreferencesAction(this);
129 latexParserAction = new LatexParserAction(this);
130 textParserAction = new TextParserAction(this);
131 proofTextParserAction = new ProofTextParserAction(this);
132 exitAction = new ExitAction();
133 addAction = new AddAction(this);
134 addFileAction = new AddFileAction(this);
135 addAllModulesFromQedeqAction = new AddAllModulesFromQedeqAction();
136 removeAllAction = new RemoveAllAction();
137 removeModuleAction = new RemoveModuleAction(this);
138 removeLocalBufferAction = new RemoveLocalBufferAction();
139 checkWellFormedAction = new CheckWellFormedAction(this);
140 checkFormallyProvedAction = new CheckFormallyProvedAction(this);
141 removePluginResultsAction = new RemovePluginResultsAction(this);
142 processViewAction = new ProcessViewAction();
143 terminateAllAction = new TerminateAllAction();
144
145 final String[] list = KernelContext.getInstance().getConfig().getModuleHistory();
146 moduleHistory = new ArrayList();
147 for (int i = 0; i < list.length; i++) {
148 getModuleHistory().add(list[i]);
149 }
150
151 // LATER mime 20070606: dynamic evaluation from web page?
152 if (getModuleHistory().size() == 0) {
153 final String prefix = "http://wwww.qedeq.org/"
154 + KernelContext.getInstance().getKernelVersionDirectory() + "/doc/";
155 getModuleHistory().add(prefix + "math/qedeq_logic_v1.xml");
156 getModuleHistory().add(prefix + "math/qedeq_formal_logic_v1.xml");
157 getModuleHistory().add(prefix + "math/qedeq_set_theory_v1.xml");
158 getModuleHistory().add(prefix + "project/qedeq_basic_concept.xml");
159 getModuleHistory().add(prefix + "project/qedeq_logic_language.xml");
160 getModuleHistory().add(prefix + "sample/qedeq_sample1.xml");
161 getModuleHistory().add(prefix + "sample/qedeq_sample2.xml");
162 getModuleHistory().add(prefix + "sample/qedeq_sample3.xml");
163 getModuleHistory().add(prefix + "sample/qedeq_sample4.xml");
164 }
165 }
166
167 /**
168 * Set tree controller.
169 *
170 * @param treeCtrl Tree controller.
171 */
172 public void setTreeCtrl(final QedeqTreeCtrl treeCtrl) {
173 this.treeCtrl = treeCtrl;
174 }
175
176 /**
177 * Get selected module.
178 *
179 * @return Selected modules.
180 * @throws NothingSelectedException No modules were selected.
181 */
182 public QedeqBo[] getSelected() throws NothingSelectedException {
183 return treeCtrl.getSelected();
184 }
185
186 /**
187 * Get about action.
188 *
189 * @return Action.
190 */
191 public Action getAboutAction() {
192 return aboutAction;
193 }
194
195 /**
196 * Get help action.
197 *
198 * @return Action.
199 */
200 public Action getHelpAction() {
201 return helpAction;
202 }
203
204 /**
205 * Get preferences window startup action.
206 *
207 * @return Action.
208 */
209 public Action getPreferencesAction() {
210 return preferencesAction;
211 }
212
213 /**
214 * Get plugin preferences window startup action.
215 *
216 * @return Action.
217 */
218 public Action getPluginPreferencesAction() {
219 return pluginPreferencesAction;
220 }
221
222 /**
223 * Get parser window startup action.
224 *
225 * @return Action.
226 */
227 public Action getLatexParserAction() {
228 return latexParserAction;
229 }
230
231 /**
232 * Get parser window startup action.
233 *
234 * @return Action.
235 */
236 public Action getTextParserAction() {
237 return textParserAction;
238 }
239
240 /**
241 * Get parser window startup action.
242 *
243 * @return Action.
244 */
245 public Action getProofTextParserAction() {
246 return proofTextParserAction;
247 }
248
249 /**
250 * Get exit action.
251 *
252 * @return Action.
253 */
254 public Action getExitAction() {
255 return exitAction;
256 }
257
258 /**
259 * Get action for adding a new QEDEQ module out of the web.
260 *
261 * @return Action.
262 */
263 public Action getAddAction() {
264 return addAction;
265 }
266
267 /**
268 * Get action for adding a new QEDEQ module from a local file.
269 *
270 * @return Action.
271 */
272 public Action getAddFileAction() {
273 return addFileAction;
274 }
275
276 /**
277 * Get all plugin actions as menu entries.
278 *
279 * @return Menu entries for plugins.
280 */
281 public JMenuItem[] getPluginMenuEntries() {
282 final Plugin[] plugins = KernelContext.getInstance().getPlugins();
283 final PluginAction[] pluginActions = new PluginAction[plugins.length];
284 for (int i = 0; i < plugins.length; i++) {
285 pluginActions[i] = new PluginAction(this, plugins[i]);
286 }
287 JMenuItem[] result = new JMenuItem[pluginActions.length];
288 for (int i = 0; i < pluginActions.length; i++) {
289 final JMenuItem item = MenuHelper.createMenuItem(pluginActions[i].getPlugin()
290 .getPluginActionName());
291 item.addActionListener(pluginActions[i]);
292 item.setIcon(pluginActions[i].getIcon());
293 item.setToolTipText(GuiHelper.getToolTipText(pluginActions[i].getPlugin()
294 .getPluginDescription()));
295 result[i] = item;
296 }
297 return result;
298 }
299
300 /**
301 * Get action for checking if the selected QEDEQ modules are well formed.
302 *
303 * @return Action.
304 */
305 public Action getCheckWellFormedAction() {
306 return checkWellFormedAction;
307 }
308
309 /**
310 * Get action for checking if the selected QEDEQ modules are fully and formally correctly proved.
311 *
312 * @return Action.
313 */
314 public Action getCheckFormallyProvedAction() {
315 return checkFormallyProvedAction;
316 }
317
318 /**
319 * Get action for removing all plugin results for the selected QEDEQ modules.
320 *
321 * @return Action.
322 */
323 public Action getRemovePluginResultsAction() {
324 return removePluginResultsAction;
325 }
326
327 /**
328 * Get action for removing all QEDEQ modules from memory.
329 *
330 * @return Action.
331 */
332 public Action getRemoveAllAction() {
333 return removeAllAction;
334 }
335
336 /**
337 * Get action for removing all seelected QEDEQ modules from memory.
338 *
339 * @return Action.
340 */
341 public Action getRemoveModuleAction() {
342 return removeModuleAction;
343 }
344
345 /**
346 * Get action for removing all QEDEQ modules from memory and local buffer.
347 *
348 * @return Action.
349 */
350 public Action getRemoveLocalBufferAction() {
351 return removeLocalBufferAction;
352 }
353
354 /**
355 * Get action for loading all QEDEQ modules for the current release from the QEDEQ web site.
356 *
357 * @return Action.
358 */
359 public Action getAddAllModulesFromQedeqAction() {
360 return addAllModulesFromQedeqAction;
361 }
362
363 /**
364 * Get action for starting the service process viewer.
365 *
366 * @return Action.
367 */
368 public Action getProcessViewAction() {
369 return processViewAction;
370 }
371
372 /**
373 * Get action for stopping all currently running plugin actions.
374 *
375 * @return Action.
376 */
377 public Action getTerminateAllAction() {
378 return terminateAllAction;
379 }
380
381 /**
382 * This method returns a string from the resource bundle.
383 *
384 * @param key Name to look for.
385 * @return Value.
386 */
387 public String getString(final String key) {
388 return DataDictionary.getInstance().getString(key);
389 }
390
391 /**
392 * Returns a mnemonic from the resource bundle. Typically used as
393 * keyboard shortcuts in menu items.
394 *
395 * @param key Name to look for.
396 * @return Mnemonic.
397 */
398 public char getMnemonic(final String key) {
399 return DataDictionary.getInstance().getMnemonic(key);
400 }
401
402 void addToModuleHistory(final String url) {
403 getModuleHistory().add(0, url);
404 for (int i = 1; i < getModuleHistory().size(); i++) {
405 if (url.equals(getModuleHistory().get(i))) {
406 getModuleHistory().remove(i);
407 i--;
408 }
409 }
410 for (int i = getModuleHistory().size() - 1; i >= QedeqController.MAXIMUM_MODULE_HISTORY;
411 i--) {
412 getModuleHistory().remove(i);
413 }
414 KernelContext.getInstance().getConfig().saveModuleHistory(getModuleHistory());
415 }
416
417 ArrayList getModuleHistory() {
418 return moduleHistory;
419 }
420
421 JFrame getMainFrame() {
422 return main;
423 }
424
425 void selectionError() {
426 JOptionPane.showMessageDialog(
427 QedeqController.this.main,
428 "No QEDEQ module selected! In the tree at least one QEDEQ module must be selected",
429 "Error",
430 JOptionPane.ERROR_MESSAGE,
431 null);
432 }
433
434 }
|