com.meyling.principia.latex
Class Module2Latex

java.lang.Object
  com.meyling.principia.latex.Module2Latex

public final class Module2Latex

extends Object

This class converts an module into an LaTeX file.

Version:

$Revision: 1.28 $

Author:

Michael Meyling

Constructor Summary

Module2Latex(String moduleAddress)
Constructor.

Method Summary

String	createLink(Module referenced) Get link address for referenced module.
String	createLink(String reference) Get link address for referenced module.
String	createLink(String reference, String description) Get link address for referenced module.
String	createQedeqLink(Module referenced) Get link address for referenced module.
static String	qedeq2latex(String text) Replace \qedeq by LaTeX commands.
static String	stripTags(String text) Strip html tags out of text.
static String	toLatex(String text) Escape certain control seqences: ", &.
void	writeFormula(Argument argument, Output output) Convert a Formula or its sub arguments into LaTeX.
void	writeModule() Convert a Module (referenced by module address in constructor) into html.
void	writeProofLine(ProofLine line, Output output, String label) Convert a ProofLine into html.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Module2Latex

public Module2Latex(String moduleAddress)

Constructor.

Parameters:

moduleAddress - convert module at this address

Method Detail

writeModule

public final void writeModule()
                       throws ParsingException,
                              IOException

Convert a Module (referenced by module address in constructor) into html.

Throws:

ParsingException - if any parsing error occurs

IOException - if any file problem occurs

writeProofLine

public final void writeProofLine(ProofLine line,
                                 Output output,
                                 String label)

Convert a ProofLine into html.

Parameters:

line - convert this

output - destination for resulting html code

label - for proof line references

writeFormula

public final void writeFormula(Argument argument,
                               Output output)

Convert a Formula or its sub arguments into LaTeX.

Parameters:

argument - convert this

output - destination for resulting LaTeX

toLatex

public static final String toLatex(String text)

Escape certain control seqences: ", &. Doesn't escape <: or >!

Parameters:

text - excape this text

Returns:

escaped text

qedeq2latex

public static final String qedeq2latex(String text)

Replace \qedeq by LaTeX commands.

Parameters:

text - excape this text

Returns:

pure LaTeX

stripTags

public static final String stripTags(String text)

Strip html tags out of text.

Parameters:

text - strip this text

Returns:

striped text

createLink

public final String createLink(Module referenced)

Get link address for referenced module.

Parameters:

referenced - link to this module

Returns:

link address

createLink

public final String createLink(String reference)

Get link address for referenced module.

Returns:

link command

createLink

public final String createLink(String reference,
                               String description)

Get link address for referenced module.

Parameters:

description - describes linked object

Returns:

link command

createQedeqLink

public final String createQedeqLink(Module referenced)

Get link address for referenced module.

Parameters:

referenced - link to this module

Returns:

link address