#
4b000659 |
|
11-Dec-2012 |
wenzelm <none@none> |
added speculative options for jEdit;
|
#
8096421a |
|
14-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete CVS Ids; tuned headers;
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
7d5c82fe |
|
07-May-2003 |
kleing <none@none> |
cleanup, comments
|
#
8e3a4630 |
|
07-May-2003 |
kleing <none@none> |
eliminated dependencies on AWT for batch mode
|
#
50903194 |
|
22-Oct-2001 |
berghofe <none@none> |
Constructor no longer takes font as an argument.
|
#
0202d8dc |
|
16-Oct-2001 |
berghofe <none@none> |
Inserted table for character widths.
|
#
c840e330 |
|
16-Oct-2001 |
berghofe <none@none> |
Font metrics used for batch mode layout (without X11 connection).
|