Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
../../../../../img/srcFileCovDistChart4.png 82% of files have more coverage
353   843   114   9,05
84   639   0,32   39
39     2,92  
1    
 
  DefaultInternalKernelServices       Line # 65 353 114 39,5% 0.394958
 
  (40)
 
1    /* $Id: DefaultInternalKernelServices.java,v 1.2 2008/08/02 04:33:09 m31 Exp $
2    *
3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
4    *
5    * Copyright 2000-2008, Michael Meyling <mime@qedeq.org>.
6    *
7    * "Hilbert II" is free software; you can redistribute
8    * it and/or modify it under the terms of the GNU General Public
9    * License as published by the Free Software Foundation; either
10    * version 2 of the License, or (at your option) any later version.
11    *
12    * This program is distributed in the hope that it will be useful,
13    * but WITHOUT ANY WARRANTY; without even the implied warranty of
14    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15    * GNU General Public License for more details.
16    */
17   
18    package org.qedeq.kernel.bo.service;
19   
20    import java.io.File;
21    import java.io.FileFilter;
22    import java.io.FileNotFoundException;
23    import java.io.FileOutputStream;
24    import java.io.IOException;
25    import java.io.InputStream;
26    import java.io.UnsupportedEncodingException;
27    import java.net.HttpURLConnection;
28    import java.net.MalformedURLException;
29    import java.net.URL;
30    import java.net.URLConnection;
31    import java.net.URLEncoder;
32    import java.util.ArrayList;
33    import java.util.List;
34   
35    import org.qedeq.base.io.IoUtility;
36    import org.qedeq.base.io.TextInput;
37    import org.qedeq.base.trace.Trace;
38    import org.qedeq.base.utility.StringUtility;
39    import org.qedeq.kernel.base.module.Qedeq;
40    import org.qedeq.kernel.base.module.Specification;
41    import org.qedeq.kernel.bo.QedeqBo;
42    import org.qedeq.kernel.bo.context.KernelProperties;
43    import org.qedeq.kernel.bo.context.KernelServices;
44    import org.qedeq.kernel.bo.log.QedeqLog;
45    import org.qedeq.kernel.bo.module.InternalKernelServices;
46    import org.qedeq.kernel.bo.module.KernelQedeqBo;
47    import org.qedeq.kernel.bo.module.QedeqFileDao;
48    import org.qedeq.kernel.bo.service.latex.Qedeq2Latex;
49    import org.qedeq.kernel.common.DefaultSourceFileExceptionList;
50    import org.qedeq.kernel.common.DependencyState;
51    import org.qedeq.kernel.common.LoadingState;
52    import org.qedeq.kernel.common.LogicalState;
53    import org.qedeq.kernel.common.ModuleAddress;
54    import org.qedeq.kernel.common.ModuleDataException;
55    import org.qedeq.kernel.common.SourceFileException;
56    import org.qedeq.kernel.common.SourceFileExceptionList;
57    import org.qedeq.kernel.dto.module.QedeqVo;
58   
59    /**
60    * This class provides a default implementation for the QEDEQ module services.
61    *
62    * @version $Revision: 1.2 $
63    * @author Michael Meyling
64    */
 
