org.jmlspecs.jmldoc.jmldoc_142
Class JmlHtmlFactory

java.lang.Object
  org.jmlspecs.jmldoc.jmldoc_142.JmlHtmlFactory

class JmlHtmlFactory

extends Object

This class is just used to create a factory instance of the JmlHTML class, from which one can call jmlize to do the actual work on a real file. The purpose of this is to allow easy subclassing if necessary. If you want to generate html using a different class than JmlHTML, then create that new class (say NewHTML - does not need to be derived from JmlHTML), create a derived class of JmlHTMLFactory (say NewJmlHTMLFactory), be sure that NewJmlHTMLFactory.jmlize instantiates an instance of NewHTML, and in Main (or a derived class of Main) assign to htmlGenerator an instance of NewJmlHTMLFactory. An alternate design would be to put this factory method in jmlHTML, but then any new Html generation class would have to subclass from JmlHtml.

Constructor Summary

JmlHtmlFactory()

 

Method Summary
void	jmlize(CompilerPassEnterable tree, JmldocOptions options)           This method creates an instance of JmlHTML and calls it to do the html generation for the given set of files (in tree) and command line options.

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

JmlHtmlFactory

public JmlHtmlFactory()

jmlize

public void jmlize(CompilerPassEnterable tree,
                   JmldocOptions options)
            throws Exception

This method creates an instance of JmlHTML and calls it to do the html generation for the given set of files (in tree) and command line options.

Parameters:

tree - The tree of parsed classes

options - The set of command-line options

Throws:

Exception