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