| Mon, 31 May 2010 09:46:43 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 30 May 2010 23:42:03 +0200 | wenzelm | control tooltip font via Swing HTML, with tooltip-font-size property; | changeset | files |
| Sun, 30 May 2010 23:40:24 +0200 | wenzelm | added HTML.encode (in Scala), similar to HTML.output in ML; | changeset | files |
| Sun, 30 May 2010 21:59:15 +0200 | wenzelm | one extra space to accomodate symbolic indentifiers etc.; | changeset | files |
| Sun, 30 May 2010 21:34:19 +0200 | wenzelm | replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; | changeset | files |
| Sun, 30 May 2010 18:23:50 +0200 | wenzelm | more detailed token markup, including command kind as sub_kind; | changeset | files |
| Sun, 30 May 2010 16:54:40 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 30 May 2010 16:00:13 +0200 | wenzelm | separate markup for ML delimiters; | changeset | files |