wenzelm [Thu, 21 Aug 2008 22:06:17 +0200] rev 27946
parse_attrib: proper index of name end!
wenzelm [Thu, 21 Aug 2008 21:42:16 +0200] rev 27945
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm [Thu, 21 Aug 2008 21:27:07 +0200] rev 27944
parse_attrib: more efficient due to indexOf('=');
wenzelm [Thu, 21 Aug 2008 20:53:31 +0200] rev 27943
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm [Thu, 21 Aug 2008 20:51:41 +0200] rev 27942
tuned comment;
wenzelm [Thu, 21 Aug 2008 19:19:31 +0200] rev 27941
added iterator over content;
wenzelm [Thu, 21 Aug 2008 17:42:59 +0200] rev 27940
proper ISABELLE_ROOT_JVM on Cygwin;
wenzelm [Thu, 21 Aug 2008 16:02:54 +0200] rev 27939
pattern: proper "." not "[.]"!
tuned;
wenzelm [Thu, 21 Aug 2008 15:27:28 +0200] rev 27938
recode: proper result for unmatched symbols;
wenzelm [Thu, 21 Aug 2008 15:20:00 +0200] rev 27937
more robust pattern: look at longer matches first, added catch-all case;
more private fields;
reworked Recoder: more direct char/string operations, avoids inefficiency of large alternatives (java.util.regex does not optimize regexps);