65    public class DefaultInternalKernelServices implements KernelServices, InternalKernelServices {
66   
67    /** This class. */
68    private static final Class CLASS = DefaultInternalKernelServices.class;
69   
70    /** For synchronized waiting. */
71    private final String monitor = "";
72   
73    /** Number of method calls. */
74    private volatile int processCounter = 0;
75   
76    /** Collection of already known QEDEQ modules. */
77    private final KernelQedeqBoStorage modules;
78   
79    /** Kernel properties access. */
80    private final KernelProperties kernel;
81   
82    /** This instance nows how to load a module from the file system. */
83    private final QedeqFileDao qedeqFileDao;
84   
85    /** Validate module dependencies and status. */
86    private boolean validate = true;
87   
88    /**
89    * Constructor.
90    *
91    * @param kernel For kernel access.
92    * @param loader For loading QEDEQ modules.
93    */
 
94  39 toggle public DefaultInternalKernelServices(final KernelProperties kernel, final QedeqFileDao loader) {
95  39 modules = new KernelQedeqBoStorage();
96  39 this.kernel = kernel;
97  39 this.qedeqFileDao = loader;
98  39 loader.setServices(this);
99    }
100   
 
101  39 toggle public void startup() {
102  39 if (kernel.getConfig().isAutoReloadLastSessionChecked()) {
103  0 autoReloadLastSessionChecked();
104    }
105    }
106   
107    /**
108    * If configured load all QEDEQ modules that where successfully loaded the last time.
109    */
 
110  0 toggle public void autoReloadLastSessionChecked() {
111  0 if (kernel.getConfig().isAutoReloadLastSessionChecked()) {
112  0 final Thread thread = new Thread() {
 
113  0 toggle public void run() {
114  0 final String method = "autoReloadLastSessionChecked.thread.run()";
115  0 try {
116  0 Trace.begin(CLASS, this, method);
117  0 QedeqLog.getInstance().logMessage(
118    "Trying to load previously successfully loaded modules.");
119  0 final int number = kernel.getConfig().getPreviouslyCheckedModules().length;
120  0 if (loadPreviouslySuccessfullyLoadedModules()) {
121  0 QedeqLog.getInstance().logMessage(
122    "Loading of " + number + " previously successfully loaded module"
123  0 + (number != 1 ? "s" : "") + " successfully done.");
124    } else {
125  0 QedeqLog.getInstance().logMessage(
126    "Loading of all previously successfully checked modules failed. "
127  0 + number + " module" + (number != 1 ? "s" : "")
128    + " were tried.");
129    }
130    } catch (Exception e) {
131  0 Trace.trace(CLASS, this, method, e);
132    } finally {
133  0 Trace.end(CLASS, this, method);
134    }
135    }
136    };
137  0 thread.setDaemon(true);
138  0 thread.start();
139    }
140    }
141   
 
142  0 toggle public void removeAllModules() {
143  0 do {
144  0 synchronized (this) {
145  0 if (processCounter == 0) {
146  0 getModules().removeAllModules();
147  0 return;
148    }
149    }
150    // we must wait for the other processes to stop (so that processCounter == 0)
151  0 synchronized (monitor) {
152  0 try {
153  0 monitor.wait(10000);
154    } catch (InterruptedException e) {
155    }
156    }
157    } while (true);
158   
159    }
160   
161    /**
162    * Remove a QEDEQ module from memory.
163    *
164    * @param address Remove module identified by this address.
165    */
 
166  0 toggle public void removeModule(final ModuleAddress address) {
167  0 final QedeqBo prop = getQedeqBo(address);
168  0 if (prop != null) {
169  0 removeModule(getModules().getKernelQedeqBo(this, address));
170  0 if (validate) {
171  0 modules.validateDependencies();
172    }
173    }
174    }
175   
176    /**
177    * Remove a QEDEQ module from memory. This method must block all other methods and if this
178    * method runs no other is allowed to run
179    *
180    * @param prop Remove module identified by this property.
181    */
 
182  0 toggle private void removeModule(final DefaultKernelQedeqBo prop) {
183  0 do {
184  0 synchronized (this) {
185  0 if (processCounter == 0) { // no other method is allowed to run
186    // TODO mime 20080319: one could call prop.setLoadingProgressState(
187    // LoadingState.STATE_DELETED) alone but that would
188    // miss to inform the KernelQedeqBoPool. How do we inform the pool?
189    // must the StateManager have a reference to it?
190  0 prop.delete();
191  0 getModules().removeModule(prop);
192  0 return;
193    }
194    }
195    // we must wait for the other processes to stop (so that processCounter == 0)
196  0 synchronized (monitor) {
197  0 try {
198  0 this.monitor.wait(10000);
199    } catch (InterruptedException e) {
200    }
201    }
202    } while (true);
203   
204    }
205   
206    /**
207    * Clear local file buffer and all loaded QEDEQ modules.
208    *
209    * @throws IOException Deletion of all buffered file was not successful.
210    */
 
211  0 toggle public void clearLocalBuffer() throws IOException {
212  0 removeAllModules();
213  0 final File bufferDir = getBufferDirectory().getCanonicalFile();
214  0 if (bufferDir.exists() && !IoUtility.deleteDir(bufferDir, new FileFilter() {
 
215  0 toggle public boolean accept(final File pathname) {
216  0 return pathname.getName().endsWith(".xml");
217    }
218    })) {
219  0 throw new IOException("buffer could not be deleted: " + bufferDir);
220    }
221    }
222   
 
223  174 toggle public QedeqBo loadModule(final ModuleAddress address) {
224  174 final String method = "loadModule(ModuleAddress)";
225  174 processInc();
226  174 final DefaultKernelQedeqBo prop = getModules().getKernelQedeqBo(this, address);
227  174 try {
228  174 synchronized (prop) {
229  174 if (prop.isLoaded()) {
230  126 return prop;
231    }
232  48 QedeqLog.getInstance().logRequest("Load module \"" + address + "\"");
233  48 if (prop.getModuleAddress().isFileAddress()) {
234  38 loadLocalModule(prop);
235    } else {
236    // search in local file buffer
237  10 try {
238  10 getCanonicalReadableFile(prop);
239    } catch (ModuleFileNotFoundException e) { // file not found
240    // we will continue by creating a local copy
241  0 saveQedeqFromWebToBuffer(prop);
242    }
243  10 loadBufferedModule(prop);
244    }
245  42 QedeqLog.getInstance().logSuccessfulReply(
246    "Module \"" + prop.getModuleAddress().getFileName()
247    + "\" was successfully loaded.");
248    }
249    } catch (SourceFileExceptionList e) {
250  6 Trace.trace(CLASS, this, method, e);
251  6 QedeqLog.getInstance().logFailureState("Loading of module failed!", address.getURL(),
252    e.toString());
253    } catch (final RuntimeException e) {
254  0 Trace.fatal(CLASS, this, method, "unexpected problem", e);
255  0 QedeqLog.getInstance().logFailureReply("Loading failed", e.getMessage());
256    } finally {
257  174 processDec();
258    }
259  48 return prop;
260    }
261   
262    /**
263    * Load buffered QEDEQ module file.
264    *
265    * @param prop Load this.
266    * @throws SourceFileExceptionList Loading or QEDEQ module failed.
267    */
 
268  10 toggle private void loadBufferedModule(final DefaultKernelQedeqBo prop) throws SourceFileExceptionList {
269  10 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_BUFFER);
270  10 final File localFile;
271  10 try {
272  10 localFile = getCanonicalReadableFile(prop);
273    } catch (ModuleFileNotFoundException e) {
274  0 final SourceFileExceptionList sfl = createSourcelFileExceptionList(e);
275  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
276  0 throw sfl;
277    }
278   
279  10 prop.setQedeqFileDao(getQedeqFileDao()); // remember loader for this module
280  10 final Qedeq qedeq;
281  10 try {
282  10 qedeq = getQedeqFileDao().loadQedeq(prop, localFile);
283    } catch (IOException e) {
284  0 final SourceFileExceptionList sfl = new DefaultSourceFileExceptionList(e);
285  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
286  0 throw sfl;
287    } catch (SourceFileExceptionList sfl) {
288  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
289  0 throw sfl;
290    }
291  10 setCopiedQedeq(prop, qedeq);
292    }
293   
294    /**
295    * Load QEDEQ module file with file loader.
296    *
297    * @param prop Load this.
298    * @throws SourceFileExceptionList Loading or copying QEDEQ module failed.
299    */
 
