wenzelm [Sun, 08 Aug 2010 14:00:59 +0200] rev 38234
YXML.parse: refrain from interning, let XML.Cache do it (partially);
wenzelm [Sun, 08 Aug 2010 13:59:57 +0200] rev 38233
cache_string: store trimmed string value;
wenzelm [Sat, 07 Aug 2010 23:02:19 +0200] rev 38232
simple_dialog: allow scala.swing.Component as well;
wenzelm [Sat, 07 Aug 2010 22:43:57 +0200] rev 38231
simplified some Markup;
wenzelm [Sat, 07 Aug 2010 22:09:52 +0200] rev 38230
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
XML.cache_tree: actually store XML.Text as well;
added Isabelle_Process.Result.properties;
wenzelm [Sat, 07 Aug 2010 21:22:39 +0200] rev 38229
more robust treatment of Markup.token;
wenzelm [Sat, 07 Aug 2010 21:03:06 +0200] rev 38228
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm [Sat, 07 Aug 2010 19:52:14 +0200] rev 38227
concentrate structural document notions in document.scala;
tuned;
wenzelm [Sat, 07 Aug 2010 17:24:46 +0200] rev 38226
maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm [Sat, 07 Aug 2010 16:49:03 +0200] rev 38225
tuned;