| java.lang.Object de.uka.ilkd.key.util.keydoc.html.BoxedFile
BoxedFile | class BoxedFile (Code) | | Class containing the HTML representation of the .Key files documentation as processed by the KeyToHTMLBuilder and some other usefull information for the Director.
It stores the three attributes fileName, shortDescription and the processed html file.
|
Constructor Summary | |
public | BoxedFile(File file, int firstLength, int firstOffset, HTMLFile htmlFile) Boxedfile Constructor. |
BoxedFile | public BoxedFile(File file, int firstLength, int firstOffset, HTMLFile htmlFile)(Code) | | Boxedfile Constructor.
Boxes a HTMLFile
Parameters: fileName - The name of the .key file Parameters: shortDescription - Short description of the purpose of the .key file Parameters: htmlFile - The processed .key file |
getFirstLength | protected int getFirstLength()(Code) | | |
getFirstOffset | protected int getFirstOffset()(Code) | | |
|
|