300  101 toggle private void loadLocalModule(final DefaultKernelQedeqBo prop) throws SourceFileExceptionList {
301  101 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE);
302  101 final File localFile;
303  101 try {
304  101 localFile = getCanonicalReadableFile(prop);
305    } catch (ModuleFileNotFoundException e) {
306  1 final SourceFileExceptionList sfl = createSourcelFileExceptionList(e);
307  1 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE_FAILED, sfl);
308  1 throw sfl;
309    }
310  100 prop.setQedeqFileDao(getQedeqFileDao()); // remember loader for this module
311   
312  100 final Qedeq qedeq;
313  100 try {
314  100 qedeq = getQedeqFileDao().loadQedeq(prop, localFile);
315    } catch (IOException e) {
316  0 final SourceFileExceptionList sfl = new DefaultSourceFileExceptionList(e);
317  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
318  0 throw sfl;
319    } catch (SourceFileExceptionList sfl) {
320  4 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE_FAILED, sfl);
321  4 throw sfl;
322    }
323  96 setCopiedQedeq(prop, qedeq);
324    }
325   
 
326  106 toggle private void setCopiedQedeq(final DefaultKernelQedeqBo prop, final Qedeq qedeq)
327    throws SourceFileExceptionList {
328  106 final String method = "setCopiedQedeq(KernelQedeqBo, Qedeq)";
329  106 prop.setLoadingProgressState(LoadingState.STATE_LOADING_INTO_MEMORY);
330  106 QedeqVo vo = null;
331  106 try {
332  106 vo = QedeqVoBuilder.createQedeq(prop.getModuleAddress(), qedeq);
333    } catch (ModuleDataException e) {
334  0 Trace.trace(CLASS, this, method, e);
335  0 final SourceFileExceptionList xl = prop.createSourceFileExceptionList(e, qedeq);
336  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, xl);
337  0 throw xl;
338    }
339  106 prop.setQedeqVo(vo);
340  106 ModuleLabelsCreator moduleNodesCreator = new ModuleLabelsCreator(prop);
341  106 try {
342  106 prop.setLoaded(vo, moduleNodesCreator.createLabels());
343    } catch (SourceFileExceptionList sfl) {
344  2 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, sfl);
345  2 throw sfl;
346    }
347    }
348   
349    /**
350    * Check if file exists and is readable. Checks the local buffer file for a buffered module or
351    * the module file address directly. Returns canonical file path.
352    *
353    * @param prop Check for this file.
354    * @return Canonical file path.
355    * @throws ModuleFileNotFoundException File doesn't exist or is not readable.
356    */
 
