Thu, 21 Aug 2008 20:53:31 +0200 replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm [Thu, 21 Aug 2008 20:53:31 +0200] rev 27943
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
Thu, 21 Aug 2008 20:51:41 +0200 tuned comment;
wenzelm [Thu, 21 Aug 2008 20:51:41 +0200] rev 27942
tuned comment;
Thu, 21 Aug 2008 19:19:31 +0200 added iterator over content;
wenzelm [Thu, 21 Aug 2008 19:19:31 +0200] rev 27941
added iterator over content;
Thu, 21 Aug 2008 17:42:59 +0200 proper ISABELLE_ROOT_JVM on Cygwin;
wenzelm [Thu, 21 Aug 2008 17:42:59 +0200] rev 27940
proper ISABELLE_ROOT_JVM on Cygwin;
Thu, 21 Aug 2008 16:02:54 +0200 pattern: proper "." not "[.]"!
wenzelm [Thu, 21 Aug 2008 16:02:54 +0200] rev 27939
pattern: proper "." not "[.]"! tuned;
Thu, 21 Aug 2008 15:27:28 +0200 recode: proper result for unmatched symbols;
wenzelm [Thu, 21 Aug 2008 15:27:28 +0200] rev 27938
recode: proper result for unmatched symbols;
Thu, 21 Aug 2008 15:20:00 +0200 more robust pattern: look at longer matches first, added catch-all case;
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);
Thu, 21 Aug 2008 13:05:37 +0200 added get_setting;
wenzelm [Thu, 21 Aug 2008 13:05:37 +0200] rev 27936
added get_setting; removed obsolete ISABELLE_HOME, ISABELLE_HOME_USER; added platform_path, which expands variables and performs basic cygwin conversion;
Thu, 21 Aug 2008 13:05:31 +0200 read_symbols: proper IsabelleSystem.platform_path;
wenzelm [Thu, 21 Aug 2008 13:05:31 +0200] rev 27935
read_symbols: proper IsabelleSystem.platform_path;
Thu, 21 Aug 2008 13:05:28 +0200 added ISABELLE_ROOT_JVM;
wenzelm [Thu, 21 Aug 2008 13:05:28 +0200] rev 27934
added ISABELLE_ROOT_JVM; removed obsolete ISABELLE_HOME_JVM, ISABELLE_HOME_USER_JVM;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip