com.meyling.principia.html
Class Module2JHtml

java.lang.Object
  com.meyling.principia.html.Module2JHtml

public final class Module2JHtml

extends Object

This class converts an module into a html file.

Version:

$Revision: 1.4 $

Author:

Michael Meyling

Constructor Summary

Module2JHtml(ModuleAddress moduleAddress)
Constructor.

Module2JHtml(String moduleAddress)
Constructor.

Method Summary

String	createLink(Module referenced) Get link address for referenced module.
URL	getGeneratedUrl()
String	getText()
static String	stripTags(String text) Strip html tags out of text and mask certain characters.
static String	symbols2Unicode(String from)
static String	toHtml(String text) Escape certain control seqences: ", &.
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

Module2JHtml

public Module2JHtml(ModuleAddress moduleAddress)
             throws ParsingException,
                    IOException

Constructor.

Parameters:

moduleAddress - convert module at this address

Throws:

ParsingException - if any parsing error occurs

IOException - if any file problem occurs

Module2JHtml

public Module2JHtml(String moduleAddress)
             throws ParsingException,
                    IOException

Constructor.

Parameters:

moduleAddress - convert module at this address

Throws:

ParsingException - if any parsing error occurs

IOException - if any file problem occurs

Method Detail

symbols2Unicode

public static final String symbols2Unicode(String from)

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

getText

public final String getText()

getGeneratedUrl

public final URL getGeneratedUrl()
                          throws MalformedURLException

Throws:

MalformedURLException

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

createLink

public final String createLink(Module referenced)

Get link address for referenced module.

Parameters:

referenced - link to this module

Returns:

link address

toHtml

public static final String toHtml(String text)

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

Parameters:

text - excape this text

Returns:

escaped text

stripTags

public static final String stripTags(String text)

Strip html tags out of text and mask certain characters.

Parameters:

text - strip this text

Returns:

striped text