JML

org.jmlspecs.jmldoc.jmldoc_142
Class JmlHTML

java.lang.Object
  extended byorg.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
Constructor Detail

JmlHTML

public JmlHTML(JmldocOptions opt)
Method Detail

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.