357  121 toggle private File getCanonicalReadableFile(final QedeqBo prop) throws ModuleFileNotFoundException {
358  121 final String method = "checkLocalBuffer(File)";
359  121 final File localFile = getLocalFilePath(prop.getModuleAddress());
360  121 final File file;
361  121 try {
362  121 file = localFile.getCanonicalFile();
363    } catch (IOException e) {
364  0 Trace.trace(CLASS, this, method, e);
365  0 throw new ModuleFileNotFoundException("file path not correct: " + localFile);
366    }
367  121 if (!file.canRead()) {
368  1 Trace.trace(CLASS, this, method, "file not readable=" + file);
369  1 throw new ModuleFileNotFoundException("file not readable: " + file);
370    }
371  120 return file;
372    }
373   
374    /**
375    * Load specified QEDEQ module from QEDEQ parent module.
376    *
377    * @param parent Parent module address.
378    * @param spec Specification for another QEDEQ module.
379    * @return Loaded module.
380    * @throws SourceFileExceptionList Loading failed.
381    */
 
382  188 toggle public KernelQedeqBo loadModule(final ModuleAddress parent, final Specification spec)
383    throws SourceFileExceptionList {
384   
385  188 final String method = "loadModule(Module, Specification)";
386  188 Trace.begin(CLASS, this, method);
387  188 Trace.trace(CLASS, this, method, spec);
388  188 processInc();
389  188 DefaultKernelQedeqBo prop = null; // currently tried module
390  188 try {
391  188 final ModuleAddress[] modulePaths;
392  188 try {
393  188 modulePaths = parent.getModulePaths(spec);
394    } catch (IOException e) {
395  0 Trace.trace(CLASS, this, method, e);
396  0 throw createSourceFileExceptionList(e);
397    }
398   
399    // now we iterate over the possible module addresses
400  188 for (int i = 0; i < modulePaths.length; i++) {
401  188 prop = getModules().getKernelQedeqBo(this, modulePaths[i]);
402  188 Trace.trace(CLASS, this, method, "synchronizing at prop=" + prop);
403  188 synchronized (prop) {
404  188 if (prop.isLoaded()) {
405  125 return (prop);
406    }
407  63 try {
408  63 if (prop.getModuleAddress().isFileAddress()) {
409  63 loadLocalModule(prop);
410    } else {
411    // search in local file buffer
412  0 try {
413  0 getCanonicalReadableFile(prop);
414    } catch (ModuleFileNotFoundException e) { // file not found
415    // we will continue by creating a local copy
416  0 saveQedeqFromWebToBuffer(prop);
417    }
418  0 loadBufferedModule(prop);
419    }
420    // success!
421  62 return prop;
422    } catch (SourceFileExceptionList e) {
423  1 Trace.trace(CLASS, this, method, e);
424  1 if (i + 1 < modulePaths.length) {
425  0 QedeqLog.getInstance().logMessage("trying alternate path");
426    // we continue with the next path
427    } else {
428    // we surrender
429  1 throw e;
430    }
431    }
432    }
433    }
434  0 return prop; // never called, only here to soothe the compiler
435   
436    } finally {
437  188 processDec();
438  188 Trace.end(CLASS, this, method);
439    }
440    }
441   
 
