Qedeq2LatexExecutor (QEDEQ Kernel for the Hilbert II project 0.04.08 API)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.qedeq.kernel.bo.service.latex
Class Qedeq2LatexExecutor

java.lang.Object
  org.qedeq.kernel.se.visitor.AbstractModuleVisitor
      org.qedeq.kernel.bo.service.basis.ControlVisitor
          org.qedeq.kernel.bo.service.latex.Qedeq2LatexExecutor

All Implemented Interfaces:: ModuleServicePluginExecutor, ServiceCompleteness, ListVisitor, QedeqVisitor

public final class Qedeq2LatexExecutor
extends ControlVisitor
implements ModuleServicePluginExecutor
extends ControlVisitor
implements ModuleServicePluginExecutor

Transfer a QEDEQ module into a LaTeX file.

This is just a quick written generator. No parsing or validation of inline LaTeX text is done. This class just generates some LaTeX output to be able to get a visual impression of a QEDEQ module.

Author:: Michael Meyling

Constructor Summary
`Qedeq2LatexExecutor(ModuleService plugin, KernelQedeqBo prop, Parameters parameters)` Constructor.

Method Summary
`java.io.InputStream`	`createLatex(InternalModuleServiceCall call, java.lang.String language, java.lang.String level)` Get an input stream for the LaTeX creation.
`java.lang.Object`	`executePlugin(InternalModuleServiceCall call, java.lang.Object data)` Execute plugin.
`java.io.File`	`generateLatex(InternalModuleServiceCall call, java.lang.String language, java.lang.String level)` Gives a LaTeX representation of given QEDEQ module as InputStream.
`ModuleContext`	`getCurrentContext(SourcePosition startDelta, SourcePosition endDelta)` Get current module context.
`protected void`	`init()` Reset counters and other variables.
`void`	`visitEnter(Add r)` Visit certain element.
`void`	`visitEnter(Axiom axiom)` Visit certain element.
`void`	`visitEnter(ChangedRule rule)` Visit certain element.
`void`	`visitEnter(ChangedRuleList list)` Visit certain element.
`void`	`visitEnter(Chapter chapter)` Visit certain element.
`void`	`visitEnter(Conclusion conclusion)` Visit certain element.
`void`	`visitEnter(ConditionalProof r)` Visit conditional proof line.
`void`	`visitEnter(Existential r)` Visit certain element.
`void`	`visitEnter(FormalProof proof)` Visit certain element.
`void`	`visitEnter(FormalProofLine line)` Visit formal proof line (but not an conditional proof line).
`void`	`visitEnter(FormalProofLineList lines)` Visit certain element.
`void`	`visitEnter(FunctionDefinition definition)` Visit certain element.
`void`	`visitEnter(Header header)` Visit certain element.
`void`	`visitEnter(Hypothesis hypothesis)` Visit certain element.
`void`	`visitEnter(Import imp)` Visit certain element.
`void`	`visitEnter(ImportList imports)` Visit certain element.
`void`	`visitEnter(InitialFunctionDefinition definition)` Visit certain element.
`void`	`visitEnter(InitialPredicateDefinition definition)` Visit certain element.
`void`	`visitEnter(LinkList linkList)` Visit certain element.
`void`	`visitEnter(LiteratureItem item)` Visit certain element.
`void`	`visitEnter(LiteratureItemList list)` Visit certain element.
`void`	`visitEnter(ModusPonens r)` Visit certain element.
`void`	`visitEnter(Node node)` Visit certain element.
`void`	`visitEnter(PredicateDefinition definition)` Visit certain element.
`void`	`visitEnter(Proof proof)` Visit certain element.
`void`	`visitEnter(Proposition proposition)` Visit certain element.
`void`	`visitEnter(Qedeq qedeq)` Visit certain element.
`void`	`visitEnter(Rename r)` Visit certain element.
`void`	`visitEnter(Rule rule)` Visit certain element.
`void`	`visitEnter(Section section)` Visit certain element.
`void`	`visitEnter(Subsection subsection)` Visit certain element.
`void`	`visitEnter(SubstFree r)` Visit certain element.
`void`	`visitEnter(SubstFunc r)` Visit certain element.
`void`	`visitEnter(SubstPred r)` Visit certain element.
`void`	`visitEnter(Universal r)` Visit certain element.
`void`	`visitLeave(Chapter chapter)` Visit certain element.
`void`	`visitLeave(Conclusion conclusion)` Visit certain element.
`void`	`visitLeave(ConditionalProof proof)` Visit certain element.
`void`	`visitLeave(FormalProof proof)` Visit certain element.
`void`	`visitLeave(FormalProofLine line)` Visit certain element.
`void`	`visitLeave(FormalProofLineList lines)` Visit certain element.
`void`	`visitLeave(FunctionDefinition definition)` Visit certain element.
`void`	`visitLeave(Header header)` Visit certain element.
`void`	`visitLeave(Hypothesis hypothesis)` Visit certain element.
`void`	`visitLeave(LiteratureItemList list)` Visit certain element.
`void`	`visitLeave(Node node)` Visit certain element.
`void`	`visitLeave(Proof proof)` Visit certain element.
`void`	`visitLeave(Qedeq qedeq)` Visit certain element.
`void`	`visitLeave(Rule rule)` Visit certain element.
`void`	`visitLeave(Section section)` Visit certain element.
`void`	`visitLeave(SectionList list)` Visit certain element.
`void`	`visitLeave(Subsection subsection)` Visit certain element.

