001 package org.qedeq.kernel.bo.module;
002
003 import org.qedeq.kernel.bo.common.Element2Latex;
004 import org.qedeq.kernel.bo.common.Element2Utf8;
005 import org.qedeq.kernel.bo.common.QedeqBo;
006 import org.qedeq.kernel.se.common.ModuleDataException;
007 import org.qedeq.kernel.se.common.Plugin;
008 import org.qedeq.kernel.se.common.SourceFileException;
009 import org.qedeq.kernel.se.common.SourceFileExceptionList;
010 import org.qedeq.kernel.se.state.DependencyState;
011 import org.qedeq.kernel.se.state.FormallyProvedState;
012 import org.qedeq.kernel.se.state.LoadingImportsState;
013 import org.qedeq.kernel.se.state.WellFormedState;
014
015 /**
016 * Kernel internal QedeqBo with additional methods.
017 *
018 * @author Michael Meyling
019 */
020 public interface KernelQedeqBo extends QedeqBo {
021
022 /**
023 * Get internal kernel services.
024 *
025 * @return Internal kernel services.
026 */
027 public InternalKernelServices getKernelServices();
028
029 /**
030 * Get labels and URLs of all referenced modules.
031 *
032 * @return URLs of all referenced modules.
033 */
034 public KernelModuleReferenceList getKernelRequiredModules();
035
036 /**
037 * Get label references for QEDEQ module.
038 *
039 * @return Label references.
040 */
041 public ModuleLabels getLabels();
042
043 /**
044 * Return mapper for transforming elements into LaTeX.
045 *
046 * @return Transformer to get LaTeX out of elements.
047 */
048 public Element2Latex getElement2Latex();
049
050 /**
051 * Return mapper for transforming elements into UTF-8 text.
052 *
053 * @return Transformer to get UTF-8 text out of elements.
054 */
055 public Element2Utf8 getElement2Utf8();
056
057 /**
058 * Create exception out of {@link ModuleDataException}.
059 *
060 * @param plugin This plugin generated the error.
061 * @param exception Take this exception.
062 * @return Newly created instance.
063 */
064 public SourceFileException createSourceFileException(Plugin plugin, ModuleDataException
065 exception);
066
067 /**
068 * Add errors and warnings for plugin.
069 *
070 * @param plugin Add errors for this plugin.
071 * @param errors These errors occurred.
072 * @param warnings These warnings occurred.
073 */
074 public void addPluginErrorsAndWarnings(Plugin plugin, SourceFileExceptionList errors,
075 SourceFileExceptionList warnings);
076
077 /**
078 * Remove all errors and warnings for all plugins.
079 */
080 public void clearAllPluginErrorsAndWarnings();
081
082 /**
083 * Get the predicate and function existence checker. Is only not <code>null</code>
084 * if logic was successfully checked.
085 *
086 * @return Checker. Checks if a predicate or function constant is defined.
087 */
088 public ModuleConstantsExistenceChecker getExistenceChecker();
089
090 /**
091 * Set failure module state.
092 *
093 * @param loadImportsFailed Module state.
094 * @param sfl Exception that occurred during loading required modules.
095 * @throws IllegalArgumentException <code>state</code> is no failure state
096 */
097 public void setLoadingImportsFailureState(LoadingImportsState loadImportsFailed,
098 SourceFileExceptionList sfl);
099
100 /**
101 * Set logical well formed module state. Must not be <code>null</code>.
102 *
103 * @param plugin Plugin that was executed.
104 * @param stateLoadImports module state
105 */
106 public void setLoadingImportsProgressState(Plugin plugin, LoadingImportsState stateLoadImports);
107
108 /**
109 * Set loaded imports state.
110 *
111 * @param imports These imports were loaded.
112 * @throws IllegalStateException Module is not yet loaded.
113 */
114 public void setLoadedImports(final KernelModuleReferenceList imports);
115
116 /**
117 * Set dependency failure module state.
118 *
119 * @param loadRequiredFailed Module state.
120 * @param sfl Exception that occurred during loading required modules.
121 * @throws IllegalArgumentException <code>loadRequiredFailed</code> is no failure state
122 * @throws IllegalStateException Module is not yet loaded.
123 * @throws NullPointerException <code>loadRequiredFailed</code> is <code>null</code>.
124 */
125 public void setDependencyFailureState(DependencyState loadRequiredFailed,
126 SourceFileExceptionList sfl);
127
128 /**
129 * Set dependency module state. Must not be <code>null</code>.
130 *
131 * @param plugin Plugin that was executed.
132 * @param state Module state
133 * @throws IllegalStateException Module is not yet loaded.
134 * @throws IllegalArgumentException <code>state</code> is failure state or loaded required
135 * state.
136 * @throws NullPointerException <code>state</code> is <code>null</code>.
137 */
138 public void setDependencyProgressState(Plugin plugin, DependencyState state);
139
140 /**
141 * Set loaded required requirements state.
142 *
143 * @throws IllegalStateException Module is not yet loaded.
144 */
145 public void setLoadedRequiredModules();
146
147 /**
148 * Set failure module state.
149 *
150 * @param stateExternalCheckingFailed Module state.
151 * @param sfl Exception that occurred during loading.
152 * @throws IllegalArgumentException <code>state</code> is no failure state
153 */
154 public void setWellfFormedFailureState(WellFormedState stateExternalCheckingFailed,
155 SourceFileExceptionList sfl);
156
157 /**
158 * Set logical well formed module state. Must not be <code>null</code>.
159 *
160 * @param plugin Plugin that was executed.
161 * @param stateInternalChecking module state
162 */
163 public void setWellFormedProgressState(Plugin plugin, WellFormedState stateInternalChecking);
164
165 /**
166 * Set logical formally proved module progress state. Must not be <code>null</code>.
167 *
168 * @param plugin Plugin that was executed.
169 * @param state module state
170 * @throws IllegalArgumentException <code>state</code> is no failure state
171 */
172 public void setFormallyProvedProgressState(Plugin plugin, FormallyProvedState state);
173
174 /**
175 * Set logical formally proved module failure state. Must not be <code>null</code>.
176 *
177 * @param state module state
178 * @param sfl Exception that occurred during loading.
179 * @throws IllegalArgumentException <code>state</code> is no failure state
180 */
181 public void setFormallyProvedFailureState(FormallyProvedState state,
182 SourceFileExceptionList sfl);
183
184 /**
185 * Set {@link ModuleConstantsExistenceChecker}. Doesn't do any status handling.
186 *
187 * @param existence Set this checker.
188 */
189 public void setExistenceChecker(ModuleConstantsExistenceChecker existence);
190
191 /**
192 * Set logic well formed state. Also set the predicate and function existence checker.
193 *
194 * @param checker Checks if a predicate or function constant is defined.
195 */
196 public void setWellFormed(ModuleConstantsExistenceChecker checker);
197
198
199 /**
200 * Set currently running plugin.
201 *
202 * @param plugin Set currently running plugin. Might be <code>null</code>.
203 */
204 public void setCurrentlyRunningPlugin(Plugin plugin);
205
206 }
|