1 /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2 *
3 * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>.
4 *
5 * "Hilbert II" is free software; you can redistribute
6 * it and/or modify it under the terms of the GNU General Public
7 * License as published by the Free Software Foundation; either
8 * version 2 of the License, or (at your option) any later version.
9 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 */
15
16 package org.qedeq.kernel.bo.common;
17
18 import java.io.File;
19 import java.io.IOException;
20 import java.net.URL;
21
22 import org.qedeq.kernel.se.common.ModuleAddress;
23 import org.qedeq.kernel.se.common.ModuleService;
24 import org.qedeq.kernel.se.visitor.InterruptException;
25
26 /**
27 * The main QEDEQ kernel methods are assembled here.
28 *
29 * @author Michael Meyling
30 */
31 public interface KernelServices {
32
33 /**
34 * Remove all modules from memory.
35 *
36 * @return Was removal successful?
37 */
38 public boolean removeAllModules();
39
40 /**
41 * Clear local buffer and all loaded QEDEQ modules.
42 *
43 * @return Was deletion successful?
44 */
45 public boolean clearLocalBuffer();
46
47 /**
48 * Get a certain module. You can check the status to know if the loading was successful.
49 *
50 * @param address Address of module.
51 * @return Wanted module.
52 */
53 public QedeqBo loadModule(ModuleAddress address);
54
55 /**
56 * Get required modules of given module. You can check the status to know if the loading was
57 * successful.
58 *
59 * @param address Address of module.
60 * @return Successful loading.
61 */
62 public boolean loadRequiredModules(ModuleAddress address);
63
64 /**
65 * Load all QEDEQ modules from project web directory for current kernel.
66 *
67 * @return Successful loading.
68 */
69 public boolean loadAllModulesFromQedeq();
70
71 /**
72 * Remove a QEDEQ module from memory.
73 *
74 * @param address Remove module identified by this address.
75 */
76 public void removeModule(ModuleAddress address);
77
78 /**
79 * Get list of all currently loaded QEDEQ modules.
80 *
81 * @return All currently loaded QEDEQ modules.
82 */
83 public ModuleAddress[] getAllLoadedModules();
84
85 /**
86 * Get {@link QedeqBo} for an address.
87 *
88 * @param address Look for this address.
89 * @return Existing or new {@link QedeqBo}.
90 */
91 public QedeqBo getQedeqBo(ModuleAddress address);
92
93 /**
94 * Get source of an QEDEQ module.
95 * If the module was not yet not buffered <code>null</code> is returned.
96 *
97 * @param address Address for QEDEQ module address.
98 * @return Contents of locally buffered QEDEQ module.
99 * @throws IOException Loading failed.
100 */
101 public String getSource(ModuleAddress address) throws IOException;
102
103 /**
104 * Get module address from URL.
105 *
106 * @param url URL for QEDEQ module.
107 * @return Module address.
108 * @throws IOException URL has not the correct format for referencing a QEDEQ module.
109 */
110 public ModuleAddress getModuleAddress(URL url) throws IOException;
111
112 /**
113 * Get module address from URL.
114 *
115 * @param url URL for QEDEQ module.
116 * @return Module address.
117 * @throws IOException URL has not the correct format for referencing a QEDEQ module.
118 */
119 public ModuleAddress getModuleAddress(String url) throws IOException;
120
121 /**
122 * Get module address from URL.
123 *
124 * @param file Local QEDEQ module.
125 * @return Module address.
126 * @throws IOException URL has not the correct format for referencing a QEDEQ module.
127 */
128 public ModuleAddress getModuleAddress(File file) throws IOException;
129
130 /**
131 * Check if all formulas of a QEDEQ module and its required modules are well formed.
132 *
133 * @param address Module to check.
134 * @return Was check successful?
135 */
136 public boolean checkWellFormedness(ModuleAddress address);
137
138 /**
139 * Check if all propositions of this and all required modules have correct formal proofs.
140 *
141 * @param address Module to check.
142 * @return Was check successful?
143 */
144 public boolean checkFormallyProved(ModuleAddress address);
145
146 /**
147 * Get all installed plugins.
148 *
149 * @return Installed plugins.
150 */
151 public ModuleService[] getPlugins();
152
153 /**
154 * Execute plugin on given QEDEQ module.
155 *
156 * @param id Plugin id.
157 * @param address QEDEQ module address.
158 * @param data Process data. Additional data beside module.
159 * @throws InterruptException User canceled further processing.
160 * @return Plugin specific resulting object. Might be <code>null</code>.
161 */
162 public Object executePlugin(final String id, final ModuleAddress address, final Object data)
163 throws InterruptException;
164
165 /**
166 * Clear all plugin warnings and errors for given module.
167 *
168 * @param address QEDEQ module address.
169 */
170 public void clearAllPluginResults(final ModuleAddress address);
171
172 /**
173 * Get information about all service processes.
174 *
175 * @return Result.
176 */
177 public ServiceJob[] getServiceProcesses();
178
179 /**
180 * Get all running service processes. But remember a running process might currently
181 * be blocked.
182 *
183 * @return All service running processes.
184 */
185 public ServiceJob[] getRunningServiceProcesses();
186
187 /**
188 * Stop all currently running service executions.
189 */
190 public void terminateAllServiceProcesses();
191
192 }