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.kernel.bo.service;
017
018 import java.util.ArrayList;
019 import java.util.List;
020
021 import org.apache.commons.lang.ArrayUtils;
022 import org.qedeq.base.io.SourceArea;
023 import org.qedeq.base.trace.Trace;
024 import org.qedeq.base.utility.EqualsUtility;
025 import org.qedeq.base.utility.StringUtility;
026 import org.qedeq.kernel.bo.common.Element2Latex;
027 import org.qedeq.kernel.bo.common.Element2Utf8;
028 import org.qedeq.kernel.bo.common.ModuleReferenceList;
029 import org.qedeq.kernel.bo.module.InternalKernelServices;
030 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
031 import org.qedeq.kernel.bo.module.KernelQedeqBo;
032 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
033 import org.qedeq.kernel.bo.module.ModuleLabels;
034 import org.qedeq.kernel.bo.module.QedeqFileDao;
035 import org.qedeq.kernel.se.base.module.LatexList;
036 import org.qedeq.kernel.se.base.module.Qedeq;
037 import org.qedeq.kernel.se.common.ModuleAddress;
038 import org.qedeq.kernel.se.common.ModuleContext;
039 import org.qedeq.kernel.se.common.ModuleDataException;
040 import org.qedeq.kernel.se.common.Plugin;
041 import org.qedeq.kernel.se.common.SourceFileException;
042 import org.qedeq.kernel.se.common.SourceFileExceptionList;
043 import org.qedeq.kernel.se.dto.module.QedeqVo;
044 import org.qedeq.kernel.se.state.AbstractState;
045 import org.qedeq.kernel.se.state.DependencyState;
046 import org.qedeq.kernel.se.state.FormallyProvedState;
047 import org.qedeq.kernel.se.state.LoadingImportsState;
048 import org.qedeq.kernel.se.state.LoadingState;
049 import org.qedeq.kernel.se.state.WellFormedState;
050
051
052 /**
053 * Represents a module and its states. This is a kernel intern representation.
054 *
055 * @author Michael Meyling
056 */
057 public class DefaultKernelQedeqBo implements KernelQedeqBo {
058
059 /** This class. */
060 private static final Class CLASS = DefaultKernelQedeqBo.class;
061
062 /** Internal kernel services. */
063 private final InternalKernelServices services;
064
065 /** Address and module specification. */
066 private final ModuleAddress address;
067
068 /** Loaded QEDEQ module. */
069 private QedeqVo qedeq;
070
071 /** Required QEDEQ modules. */
072 private KernelModuleReferenceList required;
073
074 /** Dependent QEDEQ modules. */
075 private KernelModuleReferenceList dependent;
076
077 /** Predicate and function constant existence checker. */
078 private ModuleConstantsExistenceChecker checker;
079
080 /** Labels for this module, definitions, etc. */
081 private ModuleLabels labels;
082
083 /** Can map elements to LaTeX. */
084 private Element2Latex converter;
085
086 /** Can map elements to UTF-8 text. */
087 private Element2Utf8 textConverter;
088
089 /** Loader used for loading this object. */
090 private QedeqFileDao loader;
091
092 /** State change manager. */
093 private final StateManager stateManager;
094
095 /**
096 * Creates new module properties.
097 *
098 * @param services Internal kernel services.
099 * @param address Module address (not <code>null</code>).
100 * @throws NullPointerException <code>address</code> is null.
101 */
102 public DefaultKernelQedeqBo(final InternalKernelServices services,
103 final ModuleAddress address) {
104 this.services = services;
105 this.address = address;
106 if (address == null) {
107 throw new NullPointerException("ModuleAddress must not be null");
108 }
109 required = new KernelModuleReferenceList();
110 dependent = new KernelModuleReferenceList();
111 stateManager = new StateManager(this);
112 }
113
114 /**
115 * Set loader used for loading this object.
116 *
117 * @param loader Responsible loader.
118 */
119 public void setQedeqFileDao(final QedeqFileDao loader) {
120 this.loader = loader;
121 }
122
123 /**
124 * Get loader used to load this object.
125 *
126 * @return Loader.
127 */
128 public QedeqFileDao getLoader() {
129 return this.loader;
130 }
131
132 public boolean hasBasicFailures() {
133 return stateManager.hasBasicFailures();
134 }
135
136 public boolean hasErrors() {
137 return stateManager.hasErrors();
138 }
139
140 public boolean hasWarnings() {
141 return stateManager.hasWarnings();
142 }
143
144 public ModuleAddress getModuleAddress() {
145 return address;
146 }
147
148 /**
149 * Get internal kernel services.
150 *
151 * @return Internal kernel services.
152 */
153 public InternalKernelServices getKernelServices() {
154 return this.services;
155 }
156
157 /**
158 * Set completeness percentage.
159 *
160 * @param completeness Completeness of loading into memory.
161 */
162 public void setLoadingCompleteness(final int completeness) {
163 stateManager.setLoadingCompleteness(completeness);
164 }
165
166 public int getLoadingCompleteness() {
167 return stateManager.getLoadingCompleteness();
168 }
169
170 /**
171 * Delete QEDEQ module. Invalidates all dependent modules.
172 */
173 public void delete() {
174 stateManager.delete();
175 }
176
177 /**
178 * Set loading progress module state.
179 *
180 * @param plugin Plugin that sets the state.
181 * @param state Module loading state. Must not be <code>null</code>.
182 * @throws IllegalStateException State is a failure state or module loaded state.
183 */
184 public void setLoadingProgressState(final Plugin plugin, final LoadingState state) {
185 stateManager.setLoadingProgressState(plugin, state);
186 }
187
188 /**
189 * Set failure module state.
190 *
191 * @param state Module loading state. Must not be <code>null</code>.
192 * @param e Exception that occurred during loading. Must not be <code>null</code>.
193 * @throws IllegalArgumentException <code>state</code> is no failure state
194 */
195 public void setLoadingFailureState(final LoadingState state,
196 final SourceFileExceptionList e) {
197 stateManager.setLoadingFailureState(state, e);
198 }
199
200 public LoadingState getLoadingState() {
201 return stateManager.getLoadingState();
202 }
203
204 public boolean isLoaded() {
205 return stateManager.isLoaded();
206 }
207
208 /**
209 * Set loading state to "loaded". Also puts <code>null</code> to {@link #getLabels()}.
210 *
211 * @param qedeq This module was loaded. Must not be <code>null</code>.
212 * @param labels Module labels.
213 * @param converter Can convert elements into LaTeX. Must not be <code>null</code>.
214 * @param textConverter Can convert elements into UTF-8 text. Must not be <code>null</code>.
215 * @throws NullPointerException One argument was <code>null</code>.
216 */
217 public void setLoaded(final QedeqVo qedeq, final ModuleLabels labels,
218 final Element2Latex converter, final Element2Utf8 textConverter) {
219 stateManager.setLoaded(qedeq, labels);
220 this.converter = converter;
221 this.textConverter = textConverter;
222 }
223
224 public Qedeq getQedeq() {
225 return this.qedeq;
226 }
227
228 public Element2Latex getElement2Latex() {
229 return this.converter;
230 }
231
232 public Element2Utf8 getElement2Utf8() {
233 return this.textConverter;
234 }
235
236 public void setLoadingImportsProgressState(final Plugin plugin, final LoadingImportsState state) {
237 stateManager.setLoadingImportsProgressState(plugin, state);
238 }
239
240 public void setLoadingImportsFailureState(final LoadingImportsState state,
241 final SourceFileExceptionList e) {
242 stateManager.setLoadingImportsFailureState(state, e);
243 }
244
245 public LoadingImportsState getLoadingImportsState() {
246 return stateManager.getLoadingImportsState();
247 }
248
249 public void setLoadedImports(final KernelModuleReferenceList list) {
250 stateManager.setLoadedImports(list);
251 }
252
253 public boolean hasLoadedImports() {
254 return stateManager.hasLoadedImports();
255 }
256
257
258 public void setDependencyProgressState(final Plugin plugin, final DependencyState state) {
259 stateManager.setDependencyProgressState(plugin, state);
260 }
261
262 public void setDependencyFailureState(final DependencyState state,
263 final SourceFileExceptionList e) {
264 stateManager.setDependencyFailureState(state, e);
265 }
266
267 public DependencyState getDependencyState() {
268 return stateManager.getDependencyState();
269 }
270
271 public void setLoadedRequiredModules() {
272 stateManager.setLoadedRequiredModules();
273 }
274
275 public ModuleReferenceList getRequiredModules() {
276 return getKernelRequiredModules();
277 }
278
279 public KernelModuleReferenceList getKernelRequiredModules() {
280 return required;
281 }
282
283 public boolean hasLoadedRequiredModules() {
284 return stateManager.hasLoadedRequiredModules();
285 }
286
287 /**
288 * Get labels and URLs of all directly dependent modules.
289 *
290 * @return URLs of all referenced modules.
291 */
292 public KernelModuleReferenceList getDependentModules() {
293 return dependent;
294 }
295
296 public void setWellFormed(final ModuleConstantsExistenceChecker checker) {
297 stateManager.setWellFormed(checker);
298 }
299
300 public boolean isWellFormed() {
301 return stateManager.isWellFormed();
302 }
303
304 public boolean isFullyFormallyProved() {
305 return stateManager.isFullyFormallyProved();
306 }
307
308 public void setWellFormedProgressState(final Plugin plugin, final WellFormedState state) {
309 stateManager.setWellFormedProgressState(plugin, state);
310 }
311
312 public void setWellfFormedFailureState(final WellFormedState state,
313 final SourceFileExceptionList e) {
314 stateManager.setWellFormedFailureState(state, e);
315 }
316
317 public WellFormedState getWellFormedState() {
318 return stateManager.getWellFormedState();
319 }
320
321 public void setFormallyProvedProgressState(final Plugin plugin, final FormallyProvedState state) {
322 stateManager.setFormallyProvedProgressState(plugin, state);
323 }
324
325 public void setFormallyProvedFailureState(final FormallyProvedState state,
326 final SourceFileExceptionList e) {
327 stateManager.setFormallyProvedFailureState(state, e);
328 }
329
330 public FormallyProvedState getFormallyProvedState() {
331 return stateManager.getFormallyProvedState();
332 }
333
334 public SourceFileExceptionList getErrors() {
335 return stateManager.getErrors();
336 }
337
338 public SourceFileExceptionList getWarnings() {
339 return stateManager.getWarnings();
340 }
341
342 public String getStateDescription() {
343 return stateManager.getStateDescription();
344 }
345
346 public AbstractState getCurrentState() {
347 return stateManager.getCurrentState();
348 }
349
350 public AbstractState getLastSuccessfulState() {
351 return stateManager.getLastSuccesfulState();
352 }
353
354 public Plugin getCurrentlyRunningPlugin() {
355 return stateManager.getCurrentlyRunningPlugin();
356 }
357
358 public void setCurrentlyRunningPlugin(final Plugin currentlyRunningPlugin) {
359 stateManager.setCurrentlyRunningPlugin(currentlyRunningPlugin);
360 }
361
362 public String getName() {
363 if (address == null) {
364 return "null";
365 }
366 return address.getName();
367 }
368
369 public String getRuleVersion() {
370 if (address == null || qedeq == null
371 || qedeq.getHeader() == null
372 || qedeq.getHeader().getSpecification() == null
373 || qedeq.getHeader().getSpecification().getRuleVersion() == null) {
374 return "";
375 }
376 return qedeq.getHeader().getSpecification().getRuleVersion();
377 }
378
379 public String getUrl() {
380 if (this.address == null) {
381 return null;
382 }
383 return this.address.getUrl();
384 }
385
386 /**
387 * Set label references for QEDEQ module.
388 *
389 * @param labels Label references.
390 */
391 public void setLabels(final ModuleLabels labels) {
392 this.labels = labels;
393 }
394
395 public ModuleLabels getLabels() {
396 return labels;
397 }
398
399 /**
400 * Create exception out of {@link ModuleDataException}.
401 *
402 * @param plugin This plugin generated the error.
403 * @param exception Take this exception.
404 * @return Newly created instance.
405 */
406 public SourceFileExceptionList createSourceFileExceptionList(final Plugin plugin,
407 final ModuleDataException exception) {
408 SourceArea referenceArea = null;
409 if (exception.getReferenceContext() != null) {
410 referenceArea = createSourceArea(qedeq, exception.getReferenceContext());
411 }
412 final SourceFileException e = new SourceFileException(plugin, exception,
413 createSourceArea(qedeq, exception.getContext()), referenceArea);
414 final SourceFileExceptionList list = new SourceFileExceptionList(e);
415 return list;
416 }
417
418 /**
419 * Create exception out of {@link ModuleDataException}.
420 *
421 * @param plugin This plugin generated the error.
422 * @param exception Take this exception.
423 * @param qedeq Take this QEDEQ source. (This might not be accessible via
424 * {@link #getQedeq()}.
425 * @return Newly created instance.
426 */
427 public SourceFileExceptionList createSourceFileExceptionList(final Plugin plugin,
428 final ModuleDataException exception, final Qedeq qedeq) {
429 final SourceFileException e = new SourceFileException(plugin, exception,
430 createSourceArea(qedeq, exception.getContext()), createSourceArea(qedeq,
431 exception.getReferenceContext()));
432 final SourceFileExceptionList list = new SourceFileExceptionList(e);
433 return list;
434 }
435
436 public SourceFileException createSourceFileException(final Plugin plugin, final ModuleDataException
437 exception) {
438 final SourceArea area = createSourceArea(qedeq, exception.getContext());
439 SourceArea referenceArea = null;
440 if (exception.getReferenceContext() != null) {
441 referenceArea = createSourceArea(qedeq, exception.getReferenceContext());
442 }
443 final SourceFileException e = new SourceFileException(plugin, exception, area, referenceArea);
444 return e;
445 }
446
447 /**
448 * Create area in source file for QEDEQ module context.
449 * If the system property "qedeq.test.xmlLocationFailures" is set to "true" a runtime
450 * exception is thrown if the context is not found.
451 *
452 * @param qedeq Look at this QEDEQ module.
453 * @param context Search for this context.
454 * @return Created file area. Maybe <code>null</code>.
455 */
456 public SourceArea createSourceArea(final Qedeq qedeq, final ModuleContext context) {
457 final String method = "createSourceArea(Qedeq, ModuleContext)";
458 SourceArea area = null;
459 try {
460 area = loader.createSourceArea(qedeq, context);
461 } catch (RuntimeException e) {
462 Trace.fatal(CLASS, method, "loader couldn't create context: " + context, e);
463 if (Boolean.TRUE.toString().equalsIgnoreCase(
464 System.getProperty("qedeq.test.xmlLocationFailures"))) {
465 throw e;
466 }
467 }
468 if (area == null) {
469 Trace.fatal(CLASS, "createSourceArea", "loader coudn't create context: "
470 + context, new NullPointerException());
471 area = new SourceArea(this.getModuleAddress().getUrl());
472 }
473 return area;
474 }
475
476 public String[] getSupportedLanguages() {
477 // TODO m31 20070704: there should be a better way to
478 // get all supported languages. Time for a new visitor?
479 if (!isLoaded() || getQedeq() == null || getQedeq().getHeader() == null
480 || getQedeq().getHeader().getTitle() == null) {
481 return ArrayUtils.EMPTY_STRING_ARRAY;
482 }
483 final LatexList list = getQedeq().getHeader().getTitle();
484 final List result = new ArrayList(list.size());
485 for (int i = 0; i < list.size(); i++) {
486 if (null != list.get(i) && list.get(i).getLanguage() != null
487 && list.get(i).getLanguage().trim().length() > 0) {
488 result.add(list.get(i).getLanguage());
489 }
490 }
491 return (String[]) result.toArray(ArrayUtils.EMPTY_STRING_ARRAY);
492 }
493
494 public boolean isSupportedLanguage(final String language) {
495 return StringUtility.isIn(language, getSupportedLanguages());
496 }
497
498 public String getOriginalLanguage() {
499 // TODO 20110316 m31: rework qedeq.xsd to have a default language
500 final String[] supported = getSupportedLanguages();
501 if (StringUtility.isNotIn("de", supported)) {
502 if (supported.length == 0) {
503 return "en"; // we have no German only documents
504 }
505 return supported[0];
506 }
507 return "de";
508 }
509
510
511 /**
512 * Set {@link QedeqVo}. Doesn't do any status handling. Only for internal use.
513 *
514 * @param qedeq Set this value.
515 */
516 public void setQedeqVo(final QedeqVo qedeq) {
517 this.qedeq = qedeq;
518 }
519
520 /**
521 * Get {@link StateManager}. Only for internal use.
522 *
523 * @return StateManager
524 */
525 protected StateManager getStateManager() {
526 return this.stateManager;
527 }
528
529 /**
530 * Get the predicate and function existence checker. Is not <code>null</code>
531 * if logic was (not necessarily successfully) checked.
532 *
533 * @return Checker. Checks if a predicate or function constant is defined.
534 */
535 public ModuleConstantsExistenceChecker getExistenceChecker() {
536 return checker;
537 }
538
539 public void setExistenceChecker(final ModuleConstantsExistenceChecker checker) {
540 this.checker = checker;
541 }
542
543 public int hashCode() {
544 return (getModuleAddress() == null ? 0 : getModuleAddress().hashCode());
545 }
546
547 public boolean equals(final Object obj) {
548 if (obj instanceof DefaultKernelQedeqBo) {
549 return EqualsUtility.equals(((DefaultKernelQedeqBo) obj).getModuleAddress(),
550 this.getModuleAddress());
551 }
552 return false;
553 }
554
555 public String toString() {
556 return address.getUrl();
557 }
558
559 public void addPluginErrorsAndWarnings(final Plugin plugin, final SourceFileExceptionList errors,
560 final SourceFileExceptionList warnings) {
561 stateManager.addPluginResults(plugin, errors, warnings);
562 }
563
564 public void clearAllPluginErrorsAndWarnings() {
565 stateManager.removeAllPluginResults();
566 }
567
568 }
|