442  39 toggle public ModuleAddress[] getAllLoadedModules() {
443  39 return getModules().getAllLoadedModules();
444    }
445   
 
446  63 toggle public void loadRequiredModules(final ModuleAddress address) throws SourceFileExceptionList {
447  63 final DefaultKernelQedeqBo prop = (DefaultKernelQedeqBo) loadModule(address);
448  63 if (prop.hasFailures()) {
449  0 throw prop.getException(); // FIXME mime 20080603: remove exception from signature
450    // of this function and also from loadRequired
451    }
452  63 LoadRequiredModules.loadRequired(prop);
453    }
454   
455    /**
456    * Load all previously checked QEDEQ modules.
457    *
458    * @return Successfully reloaded all modules.
459    */
 
460  0 toggle public boolean loadPreviouslySuccessfullyLoadedModules() {
461  0 processInc();
462  0 try {
463  0 final String[] list = kernel.getConfig().getPreviouslyCheckedModules();
464  0 boolean errors = false;
465  0 for (int i = 0; i < list.length; i++) {
466  0 try {
467  0 final ModuleAddress address = getModuleAddress(list[i]);
468  0 final QedeqBo prop = loadModule(address);
469  0 if (prop.hasFailures()) {
470  0 errors = true;
471    }
472    } catch (IOException e) {
473  0 Trace.fatal(CLASS, this, "loadPreviouslySuccessfullyLoadedModules",
474    "internal error: " + "saved URLs are malformed", e);
475  0 errors = true;
476    }
477    }
478  0 return !errors;
479    } finally {
480  0 processDec();
481    }
482    }
483   
484    // LATER mime 20070326: dynamic loading from web page directory
 
485  0 toggle public boolean loadAllModulesFromQedeq() {
486  0 processInc();
487  0 try {
488  0 final String prefix = "http://qedeq.org/" + kernel.getKernelVersionDirectory() + "/";
489  0 final String[] list = new String[] { prefix + "doc/math/qedeq_logic_v1.xml",
490    prefix + "doc/math/qedeq_set_theory_v1.xml",
491    prefix + "doc/project/qedeq_basic_concept.xml",
492    prefix + "doc/project/qedeq_logic_language.xml",
493    prefix + "sample/qedeq_sample1.xml", prefix + "sample/qedeq_error_sample_00.xml",
494    prefix + "sample/qedeq_error_sample_01.xml",
495    prefix + "sample/qedeq_error_sample_02.xml",
496    prefix + "sample/qedeq_error_sample_03.xml",
497    prefix + "sample/qedeq_error_sample_04.xml",
498    prefix + "sample/qedeq_sample2_error.xml",
499    prefix + "sample/qedeq_sample3_error.xml",
500    prefix + "sample/qedeq_sample4_error.xml",
501    prefix + "sample/qedeq_sample5_error.xml",
502    prefix + "sample/qedeq_sample6_error.xml",
503    prefix + "sample/qedeq_sample7_error.xml", };
504  0 boolean errors = false;
505  0 for (int i = 0; i < list.length; i++) {
506  0 try {
507  0 final ModuleAddress address = getModuleAddress(list[i]);
508  0 final QedeqBo prop = loadModule(address);
509  0 if (prop.hasFailures()) {
510  0 errors = true;
511    }
512    } catch (IOException e) {
513  0 Trace.fatal(CLASS, this, "loadPreviouslySuccessfullyLoadedModules",
514    "internal error: " + "saved URLs are malformed", e);
515  0 errors = true;
516    }
517    }
518  0 return !errors;
519    } finally {
520  0 processDec();
521    }
522    }
523   
524    /**
525    * Make local copy of a module if it is no file address.
526    *
527    * @param prop Module properties.
528    * @throws SourceFileExceptionList Address was malformed or the file can not be found.
529    */
 
