org.jmlspecs.jmldoc.jmldoc_142
Class JmlHTML

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

public class JmlHTML

extends Object

This class contains functions to generate html, fitting in with javadoc comments, that documents jml annotations. The current implementation requires that a javadoc file already exist; the code here will insert additional html into the existing javadoc files. It is ok to run this operation of inserting additional html multiple times since the inserted material is marked and removed prior to inserting regenerated material.

An improved implementation will generate the html from scratch, by calling appropriate methods in the javadoc implementation, potentially as a doclet. Note that the current implementation requires that javadoc be runnable on the file; thus the files must be legal java, without mjc extensions.

Not currently implemented:
reading of spec/.jml files (and refines clauses and files)
implement weakly, jml_var_assertion, static_initializer, initializer
model programs

Other comments and bugs:
Better wrapping of long specs: mostly ok, but would like to have hanging indents
format specifications: can we get rid of blank lines near {| and |}?
Add comments, javadoc comments, specifications to this code
Better error reporting when a ; is missing from a jml spec.
Interleave parsing and jml generation
How to record http: links in the docpath and associate them with packages - use multiple -link options ?
Resolve all ??? comments in the code, and these comments here.
The <- does not appear very elegantly (also _ and \ )
Loosen up the syntactic requirements on PRE JML (as tags)
sort out the finding of target html files (package-lists etc.)
find a better way to find information from CClass objects rather than having to find the JmlTypeDeclaration (and parse the relevant file)
CAUTION: There are static values that are not protected. If any thought is given to multi-threading the generation of html, some work will need to be done here.

Nested Class Summary
static class	JmlHTML.IntPair           This class holds a pair of integers, used here to mark the start and (one past the) end of a section of a text string.
static class	JmlHTML.IntString           This class holds an integer and a String, corresponding to a position at which to insert text, and the text to be inserted at that position.

 

Field Summary
private static String	adjustedDestination           This gives the absolute path of the destination for generated html files.
private static String	alternateSuffix           A second suffix for html files that should be tried.
private  String	classSpecsTitle
protected  File	currentFile
protected  String	currentFilePath
private static String	eol           The string that terminates lines on this platform.
private static String	jmlbegin           Used to begin any section of material added to an HTML file.
private static String	jmlcomment1
private static String	jmlcomment2
private static String	jmlend           Used to end any section of material added to an HTML file.
private static String	newsuffix           This string is used as a suffix for the new html file, temporarily; Once the file is complete it is moved on top of the old one.
private static String	oldsuffix           This string is used as a suffix for the backup files - the original html files before begin altered by adding jml annotations.
private static JmldocOptions	options           This is a cached value of the options object supplied here from Main.
private  boolean	printedClassSpecsHeader
private static String	suffix           The value of the suffix that javadoc uses on this platform for html files, with the leading period.
private static boolean	useDollar           This field is true if html files generated by javadoc use dollar signs to separate components in the names of HTML files for inner classes (this is not the same as using dollar signs in .class files).

 

Constructor Summary

JmlHTML(JmldocOptions opt)

 

