Sat, 18 Jun 2011 17:42:28 +0200 | wenzelm | updated to jedit_build-20110618, which is required for sub/superscript rendering; | changeset | files |
Sat, 18 Jun 2011 17:33:27 +0200 | wenzelm | basic support for extended syntax styles: sub/superscript; | changeset | files |
Sat, 18 Jun 2011 17:32:13 +0200 | wenzelm | tuned -- Map.empty serves as partial function; | changeset | files |