530  0 toggle public void saveQedeqFromWebToBuffer(final DefaultKernelQedeqBo prop)
531    throws SourceFileExceptionList {
532  0 final String method = "makeLocalCopy";
533  0 Trace.begin(CLASS, this, method);
534   
535  0 if (prop.getModuleAddress().isFileAddress()) { // this is already a local file
536  0 Trace.fatal(CLASS, this, method, "tried to make a local copy for a local module", null);
537  0 Trace.end(CLASS, this, method);
538  0 return;
539    }
540  0 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_WEB);
541   
542  0 FileOutputStream out = null;
543  0 InputStream in = null;
544  0 final File f = getLocalFilePath(prop.getModuleAddress());
545  0 try {
546  0 final URLConnection connection = prop.getUrl().openConnection();
547   
548  0 if (connection instanceof HttpURLConnection) {
549  0 final HttpURLConnection httpConnection = (HttpURLConnection) connection;
550  0 int responseCode = httpConnection.getResponseCode();
551  0 if (responseCode == 200) {
552  0 in = httpConnection.getInputStream();
553    } else {
554  0 in = httpConnection.getErrorStream(); // FIXME do something with this stream?
555  0 throw new IOException("Response code from HTTP server was " + responseCode);
556    // FIXME give more explanation over response codes
557    }
558    } else {
559  0 Trace.paramInfo(CLASS, this, method, "connection.getClass", connection.getClass()
560    .toString());
561  0 in = connection.getInputStream();
562    }
563   
564  0 if (!prop.getUrl().equals(connection.getURL())) {
565  0 throw new FileNotFoundException("\"" + prop.getUrl() + "\" was substituted by "
566    + "\"" + connection.getURL() + "\" from server");
567    }
568  0 final int maximum = connection.getContentLength();
569  0 IoUtility.createNecessaryDirectories(f);
570  0 out = new FileOutputStream(f);
571  0 final byte[] buffer = new byte[4096];
572  0 int bytesRead; // bytes read during one buffer read
573  0 int position = 0; // current reading position within the whole document
574    // continue writing
575  0 while ((bytesRead = in.read(buffer)) != -1) {
576  0 position += bytesRead;
577  0 out.write(buffer, 0, bytesRead);
578  0 if (maximum > 0) {
579  0 long completeness = (long) (position * 100 / maximum);
580  0 if (completeness < 0) {
581  0 completeness = 0;
582    }
583  0 if (completeness > 100) {
584  0 completeness = 100;
585    }
586  0 prop.setLoadingCompleteness((int) completeness);
587    }
588    }
589  0 prop.setLoadingCompleteness(100);
590    } catch (IOException e) {
591  0 Trace.trace(CLASS, this, method, e);
592  0 IoUtility.close(out);
593  0 out = null;
594  0 try {
595  0 f.delete(); // FIXME do we really want to delete it? Perhaps there are infos in it!!
596    } catch (Exception ex) {
597  0 Trace.trace(CLASS, this, method, ex);
598    }
599  0 final SourceFileExceptionList sfl = new DefaultSourceFileExceptionList(e);
600  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_WEB_FAILED, sfl);
601  0 Trace.trace(CLASS, this, method, "Couldn't access " + prop.getUrl());
602  0 throw sfl;
603    } finally {
604  0 IoUtility.close(out);
605  0 IoUtility.close(in);
606  0 Trace.end(CLASS, this, method);
607    }
608    }
609   
610    /**
611    * Transform an URL address into a relative local file path. This might also change the file
612    * name. If the URL address is already a file address, the original file path is returned.
613    *
614    * @param address Transform this URL.
615    * @return Result of transformation.
616    */
 
617  25119 toggle public final File getLocalFilePath(final ModuleAddress address) {
618  25119 final String method = "localizeInFileSystem(URL)";
619  25119 if (address.isFileAddress()) {
620  25063 return new File(address.getURL().getFile());
621    }
622  56 final URL url = address.getURL();
623  56 Trace.param(CLASS, this, method, "protocol", url.getProtocol());
624  56 Trace.param(CLASS, this, method, "host", url.getHost());
625  56 Trace.param(CLASS, this, method, "port", url.getPort());
626  56 Trace.param(CLASS, this, method, "path", url.getPath());
627  56 Trace.param(CLASS, this, method, "file", url.getFile());
628  56 StringBuffer file = new StringBuffer(url.getFile());
629  56 StringUtility.replace(file, "_", "_1"); // remember all '_'
630  56 StringUtility.replace(file, "/", "_2"); // preserve all '/'
631  56 String encoded = file.toString(); // fallback file name
632  56 try {
633  56 encoded = URLEncoder.encode(file.toString(), "UTF-8");
634    } catch (UnsupportedEncodingException e) {
635    // should not occur
636  0 Trace.trace(DefaultModuleAddress.class, "localizeInFileSystem(String)", e);
637    }
638  56 file.setLength(0);
639  56 file.append(encoded);
640  56 StringUtility.replace(file, "#", "##"); // escape all '#'
641  56 StringUtility.replace(file, "_2", "#"); // from '/' into '#'
642  56 StringUtility.replace(file, "_1", "_"); // from '_' into '_'
643  56 StringBuffer adr = new StringBuffer(url.toExternalForm());
644  56 try {
645  56 adr = new StringBuffer(new URL(url.getProtocol(), url.getHost(), url.getPort(), file
646    .toString()).toExternalForm());
647    } catch (MalformedURLException e) {
648  0 Trace.fatal(CLASS, this, "localizeInFileSystem(URL)", "unexpected", e);
649  0 e.printStackTrace();
650    }
651    // escape characters:
652  56 StringUtility.replace(adr, "://", "_"); // before host
653  56 StringUtility.replace(adr, ":", "_"); // before protocol
654  56 return new File(getBufferDirectory(), adr.toString());
655    }
656   
657    /**
658    * Increment intern process counter.
659    */
 
