Tue, 21 Jun 2011 13:29:44 +0200 | wenzelm | tuned iteration over short symbols; | changeset | files |
Tue, 21 Jun 2011 12:53:55 +0200 | wenzelm | Symbol.is_ctrl: handle decoded version as well; | changeset | files |
Tue, 21 Jun 2011 01:08:15 +0200 | wenzelm | some support for user symbol fonts; | changeset | files |
Mon, 20 Jun 2011 23:25:39 +0200 | wenzelm | removed obsolete font specification; | changeset | files |
Mon, 20 Jun 2011 23:21:24 +0200 | wenzelm | more tolerant Symbol.decode; | changeset | files |
Mon, 20 Jun 2011 23:19:38 +0200 | wenzelm | simplified/generalized ISABELLE_FONTS handling; | changeset | files |
Mon, 20 Jun 2011 22:48:41 +0200 | wenzelm | updated to jedit_build-20110620; | changeset | files |