Methods inherited from class org.qedeq.kernel.bo.service.basis.ControlVisitor
`addError, addError, addWarning, getBlocked, getCurrentContext, getCurrentNumbers, getErrorList, getInternalServiceCall, getInterrupted, getKernelQedeqBo, getLocalRuleKey, getLocationDescription, getNodeBo, getNodeDisplay, getReference, getService, getServices, getTraverser, getVisitPercentage, getWarningList, hasErrors, hasNoErrors, setBlocked, setLocationWithinModule, traverse`

Methods inherited from class org.qedeq.kernel.se.visitor.AbstractModuleVisitor
visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave

Methods inherited from class org.qedeq.kernel.se.visitor.AbstractModuleVisitor

visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitEnter, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave, visitLeave

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Methods inherited from interface org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor
`getInterrupted, getLocationDescription, getVisitPercentage`

Constructor Detail

Qedeq2LatexExecutor

public Qedeq2LatexExecutor(ModuleService plugin,
                           KernelQedeqBo prop,
                           Parameters parameters)

Constructor.

Parameters:: plugin - This plugin we work for.; prop - QEDEQ BO object.; parameters - Parameters.

Method Detail

executePlugin

public java.lang.Object executePlugin(InternalModuleServiceCall call,
                                      java.lang.Object data)

Description copied from interface: ModuleServicePluginExecutor

Execute plugin.

Specified by:: executePlugin in interface ModuleServicePluginExecutor

Parameters:: call - Service call.; data - Process execution data.
Returns:: Plugin specific resulting object. Might be null.

createLatex

public java.io.InputStream createLatex(InternalModuleServiceCall call,
                                       java.lang.String language,
                                       java.lang.String level)
                                throws SourceFileExceptionList,
                                       java.io.IOException

Get an input stream for the LaTeX creation.

Parameters:: call - This process executes us.; language - Filter text to get and produce text in this language only.; level - Filter for this detail level. LATER mime 20050205: not supported yet.
Returns:: Resulting LaTeX.
Throws:: SourceFileExceptionList - Major problem occurred.; java.io.IOException - File IO failed.

generateLatex

public java.io.File generateLatex(InternalModuleServiceCall call,
                                  java.lang.String language,
                                  java.lang.String level)
                           throws SourceFileExceptionList,
                                  java.io.IOException

Gives a LaTeX representation of given QEDEQ module as InputStream.

Parameters:: call - This process executes us.; language - Filter text to get and produce text in this language only. null is ok.; level - Filter for this detail level. LATER mime 20050205: not supported yet.
Returns:: Resulting LaTeX.
Throws:: SourceFileExceptionList - Major problem occurred.; java.io.IOException - File IO failed.

init

protected void init()

Reset counters and other variables. Should be executed before #traverse().