660  362 toggle private synchronized void processInc() {
661  362 this.processCounter++;
662    }
663   
664    /**
665    * Decrement intern process counter.
666    */
 
667  362 toggle private synchronized void processDec() {
668  362 this.processCounter--;
669    }
670   
 
671  56 toggle public File getBufferDirectory() {
672  56 return kernel.getConfig().getBufferDirectory();
673    }
674   
 
675  0 toggle public File getGenerationDirectory() {
676  0 return kernel.getConfig().getGenerationDirectory();
677    }
678   
 
679  2 toggle public KernelQedeqBo getKernelQedeqBo(final ModuleAddress address) {
680  2 return getModules().getKernelQedeqBo(this, address);
681    }
682   
 
683  34 toggle public QedeqBo getQedeqBo(final ModuleAddress address) {
684  34 return getModules().getKernelQedeqBo(this, address);
685    }
686   
 
687  51 toggle public ModuleAddress getModuleAddress(final URL url) throws IOException {
688  51 return new DefaultModuleAddress(url);
689    }
690   
 
691  0 toggle public ModuleAddress getModuleAddress(final String url) throws IOException {
692  0 return new DefaultModuleAddress(url);
693    }
694   
 
695  2 toggle public ModuleAddress getModuleAddress(final File file) throws IOException {
696  2 return new DefaultModuleAddress(file);
697    }
698   
 
699  2 toggle public String getSource(final ModuleAddress address) throws IOException {
700  2 final KernelQedeqBo bo = getKernelQedeqBo(address);
701  2 if (bo.getLoadingState().equals(LoadingState.STATE_UNDEFINED)
702    || bo.getLoadingState().equals(LoadingState.STATE_LOADING_FROM_WEB)
703    || bo.getLoadingState().equals(LoadingState.STATE_LOADING_FROM_WEB_FAILED)) {
704  0 return null;
705    // TODO mime 20080313: remove me
706    // throw new IllegalStateException("module is not yet buffered " + address);
707    }
708  2 final StringBuffer buffer = new StringBuffer();
709  2 IoUtility.loadReader(getQedeqFileDao().getModuleReader(bo), buffer);
710  2 return buffer.toString();
711    }
712   
 
713  74 toggle public boolean checkModule(final ModuleAddress address) {
714   
715  74 final String method = "checkModule(ModuleAddress)";
716  74 final DefaultKernelQedeqBo prop = modules.getKernelQedeqBo(this, address);
717  74 try {
718  74 QedeqLog.getInstance().logRequest(
719    "Check logical correctness for \"" + prop.getUrl() + "\"");
720   
721  74 loadModule(address);
722  74 LoadRequiredModules.loadRequired(prop);
723   
724  74 QedeqBoFormalLogicChecker.check(prop);
725  66 QedeqLog.getInstance().logSuccessfulReply(
726    "Check of logical correctness successful for \"" + prop.getUrl() + "\"");
727    } catch (final SourceFileExceptionList e) {
728  8 final String msg = "Check of logical correctness failed for \"" + address.getURL()
729    + "\"";
730  8 QedeqLog.getInstance().logFailureReply(msg, e.getMessage());
731    } catch (final RuntimeException e) {
732  0 final String msg = "Check of logical correctness failed for \"" + address.getURL()
733    + "\"";
734  0 Trace.fatal(CLASS, this, method, msg, e);
735  0 final SourceFileExceptionList xl = new DefaultSourceFileExceptionList(e);
736    // TODO mime 20080124: every state must be able to change into
737    // a failure state, here we only assume three cases
738  0 if (!prop.isLoaded()) {
739  0 if (!prop.getLoadingState().isFailure()) {
740  0 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, xl);
741    }
742  0 } else if (!prop.hasLoadedRequiredModules()) {
743  0 if (!prop.getDependencyState().isFailure()) {
744  0 prop.setDependencyFailureState(
745    DependencyState.STATE_LOADING_REQUIRED_MODULES_FAILED, xl);
746    }
747    } else {
748  0 if (!prop.getLogicalState().isFailure()) {
749  0 prop.setLogicalFailureState(LogicalState.STATE_EXTERNAL_CHECKING_FAILED, xl);
750    }
751    }
752  0 QedeqLog.getInstance().logFailureReply(msg, e.toString());
753    }
754  74 if (validate) {
755  74 modules.validateDependencies();
756    }
757  74 return prop.isChecked();
758    }
759   
 
