Sun, 21 Dec 2008 22:09:08 +0100dummy class to make ant javadoc work;
wenzelm [Sun, 21 Dec 2008 22:09:08 +0100] rev 34440
dummy class to make ant javadoc work;

Sun, 21 Dec 2008 21:43:41 +0100use Plugin.self.symbols;
wenzelm [Sun, 21 Dec 2008 21:43:41 +0100] rev 34439
use Plugin.self.symbols;
tuned;

Sun, 21 Dec 2008 21:43:41 +0100renamed Plugin.plugin to Plugin.self;
wenzelm [Sun, 21 Dec 2008 21:43:41 +0100] rev 34438
renamed Plugin.plugin to Plugin.self;
use Plugin.self.symbols;
tuned;

Sun, 21 Dec 2008 21:43:41 +0100renamed Plugin.plugin to Plugin.self;
wenzelm [Sun, 21 Dec 2008 21:43:41 +0100] rev 34437
renamed Plugin.plugin to Plugin.self;
tuned Plugin.font handling;

Sun, 21 Dec 2008 21:43:41 +0100renamed Plugin.plugin to Plugin.self;
wenzelm [Sun, 21 Dec 2008 21:43:41 +0100] rev 34436
renamed Plugin.plugin to Plugin.self;
added Symbol.Interpretation (formerly in VFS);
tuned Plugin.font handling;
tuned;

Sun, 21 Dec 2008 21:43:40 +0100renamed Plugin.plugin to Plugin.self;
wenzelm [Sun, 21 Dec 2008 21:43:40 +0100] rev 34435
renamed Plugin.plugin to Plugin.self;

Sun, 21 Dec 2008 20:36:41 +0100tuned;
wenzelm [Sun, 21 Dec 2008 20:36:41 +0100] rev 34434
tuned;

Sun, 21 Dec 2008 20:36:09 +0100renamed isabelle.jedit.UserAgent to isabelle.renderer.UserAgent;
wenzelm [Sun, 21 Dec 2008 20:36:09 +0100] rev 34433
renamed isabelle.jedit.UserAgent to isabelle.renderer.UserAgent;

Sun, 21 Dec 2008 20:16:43 +0100tuned;
wenzelm [Sun, 21 Dec 2008 20:16:43 +0100] rev 34432
tuned;

Sun, 21 Dec 2008 19:51:56 +0100basic setup of anti-aliasing, according to jEdit property;
wenzelm [Sun, 21 Dec 2008 19:51:56 +0100] rev 34431
basic setup of anti-aliasing, according to jEdit property;
tuned;