wenzelm [Sun, 08 Aug 2010 14:22:54 +0200] rev 38235
fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
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;