760  0 toggle public InputStream createLatex(final ModuleAddress address, final String language,
761    final String level) throws DefaultSourceFileExceptionList, IOException {
762  0 return Qedeq2Latex.createLatex(getKernelQedeqBo(address), language, level);
763    }
764   
 
765  0 toggle public String generateLatex(final ModuleAddress address, final String language,
766    final String level) throws DefaultSourceFileExceptionList, IOException {
767  0 return Qedeq2Latex.generateLatex(getKernelQedeqBo(address), language, level).toString();
768    }
769   
770    /**
771    * Get all loaded QEDEQ modules.
772    *
773    * @return All QEDEQ modules.
774    */
 
775  437 toggle private KernelQedeqBoStorage getModules() {
776  437 return modules;
777    }
778   
 
779  0 toggle private SourceFileExceptionList createSourceFileExceptionList(final IOException e) {
780  0 return new DefaultSourceFileExceptionList(e);
781    }
782   
 
783  1 toggle private SourceFileExceptionList createSourcelFileExceptionList(
784    final ModuleFileNotFoundException e) {
785  1 return new DefaultSourceFileExceptionList(new IOException(e.getMessage()));
786    }
787   
788    /**
789    * Get description of source file exception list.
790    *
791    * @param address Get description for this module exceptions.
792    * @return Error description and location.
793    */
 
794  0 toggle public String[] getSourceFileExceptionList(final ModuleAddress address) {
795  0 final List list = new ArrayList();
796  0 final KernelQedeqBo bo = getKernelQedeqBo(address);
797  0 final SourceFileExceptionList sfl = bo.getException();
798  0 if (sfl != null) {
799  0 final StringBuffer buffer = new StringBuffer();
800  0 do {
801  0 try {
802  0 IoUtility.loadReader(getQedeqFileDao().getModuleReader(bo), buffer);
803    } catch (IOException e) {
804  0 for (int i = 0; i < sfl.size(); i++) {
805  0 list.add(sfl.get(i).getDescription());
806    }
807  0 break; // out of do while
808    }
809  0 final TextInput input = new TextInput(buffer);
810  0 input.setPosition(0);
811  0 final StringBuffer buf = new StringBuffer();
812  0 for (int i = 0; i < sfl.size(); i++) {
813  0 buf.setLength(0);
814  0 final SourceFileException sf = sfl.get(i);
815  0 buf.append(sf.getDescription());
816  0 try {
817  0 if (sf.getSourceArea() != null
818    && sf.getSourceArea().getStartPosition() != null) {
819  0 buf.append("\n");
820  0 input.setRow(sf.getSourceArea().getStartPosition().getLine());
821  0 buf.append(StringUtility.replace(input.getLine(), "\t", " "));
822  0 buf.append("\n");
823  0 final StringBuffer whitespace = StringUtility.getSpaces(sf
824    .getSourceArea().getStartPosition().getColumn() - 1);
825  0 buffer.append(whitespace);
826  0 buffer.append("^");
827    }
828    } catch (Exception e) {
829  0 Trace.trace(CLASS, this, "getSourceFileExceptionList(ModuleAddress)", e);
830    }
831  0 list.add(buf.toString());
832    }
833  0 break; // out of do while
834    } while (true);
835    }
836  0 return (String[]) list.toArray(new String[] {});
837    }
838   
 
839  222 toggle public QedeqFileDao getQedeqFileDao() {
840  222 return qedeqFileDao;
841    }
842   
843    }