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.text.se.main;
017
018 import java.io.File;
019 import java.io.IOException;
020 import java.net.URL;
021
022 import org.apache.log4j.PropertyConfigurator;
023 import org.apache.log4j.xml.DOMConfigurator;
024 import org.qedeq.base.io.IoUtility;
025 import org.qedeq.base.io.UrlUtility;
026 import org.qedeq.gui.se.pane.QedeqGuiConfig;
027 import org.qedeq.kernel.bo.KernelContext;
028 import org.qedeq.kernel.bo.log.LogListenerImpl;
029 import org.qedeq.kernel.bo.log.ModuleEventListenerLog;
030 import org.qedeq.kernel.bo.log.ModuleEventLog;
031 import org.qedeq.kernel.bo.log.QedeqLog;
032 import org.qedeq.kernel.bo.log.TraceListener;
033 import org.qedeq.kernel.bo.service.DefaultInternalKernelServices;
034 import org.qedeq.kernel.bo.service.logic.SimpleProofFinderPlugin;
035 import org.qedeq.kernel.se.common.ModuleAddress;
036 import org.qedeq.kernel.xml.dao.XmlQedeqFileDao;
037
038 /**
039 * This is the main console for a standalone program version of <b>Hilbert II</b>.
040 *
041 * @author Michael Meyling
042 */
043 public final class Main {
044
045 /**
046 * Don't call me.
047 *
048 */
049 private Main() {
050 // nothing to do
051 }
052
053 private static void checkDirectoryExistenceAndOptionallyCreate(final QedeqGuiConfig config)
054 throws IOException {
055 // application log file directory
056 {
057 final File file = config.getLogFile();
058 final File dir = file.getParentFile();
059 if (!dir.exists() && !dir.mkdirs()) {
060 throw new IOException("can't create directory: " + dir.getAbsolutePath());
061 }
062 }
063 }
064
065 /**
066 * Make local copy of Log4J properties if we don't find the Log4J property file in application
067 * config directory. This is necessary especially if the application was launched by
068 * Webstart.
069 * <p>
070 * If the copy action fails, error messages are written to <code>System.err</code> but the
071 * application continues.
072 *
073 * @param config Configuration file.
074 */
075 private static void initLog4J(final QedeqGuiConfig config) {
076 final String resourceName = "log4j.xml";
077 // LATER mime 20070927: hard coded entry "config":
078 String resourceDirectoryName = "config";
079 final File resourceDir = new File(config.getBasisDirectory(), resourceDirectoryName);
080 final File resource = new File(resourceDir, resourceName);
081 String res = "/" + resourceDirectoryName + "/" + resourceName;
082 if (!resource.exists()) {
083 final URL url = Main.class.getResource(res);
084 if (url == null) {
085 errorPrintln("Resource not found: " + res);
086 } else {
087 try {
088 if (!resourceDir.exists()) {
089 if (!resourceDir.mkdirs()) {
090 errorPrintln("Creation of directory failed: "
091 + resourceDir.getAbsolutePath());
092 }
093 }
094 final StringBuffer buffer = new StringBuffer();
095 // if this would be a properties file would have to load it with ISO-8859-1
096 IoUtility.loadFile(url, buffer, "UTF-8");
097 IoUtility.saveFile(resource, buffer, "UTF-8");
098 } catch (IOException e1) {
099 errorPrintln("Resource can not be saved: " + resource.getAbsolutePath());
100 e1.printStackTrace();
101 }
102 }
103 } else {
104 res = UrlUtility.toUrl(resource).toString();
105 }
106 System.setProperty("log4j.configDebug", "true");
107 System.setProperty("log4j.configuration", res);
108
109 // init Log4J watchdog
110 try {
111 // set properties and watch file every 5 seconds
112 if (res.endsWith(".xml")) {
113 DOMConfigurator.configureAndWatch(resource.getCanonicalPath(), 5000);
114 } else {
115 PropertyConfigurator.configureAndWatch(resource.getCanonicalPath(), 5000);
116 }
117 } catch (Exception e) {
118 e.printStackTrace();
119 }
120 }
121
122 /**
123 * Print error message. Writes to <code>System.err</code>.
124 *
125 * @param message Message to print.
126 */
127 private static void errorPrintln(final String message) {
128 System.err.println("ERROR>>> " + message);
129 }
130
131 /**
132 * Main method.
133 *
134 * @param args Various parameters. See implementation of {@link #printProgramInformation()}.
135 */
136 public static void main(final String[] args) {
137 String qedeq = null;
138
139 if (args.length == 0) {
140 printProgramInformation();
141 return;
142 }
143
144 for (int i = 0; i < args.length; i++) {
145 if (args[i].startsWith("-")) { // option
146 String option = args[i].substring(1).toLowerCase();
147 if (option.length() <= 0 && i + 1 < args.length) {
148 option = args[i + 1];
149 }
150 if (option.equals("help") || option.equals("h")
151 || option.equals("?")) {
152 printProgramInformation();
153 return;
154 } else { // unknown option
155 printArgumentError("Unknown option: " + option);
156 return;
157 }
158 } else { // no option, must be directory name
159 if (qedeq != null) {
160 printArgumentError("only one QEDEQ module can be searched at once.");
161 return;
162 }
163 qedeq = args[i];
164 }
165 }
166
167 // check parameters
168 if (qedeq == null) {
169 printArgumentError("QEDEQ module must be specified.");
170 return;
171 }
172
173 findProofs(qedeq);
174 }
175
176 /**
177 * Writes calling convention to <code>System.err</code>.
178 */
179 public static void printProgramInformation() {
180 System.err.println("Name");
181 System.err.println("----");
182 System.err.println(Main.class.getName() + " - find simple propositional calculus proofs");
183 System.err.println();
184 System.err.println("Synopsis");
185 System.err.println("--------");
186 System.err.println("[-h] <module url>");
187 System.err.println();
188 System.err.println("Description");
189 System.err.println("-----------");
190 System.err.println("This program finds formal proofs for propositional calculus propositions.");
191 System.err.println("You give it an QEDEQ module URL and the missing formal proofs will be added.");
192 System.err.println("When a proof was found the buffered file (or original if the protocol is");
193 System.err.println("\"file\") will be altered.");
194 System.err.println();
195 System.err.println("Options and Parameter");
196 System.err.println("---------------------");
197 System.err.println("-h writes this text and returns");
198 System.err.println("<module url> URL for QEDEQ module to work on");
199 System.err.println();
200 System.err.println("Example");
201 System.err.println("-------");
202 System.err.println("http://www.qedeq.org/" + KernelContext.getInstance().getKernelVersionDirectory()
203 + "/sample/qedeq_sample4.xml");
204 System.err.println();
205 }
206
207 /**
208 * Print argument error to System.err.
209 *
210 * @param message Message to print.
211 */
212 private static void printArgumentError(final String message) {
213 System.err.println(">>>ERROR reason:");
214 System.err.println(message);
215 System.err.println();
216 System.err.println(">>>Calling convention:");
217 printProgramInformation();
218 }
219
220 public static void findProofs(final String qedeq) {
221 // load configuration file
222 try {
223 QedeqGuiConfig.init(new File(IoUtility.getStartDirectory("qedeq"),
224 "config/org.qedeq.properties"), IoUtility.getStartDirectory("qedeq"));
225 } catch (Throwable e) {
226 e.printStackTrace();
227 System.err.println("Configuration file not found!");
228 System.exit(-1);
229 return;
230 }
231
232 try {
233 // we make a local file copy of the log4j.properties if it dosen't exist already
234 initLog4J(QedeqGuiConfig.getInstance());
235 } catch (Throwable e) {
236 e.printStackTrace();
237 System.err.println("Initialization of Log4J failed!");
238 System.exit(-2);
239 return;
240 }
241
242 try {
243 try {
244 checkDirectoryExistenceAndOptionallyCreate(QedeqGuiConfig.getInstance());
245
246 // add various loggers
247 QedeqLog.getInstance().addLog(new LogListenerImpl()); // System.out
248 QedeqLog.getInstance().addLog(new TraceListener()); // trace file
249 ModuleEventLog.getInstance().addLog(new ModuleEventListenerLog()); // all loggers
250
251 // initialize the kernel, this may create already some logging events
252 KernelContext.getInstance().init(
253 QedeqGuiConfig.getInstance(),
254 new DefaultInternalKernelServices(QedeqGuiConfig.getInstance(),
255 KernelContext.getInstance(), new XmlQedeqFileDao()));
256 KernelContext.getInstance().startup();
257 final ModuleAddress address = KernelContext.getInstance().getModuleAddress(qedeq);
258 KernelContext.getInstance().loadModule(address);
259 KernelContext.getInstance().executePlugin(SimpleProofFinderPlugin.class.getName(),
260 address, null);
261 KernelContext.getInstance().shutdown();
262 } catch (IOException e) {
263 System.err.println("Application start failed!");
264 System.exit(-3);
265 return;
266 }
267
268 } catch (Throwable e) {
269 e.printStackTrace();
270 System.err.println("Unexpected major failure!");
271 System.exit(-4);
272 return;
273 }
274 }
275
276 }
|