| Sun, 09 Jan 2011 20:30:47 +0100 | wenzelm | more direct treatment of Position.end_offset; | changeset | files |
| Sun, 09 Jan 2011 16:03:56 +0100 | wenzelm | discontinued unused end_line, end_column; | changeset | files |
| Sun, 09 Jan 2011 13:58:31 +0100 | wenzelm | more scalable HTML.output_width; | changeset | files |