Hilbert II - JAVA-Packages - Principia Mathematica II

com.meyling.principia.html
Class Module2JHtml

java.lang.Object
  extended bycom.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

Hilbert II - JAVA-Packages - Principia Mathematica II

©left GNU General Public Licence
All Rights Reserved.