001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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.utility.StringUtility;
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
051 }
052
053 private static void checkDirectoryExistenceAndOptionallyCreate(final QedeqGuiConfig config)
054 throws IOException {
055 // application log file directory
056 {
057 final File file = new File(config.getBasisDirectory(), 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 IoUtility.loadFile(url, buffer, "ISO-8859-1");
096 File traceFile = config.createAbsolutePath("log/trace.txt");
097 StringUtility.replace(buffer, "@trace_file_path@", traceFile.toString()
098 .replace('\\', '/'));
099 // for a properties file:
100 // IoUtility.escapeProperty(traceFile.toString().replace('\\', '/')));
101 IoUtility.saveFile(resource, buffer, "ISO-8859-1");
102 res = IoUtility.toUrl(resource).toString();
103 } catch (IOException e1) {
104 errorPrintln("Resource can not be saved: " + resource.getAbsolutePath());
105 e1.printStackTrace();
106 }
107 }
108 } else {
109 res = IoUtility.toUrl(resource).toString();
110 }
111 System.setProperty("log4j.configDebug", "true");
112 System.setProperty("log4j.configuration", res);
113
114 // init Log4J watchdog
115 try {
116 // set properties and watch file every 5 seconds
117 if (res.endsWith(".xml")) {
118 DOMConfigurator.configureAndWatch(resource.getCanonicalPath(), 5000);
119 } else {
120 PropertyConfigurator.configureAndWatch(resource.getCanonicalPath(), 5000);
121 }
122 } catch (Exception e) {
123 e.printStackTrace();
124 }
125 }
126
127 /**
128 * Print error message. Writes to <code>System.err</code>.
129 *
130 * @param message Message to print.
131 */
132 private static void errorPrintln(final String message) {
133 System.err.println("ERROR>>> " + message);
134 }
135
136 /**
137 * Main method.
138 *
139 * @param args Various parameters. See implementation of {@link #printProgramInformation()}.
140 */
141 public static void main(final String[] args) {
142 String qedeq = null;
143
144 if (args.length == 0) {
145 printProgramInformation();
146 return;
147 }
148
149 for (int i = 0; i < args.length; i++) {
150 if (args[i].startsWith("-")) { // option
151 String option = args[i].substring(1).toLowerCase();
152 if (option.length() <= 0 && i + 1 < args.length) {
153 option = args[i + 1];
154 }
155 if (option.equals("help") || option.equals("h")
156 || option.equals("?")) {
157 printProgramInformation();
158 return;
159 } else { // unknown option
160 printArgumentError("Unknown option: " + option);
161 return;
162 }
163 } else { // no option, must be directory name
164 if (qedeq != null) {
165 printArgumentError("only one QEDEQ module can be searched at once.");
166 return;
167 }
168 qedeq = args[i];
169 }
170 }
171
172 // check parameters
173 if (qedeq == null) {
174 printArgumentError("QEDEQ module must be specified.");
175 return;
176 }
177
178 findProofs(qedeq);
179 }
180
181 /**
182 * Writes calling convention to <code>System.err</code>.
183 */
184 public static void printProgramInformation() {
185 System.err.println("Name");
186 System.err.println("----");
187 System.err.println(Main.class.getName() + " - find simple propositional calculus proofs");
188 System.err.println();
189 System.err.println("Synopsis");
190 System.err.println("--------");
191 System.err.println("[-h] <module url>");
192 System.err.println();
193 System.err.println("Description");
194 System.err.println("-----------");
195 System.err.println("This program finds formal proofs for propositional calculus propositions.");
196 System.err.println("You give it an QEDEQ module URL and the missing formal proofs will be added.");
197 System.err.println("When a proof was found the buffered file (or original if the protocol is");
198 System.err.println("\"file\") will be altered.");
199 System.err.println();
200 System.err.println("Options and Parameter");
201 System.err.println("---------------------");
202 System.err.println("-h writes this text and returns");
203 System.err.println("<module url> URL for QEDEQ module to work on");
204 System.err.println();
205 System.err.println("Example");
206 System.err.println("-------");
207 System.err.println("http://www.qedeq.org/" + KernelContext.getInstance().getKernelVersionDirectory()
208 + "/sample/qedeq_sample4.xml");
209 System.err.println();
210 }
211
212 /**
213 * Print argument error to System.err.
214 *
215 * @param message Message to print.
216 */
217 private static void printArgumentError(final String message) {
218 System.err.println(">>>ERROR reason:");
219 System.err.println(message);
220 System.err.println();
221 System.err.println(">>>Calling convention:");
222 printProgramInformation();
223 }
224
225 public static void findProofs(final String qedeq) {
226 // load configuration file
227 try {
228 QedeqGuiConfig.init(new File(IoUtility.getStartDirectory("qedeq"),
229 "config/org.qedeq.properties"), IoUtility.getStartDirectory("qedeq"));
230 } catch (Throwable e) {
231 e.printStackTrace();
232 System.err.println("Configuration file not found!");
233 System.exit(-1);
234 return;
235 }
236
237 try {
238 // we make a local file copy of the log4j.properties if it dosen't exist already
239 initLog4J(QedeqGuiConfig.getInstance());
240 } catch (Throwable e) {
241 e.printStackTrace();
242 System.err.println("Initialization of Log4J failed!");
243 System.exit(-2);
244 return;
245 }
246
247 try {
248 try {
249 checkDirectoryExistenceAndOptionallyCreate(QedeqGuiConfig.getInstance());
250
251 // add various loggers
252 QedeqLog.getInstance().addLog(new LogListenerImpl()); // System.out
253 QedeqLog.getInstance().addLog(new TraceListener()); // trace file
254 ModuleEventLog.getInstance().addLog(new ModuleEventListenerLog()); // all loggers
255
256 // initialize the kernel, this may create already some logging events
257 KernelContext.getInstance().init(
258 QedeqGuiConfig.getInstance(),
259 new DefaultInternalKernelServices(QedeqGuiConfig.getInstance(),
260 KernelContext.getInstance(), new XmlQedeqFileDao()));
261 KernelContext.getInstance().startup();
262 final ModuleAddress address = KernelContext.getInstance().getModuleAddress(qedeq);
263 KernelContext.getInstance().loadModule(address);
264 KernelContext.getInstance().executePlugin(SimpleProofFinderPlugin.class.getName(),
265 address);
266 KernelContext.getInstance().shutdown();
267 } catch (IOException e) {
268 System.err.println("Application start failed!");
269 System.exit(-3);
270 return;
271 }
272
273 } catch (Throwable e) {
274 e.printStackTrace();
275 System.err.println("Unexpected major failure!");
276 System.exit(-4);
277 return;
278 }
279 }
280
281 }
|