Method Summary
void	addLink(CClass container, JmlStoreRefExpression sre, JmldocFieldSubWriter fsw, SpecWriter sw)
protected  boolean	checkFile(String dp, boolean useD, String cp, String suf)           This function checks whether a html file exists with a name constructed from the given class name (cp), and the given settings of the destination directory (dp), useDollar (useD) and suffix to use (suf).
(package private) static boolean	checkModifiers(long mods)           This function compares the argument to the privacy level set in the command-line options ; it returns true if the argument is enabled to be printed per the option.
protected  void	classSpecs(JmlTypeDeclaration jmltype, StringBuffer sb, boolean inherited, String title)           This method generates the html describing the specifications of class/interface jmltype.
protected  boolean	findFile(String cpath, String packageRoot)           This function finds an html file for the given class name (cpath) and directory containing the package root (packageRoot).
(package private) static JmlMethodDeclaration	findMatchingMethod(JmlTypeDeclaration jt, JmlMethodDeclaration jm)           Looks for method jm in class/interface jt; returns null if not found, otherwise returns the corresponding JmlMethodDeclaration.
void	findSections(String fileString, String begin, String end, ArrayList extracts)           This function finds all occurrences of text in 'fileString' bracketed by the given begin and end Strings.
void	findSections(String fileString, String begin, ArrayList extracts)           This function finds all occurrences of the string begin in 'fileString' .
protected  String	generateClassSpecification(JmlTypeDeclaration jmltype, com.sun.tools.doclets.standard.HtmlStandardWriter writer)           This generates the full html insert for the class level specifications, including those for any super classes and including the leading jmlbegin and jmlend strings.
String	generateFieldSpecification(JFieldDeclarationType jm, JmldocFieldSubWriter fsw)
String	generateMethodSpecification(JmlMethodDeclaration jm, CClass cclass, String sig, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
(package private) static List	getAllInterfaces(CClass cc)           The result is a List of CClassType objects containing all the interfaces, with no duplicates.
private static void	getAllInterfaces(CClassType[] ints, List interfaces)           This function adds to 'interfaces' any interfaces implemented by the classes or interfaces in 'ints'.
protected  void	insertFieldSpecs(JmlTypeDeclaration jmltype, String fileString, ArrayList insertions)           This method generates the html text for the specifications of the fields for type jmlType, with reference to the original file content in fileString.
protected  void	insertMethodSpecs(JmlMethodDeclaration jm, String fileString, ArrayList insertions, String sig, JmlTypeDeclaration jmltype)           This method generates the specification text for the method jm with signature string sig belonging to class jmltype, and with reference to the original html file in fileString.
protected  void	insertMethodSpecs(JmlTypeDeclaration jmltype, String fileString, ArrayList insertions)           This method generates the html text for the specifications of the methods for type jmlType, with reference to the original file content in fileString.
protected  void	insertSpecification(StringBuffer s, JmlMethodSpecification jms)           This method actually generates a string representing the given JmlMethodSpecification and appends it to the given StringBuffer.
void	jmlize(CompilerPassEnterable tree)           This is the entry point into these routines for adding html material representing the jml annotations to an html file.
(package private)  void	jmlize(JTypeDeclarationType jtype, String packageRoot)           This method generates the html file for the class represented by 'jtype'.
protected  void	jmlizeFile(File f, JTypeDeclarationType jtype)           This method inserts into the given File all the jml annotations corresponding to the given JTypeDeclarationType.
String	linkString(CClass cclass, boolean fullname, com.sun.tools.doclets.standard.HtmlStandardWriter writer)           This function generates a String giving the name of the class corresponding to 'cclass'; if an html file can be located for this class, then the string consists of an HTML link reference to that class.
(package private) static String	makeSig(JmlMethodDeclaration m, JmlTypeDeclaration jmltype)           This function returns a String giving the signature of a method - the method name and fully qualified argument types, but not formal parameter names.
void	printClassSpecsFooter(StringBuffer classspec)
void	printClassSpecsHeader(StringBuffer classspec, boolean inherited, String title)
void	printClassSpecsHeaderInherited(StringBuffer classspec, String title)
void	printClassSpecsHeaderMain(StringBuffer classspec)
void	printClassSpecsHeaderShort(StringBuffer classspec)
protected  boolean	superSpecification(StringBuffer s, CClass sclass, JmlMethodDeclaration jm, String sig, boolean isclass, com.sun.tools.doclets.standard.HtmlStandardWriter writer)           Generates the html for any specifications for the method 'jm' in the super class 'sclass'.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

eol

private static final String eol

The string that terminates lines on this platform.

jmlbegin

private static final String jmlbegin

Used to begin any section of material added to an HTML file.

jmlend

private static final String jmlend

Used to end any section of material added to an HTML file.

jmlcomment1

private static final String jmlcomment1

jmlcomment2

private static final String jmlcomment2

oldsuffix

private static final String oldsuffix

This string is used as a suffix for the backup files - the original html files before begin altered by adding jml annotations.

newsuffix

private static final String newsuffix

This string is used as a suffix for the new html file, temporarily; Once the file is complete it is moved on top of the old one.

options

private static JmldocOptions options

This is a cached value of the options object supplied here from Main.

adjustedDestination

private static String adjustedDestination

This gives the absolute path of the destination for generated html files. It is the same as the command-line option, unless the destination is not specified on the command-line, in which case this variable is set to where the output files are found to be located.

useDollar

private static boolean useDollar

This field is true if html files generated by javadoc use dollar signs to separate components in the names of HTML files for inner classes (this is not the same as using dollar signs in .class files). This is platform dependent. On Mac OS X, the value is false. If the files cannot be found, the functions below will try alternate values of this variable in an attempt to find the files.

suffix

private static String suffix

The value of the suffix that javadoc uses on this platform for html files, with the leading period. On Mac OS X: html

alternateSuffix

private static String alternateSuffix

A second suffix for html files that should be tried.

currentFile

protected File currentFile

currentFilePath

protected String currentFilePath

classSpecsTitle

private final String classSpecsTitle

printedClassSpecsHeader

private boolean printedClassSpecsHeader

JmlHTML

public JmlHTML(JmldocOptions opt)

jmlize

public void jmlize(CompilerPassEnterable tree)
            throws Exception

This is the entry point into these routines for adding html material representing the jml annotations to an html file. It does this work for all the classes defined in the compilation unit represented by 'tree'.

Throws:

Exception

jmlize

void jmlize(JTypeDeclarationType jtype,
            String packageRoot)
      throws Exception

This method generates the html file for the class represented by 'jtype'.

Throws:

Exception

checkModifiers

static boolean checkModifiers(long mods)

This function compares the argument to the privacy level set in the command-line options ; it returns true if the argument is enabled to be printed per the option.

checkFile

protected boolean checkFile(String dp,
                            boolean useD,
                            String cp,
                            String suf)

This function checks whether a html file exists with a name constructed from the given class name (cp), and the given settings of the destination directory (dp), useDollar (useD) and suffix to use (suf). It returns true if the file could be found.

findFile

protected boolean findFile(String cpath,
                           String packageRoot)

This function finds an html file for the given class name (cpath) and directory containing the package root (packageRoot). It tries various options for adjustedDestination, useDollar, and suffix until it finds a successful combination. Returns true if some combination is successful, and false if not. If successful adjustedDestination, useDollar, and suffix are set to the successful values.

findSections

public void findSections(String fileString,
                         String begin,
                         String end,
                         ArrayList extracts)
                  throws Exception

This function finds all occurrences of text in 'fileString' bracketed by the given begin and end Strings. The beginning and end of that text segment (including the bracketing strings) is added as an element to the 'extracts' ArrayList.

Throws:

Exception

findSections

public void findSections(String fileString,
                         String begin,
                         ArrayList extracts)
                  throws Exception

This function finds all occurrences of the string begin in 'fileString' . The beginning and end of that text segment (including the bracketing strings) is added as an element to the 'extracts' ArrayList.

Throws:

Exception

classSpecs

protected void classSpecs(JmlTypeDeclaration jmltype,
                          StringBuffer sb,
                          boolean inherited,
                          String title)

This method generates the html describing the specifications of class/interface jmltype. The text is appended to the given StringBuffer (without jmlbegin and jmlend). If this is a super class/interface, then 'inherited' should be true. 'jmltype' is null iff the specs for 'title' cannot be located.

printClassSpecsHeader

public void printClassSpecsHeader(StringBuffer classspec,
                                  boolean inherited,
                                  String title)

printClassSpecsHeaderMain

public void printClassSpecsHeaderMain(StringBuffer classspec)

printClassSpecsHeaderShort

public void printClassSpecsHeaderShort(StringBuffer classspec)

printClassSpecsHeaderInherited

public void printClassSpecsHeaderInherited(StringBuffer classspec,
                                           String title)

printClassSpecsFooter

public void printClassSpecsFooter(StringBuffer classspec)

jmlizeFile

protected void jmlizeFile(File f,
                          JTypeDeclarationType jtype)
                   throws Exception

This method inserts into the given File all the jml annotations corresponding to the given JTypeDeclarationType. The file must be the html file for the given class/interface.

Throws:

Exception

generateClassSpecification

protected String generateClassSpecification(JmlTypeDeclaration jmltype,
                                            com.sun.tools.doclets.standard.HtmlStandardWriter writer)

This generates the full html insert for the class level specifications, including those for any super classes and including the leading jmlbegin and jmlend strings.

getAllInterfaces

static List getAllInterfaces(CClass cc)

The result is a List of CClassType objects containing all the interfaces, with no duplicates.

getAllInterfaces

private static void getAllInterfaces(CClassType[] ints,
                                     List interfaces)

This function adds to 'interfaces' any interfaces implemented by the classes or interfaces in 'ints'.

makeSig

static String makeSig(JmlMethodDeclaration m,
                      JmlTypeDeclaration jmltype)

This function returns a String giving the signature of a method - the method name and fully qualified argument types, but not formal parameter names. It must be called after type checking has been run on the parse tree.

findMatchingMethod

static JmlMethodDeclaration findMatchingMethod(JmlTypeDeclaration jt,
                                               JmlMethodDeclaration jm)

Looks for method jm in class/interface jt; returns null if not found, otherwise returns the corresponding JmlMethodDeclaration.

insertMethodSpecs

protected void insertMethodSpecs(JmlTypeDeclaration jmltype,
                                 String fileString,
                                 ArrayList insertions)
                          throws Exception

This method generates the html text for the specifications of the methods for type jmlType, with reference to the original file content in fileString. The insertion points and text are recorded in the insertions ArrayList for later insertion.

Throws:

Exception

insertFieldSpecs

protected void insertFieldSpecs(JmlTypeDeclaration jmltype,
                                String fileString,
                                ArrayList insertions)
                         throws Exception

This method generates the html text for the specifications of the fields for type jmlType, with reference to the original file content in fileString. The insertion points and text are recorded in the insertions ArrayList for later insertion.

Throws:

Exception

generateFieldSpecification

public String generateFieldSpecification(JFieldDeclarationType jm,
                                         JmldocFieldSubWriter fsw)

addLink

public void addLink(CClass container,
                    JmlStoreRefExpression sre,
                    JmldocFieldSubWriter fsw,
                    SpecWriter sw)

insertMethodSpecs

protected void insertMethodSpecs(JmlMethodDeclaration jm,
                                 String fileString,
                                 ArrayList insertions,
                                 String sig,
                                 JmlTypeDeclaration jmltype)
                          throws Exception

This method generates the specification text for the method jm with signature string sig belonging to class jmltype, and with reference to the original html file in fileString. The jm method may be a method of a super class/interface that is being overridden by a method in jmltype. The new text and its insertion point are recorded in the insertions ArrayList.

Throws:

Exception

generateMethodSpecification

public String generateMethodSpecification(JmlMethodDeclaration jm,
                                          CClass cclass,
                                          String sig,
                                          com.sun.tools.doclets.standard.HtmlStandardWriter writer)

superSpecification

protected boolean superSpecification(StringBuffer s,
                                     CClass sclass,
                                     JmlMethodDeclaration jm,
                                     String sig,
                                     boolean isclass,
                                     com.sun.tools.doclets.standard.HtmlStandardWriter writer)

Generates the html for any specifications for the method 'jm' in the super class 'sclass'. 'isclass' is true if 'sclass' is a class, false if it is an interface. The function returns true if any text was generated, false if no text was generated. Any html text generated is appended to the given StringBuffer. The String 'sig' is the textual signature of the method.

insertSpecification

protected void insertSpecification(StringBuffer s,
                                   JmlMethodSpecification jms)

This method actually generates a string representing the given JmlMethodSpecification and appends it to the given StringBuffer. This happens by walking the AST that represents the method specification.

linkString

public String linkString(CClass cclass,
                         boolean fullname,
                         com.sun.tools.doclets.standard.HtmlStandardWriter writer)

This function generates a String giving the name of the class corresponding to 'cclass'; if an html file can be located for this class, then the string consists of an HTML link reference to that class. If 'fullname' is true, then the name is given with the package prefix; otherwise just the name (with enclosing classes) is given.