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.common;
017
018 import java.io.File;
019 import java.io.IOException;
020 import java.net.URL;
021
022 import org.qedeq.kernel.se.common.ModuleAddress;
023 import org.qedeq.kernel.se.common.Plugin;
024
025 /**
026 * The main QEDEQ kernel methods are assembled here.
027 *
028 * @author Michael Meyling
029 */
030 public interface KernelServices {
031
032 /**
033 * Remove all modules from memory.
034 */
035 public void removeAllModules();
036
037 /**
038 * Clear local buffer and all loaded QEDEQ modules.
039 *
040 * @return Was deletion successful?
041 */
042 public boolean clearLocalBuffer();
043
044 /**
045 * Get a certain module. You can check the status to know if the loading was successful.
046 *
047 * @param address Address of module.
048 * @return Wanted module.
049 */
050 public QedeqBo loadModule(ModuleAddress address);
051
052 /**
053 * Get required modules of given module. You can check the status to know if the loading was
054 * successful.
055 *
056 * @param address Address of module.
057 * @return Successful loading.
058 */
059 public boolean loadRequiredModules(ModuleAddress address);
060
061 /**
062 * Load all QEDEQ modules from project web directory for current kernel.
063 *
064 * @return Successful loading.
065 */
066 public boolean loadAllModulesFromQedeq();
067
068 /**
069 * Remove a certain module.
070 *
071 * @param address Address of module.
072 */
073 public void removeModule(ModuleAddress address);
074
075 /**
076 * Get list of all currently loaded QEDEQ modules.
077 *
078 * @return All currently loaded QEDEQ modules.
079 */
080 public ModuleAddress[] getAllLoadedModules();
081
082 /**
083 * Get {@link QedeqBo} for an address.
084 *
085 * @param address Look for this address.
086 * @return Existing or new {@link QedeqBo}.
087 */
088 public QedeqBo getQedeqBo(ModuleAddress address);
089
090 /**
091 * Get source of an QEDEQ module.
092 * If the module was not yet not buffered <code>null</code> is returned.
093 *
094 * @param address Address for QEDEQ module address.
095 * @return Contents of locally buffered QEDEQ module.
096 * @throws IOException Loading failed.
097 */
098 public String getSource(ModuleAddress address) throws IOException;
099
100 /**
101 * Get module address from URL.
102 *
103 * @param url URL for QEDEQ module.
104 * @return Module address.
105 * @throws IOException URL has not the correct format for referencing a QEDEQ module.
106 */
107 public ModuleAddress getModuleAddress(URL url) throws IOException;
108
109 /**
110 * Get module address from URL.
111 *
112 * @param url URL for QEDEQ module.
113 * @return Module address.
114 * @throws IOException URL has not the correct format for referencing a QEDEQ module.
115 */
116 public ModuleAddress getModuleAddress(String url) throws IOException;
117
118 /**
119 * Get module address from URL.
120 *
121 * @param file Local QEDEQ module.
122 * @return Module address.
123 * @throws IOException URL has not the correct format for referencing a QEDEQ module.
124 */
125 public ModuleAddress getModuleAddress(File file) throws IOException;
126
127 /**
128 * Check if all formulas of a QEDEQ module and its required modules are well formed.
129 *
130 * @param address Module to check.
131 * @return Was check successful?
132 */
133 public boolean checkWellFormedness(ModuleAddress address);
134
135 /**
136 * Check if all propositions of this and all required modules have correct formal proofs.
137 *
138 * @param address Module to check.
139 * @return Was check successful?
140 */
141 public boolean checkFormallyProved(ModuleAddress address);
142
143 /**
144 * Get all installed plugins.
145 *
146 * @return Installed plugins.
147 */
148 public Plugin[] getPlugins();
149
150 /**
151 * Execute plugin on given QEDEQ module.
152 *
153 * @param id Plugin id.
154 * @param address QEDEQ module address.
155 * @param data Process data. Additional data beside module.
156 * @return Plugin specific resulting object. Might be <code>null</code>.
157 */
158 public Object executePlugin(final String id, final ModuleAddress address, final Object data);
159
160 /**
161 * Clear all plugin warnings and errors for given module.
162 *
163 * @param address QEDEQ module address.
164 */
165 public void clearAllPluginResults(final ModuleAddress address);
166
167 /**
168 * Get information about all service processes.
169 *
170 * @return Result.
171 */
172 public ServiceProcess[] getServiceProcesses();
173
174 /**
175 * Get all running service processes. But remember a running process might currently
176 * be blocked.
177 *
178 * @return All service running processes.
179 */
180 public ServiceProcess[] getRunningServiceProcesses();
181
182 /**
183 * Stop all currently running plugin executions.
184 */
185 public void stopAllPluginExecutions();
186
187 }
|