org.qedeq.kernel.bo.module
Interface InternalKernelServices

All Superinterfaces:

KernelProperties

All Known Implementing Classes:

DefaultInternalKernelServices

public interface InternalKernelServices
extends KernelProperties

The kernel internal service methods are assembled here. Needed by the kernel and its helpers.

Author:

Michael Meyling

Method Summary

boolean	checkFormallyProved(InternalServiceJob process, KernelQedeqBo qedeq) Check if all propositions of this and all required modules have correct formal proofs.
boolean	checkWellFormedness(InternalServiceJob process, KernelQedeqBo qedeq) Check if all formulas of a QEDEQ module and its required modules are well formed.
SourceFileExceptionList	createSourceFileExceptionList(int code, java.lang.String message, java.lang.String address, java.lang.Exception e) Creates a list with a SourceFileException with dummy position.
SourceFileExceptionList	createSourceFileExceptionList(int code, java.lang.String message, java.lang.String address, java.io.IOException e) Creates a list with a SourceFileException with dummy position.
SourceFileExceptionList	createSourceFileExceptionList(int code, java.lang.String message, java.lang.String address, java.lang.RuntimeException e) Creates a list with a SourceFileException with dummy position.
java.lang.Object	executePlugin(InternalServiceJob parent, java.lang.String id, KernelQedeqBo qedeq, java.lang.Object data) Execute plugin on given QEDEQ module.
java.io.File	getBufferDirectory() Get buffer directory for QEDEQ module files.
QedeqConfig	getConfig() Get access to configuration parameters.
ContextChecker	getContextChecker() Get context checker.
java.io.File	getGenerationDirectory() Get directory for generated files.
KernelQedeqBo	getKernelQedeqBo(ModuleAddress address) Get KernelQedeqBo for an address.
java.io.File	getLocalFilePath(ModuleAddress address) Transform an URL address into a local file path where the QEDEQ module is buffered.
QedeqFileDao	getQedeqFileDao() Get DAO for reading and writing QEDEQ modules from or to a file.
KernelQedeqBo	loadKernelModule(InternalServiceJob process, ModuleAddress address) Load QEDEQ module.
KernelQedeqBo	loadKernelModule(InternalServiceJob process, ModuleAddress parent, Specification spec) Load specified QEDEQ module from QEDEQ parent module.
boolean	loadRequiredModules(InternalServiceJob process, KernelQedeqBo qedeq) Get required modules of given module.

Methods inherited from interface org.qedeq.kernel.bo.common.KernelProperties

getBuildId, getDedication, getDescriptiveKernelVersion, getKernelCodeName, getKernelVersion, getKernelVersionDirectory, getMaximalRuleVersion, isRuleVersionSupported, isSetConnectionTimeOutSupported, isSetReadTimeoutSupported

Method Detail

getConfig

QedeqConfig getConfig()

Get access to configuration parameters.

Returns:

Configuration access.

getBufferDirectory

java.io.File getBufferDirectory()

Get buffer directory for QEDEQ module files.

Returns:

buffer directory.

getGenerationDirectory

java.io.File getGenerationDirectory()

Get directory for generated files.

Returns:

Generation directory.

getKernelQedeqBo

KernelQedeqBo getKernelQedeqBo(ModuleAddress address)

Get KernelQedeqBo for an address.

Parameters:

address - Look for this address.

Returns:

Existing or new KernelQedeqBo. Never null.

getLocalFilePath

java.io.File getLocalFilePath(ModuleAddress address)

Transform an URL address into a local file path where the QEDEQ module is buffered. If the QEDEQ module is a local file the path to that file is given.

Parameters:

address - Get local address for this QEDEQ module address.

Returns:

Local file path for that address.

loadKernelModule

KernelQedeqBo loadKernelModule(InternalServiceJob process,
                               ModuleAddress address)
                               throws InterruptException

Load QEDEQ module.

Parameters:

process - Working process.

address - Load module from this address.

Returns:

BO for QEDEQ module. Loading still might have failed. Check status.

Throws:

InterruptException - User canceled request.

loadKernelModule

KernelQedeqBo loadKernelModule(InternalServiceJob process,
                               ModuleAddress parent,
                               Specification spec)
                               throws SourceFileExceptionList,
                                      InterruptException

Load specified QEDEQ module from QEDEQ parent module.

Parameters:

process - Working process.

parent - Parent module address.

spec - Specification for another QEDEQ module.

Returns:

Loaded module.

Throws:

SourceFileExceptionList - Loading failed.

InterruptException - User canceled request.

loadRequiredModules

boolean loadRequiredModules(InternalServiceJob process,
                            KernelQedeqBo qedeq)
                            throws InterruptException

Get required modules of given module. You can check the status to know if the loading was successful.

Parameters:

process - Working process.

qedeq - Module to check.

Returns:

Successful loading.

Throws:

InterruptException - User canceled request.

checkWellFormedness

boolean checkWellFormedness(InternalServiceJob process,
                            KernelQedeqBo qedeq)
                            throws InterruptException

Check if all formulas of a QEDEQ module and its required modules are well formed.

Parameters:

process - Working process.

qedeq - Module to check.

Returns:

Was check successful?

Throws:

InterruptException - User canceled request.

checkFormallyProved

boolean checkFormallyProved(InternalServiceJob process,
                            KernelQedeqBo qedeq)
                            throws InterruptException

Check if all propositions of this and all required modules have correct formal proofs.

Parameters:

process - Working process.

qedeq - Module to check.

Returns:

Was check successful?

Throws:

InterruptException - Process execution was canceled by user.

executePlugin

java.lang.Object executePlugin(InternalServiceJob parent,
                               java.lang.String id,
                               KernelQedeqBo qedeq,
                               java.lang.Object data)
                               throws InterruptException

Execute plugin on given QEDEQ module.

Parameters:

parent - Parent service process. Must not be null

id - Plugin id.

qedeq - QEDEQ module.

data - Process data. Additional data beside module.

Returns:

Plugin specific resulting object. Might be null.

Throws:

InterruptException - Process execution was canceled by user.

java.lang.NullPointerException - parent was null.

getQedeqFileDao

QedeqFileDao getQedeqFileDao()

Get DAO for reading and writing QEDEQ modules from or to a file.

Returns:

DAO.

createSourceFileExceptionList

SourceFileExceptionList createSourceFileExceptionList(int code,
                                                      java.lang.String message,
                                                      java.lang.String address,
                                                      java.io.IOException e)

Creates a list with a SourceFileException with dummy position.

Parameters:

address - This source had a problem.

code - Failure code.

message - Textual description of failure.

e - Wrapped exception.

Returns:

Created list.

createSourceFileExceptionList

SourceFileExceptionList createSourceFileExceptionList(int code,
                                                      java.lang.String message,
                                                      java.lang.String address,
                                                      java.lang.RuntimeException e)

Creates a list with a SourceFileException with dummy position.

Parameters:

address - This source had a problem.

code - Failure code.

message - Textual description of failure.

e - Wrapped exception.

Returns:

Created list.

createSourceFileExceptionList

SourceFileExceptionList createSourceFileExceptionList(int code,
                                                      java.lang.String message,
                                                      java.lang.String address,
                                                      java.lang.Exception e)

Creates a list with a SourceFileException with dummy position.

Parameters:

address - This source had a problem.

code - Failure code.

message - Textual description of failure.

e - Wrapped exception.

Returns:

Created list.

getContextChecker

ContextChecker getContextChecker()

Get context checker.

Returns:

Checker for testing if context is valid.