src/Pure/library.ML
2015-01-29 wenzelm 2015-01-29 tuned;
2014-12-22 wenzelm 2014-12-22 obsolete;
2014-12-22 wenzelm 2014-12-22 separate module Random; proper Synchronized.var;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-08 wenzelm 2014-10-08 eliminated some exotic combinators;
2014-10-08 wenzelm 2014-10-08 tuned;
2014-08-12 wenzelm 2014-08-12 more compact representation of special string values;
2014-08-10 wenzelm 2014-08-10 tuned -- avoid confusion with @{assert} for system failures (exception Fail);
2014-07-31 wenzelm 2014-07-31 more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-03-10 wenzelm 2014-03-10 tuned messages -- in accordance to Isabelle/Scala;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-05-31 haftmann 2013-05-31 combinator fold_range, corresponding to map_range
2013-05-14 wenzelm 2013-05-14 more uniform Markup.print_real;
2013-03-07 wenzelm 2013-03-07 tuned signature -- prefer terminology of Scala and Axiom;
2013-01-16 wenzelm 2013-01-16 eliminated dead code;
2012-12-30 wenzelm 2012-12-30 tuned whitespace;
2012-08-23 wenzelm 2012-08-23 prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2012-07-16 wenzelm 2012-07-16 replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
2012-04-16 wenzelm 2012-04-16 redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-19 wenzelm 2012-03-19 discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
2012-03-19 wenzelm 2012-03-19 moved some legacy stuff;
2012-03-12 wenzelm 2012-03-12 some support for grouped list operations;
2012-03-08 wenzelm 2012-03-08 tuned;
2012-03-03 wenzelm 2012-03-03 discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
2011-11-24 wenzelm 2011-11-24 more abstract datatype stamp, which avoids pointless allocation of mutable cells;
2011-09-01 wenzelm 2011-09-01 more flexible sorting; tuned display;
2011-07-13 wenzelm 2011-07-13 low-level tuning;
2011-07-04 wenzelm 2011-07-04 pervasive Basic_Library in Scala; tuned;
2011-06-30 wenzelm 2011-06-30 getenv_strict in ML; tuned;
2011-06-27 wenzelm 2011-06-27 old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-19 wenzelm 2011-04-19 slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
2011-01-12 wenzelm 2011-01-12 smart_string_of_real: print integer values without fractional part;
2011-01-10 wenzelm 2011-01-10 made SML/NJ happy;
2011-01-10 wenzelm 2011-01-10 tuned string_of_int to avoid allocation for small integers;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2010-12-03 wenzelm 2010-12-03 removed confusing comments (cf. 500171e7aa59);
2010-12-03 krauss 2010-12-03 really fixed comment (cf. 7abeb749ae99)
2010-12-03 bulwahn 2010-12-03 fixing comment in library
2010-11-27 wenzelm 2010-11-27 merged; adapted ListPair.UnequalLengths;
2010-11-26 haftmann 2010-11-26 strict forall2
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26 wenzelm 2010-11-26 just one version of fold_rev2;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-16 haftmann 2010-11-16 added forall2 predicate lifter
2010-11-12 wenzelm 2010-11-12 tuned signatures;
2010-11-03 wenzelm 2010-11-03 discontinued obsolete function sys_error and exception SYS_ERROR;
2010-10-30 wenzelm 2010-10-30 support for real valued configuration options;
2010-10-01 haftmann 2010-10-01 chop_while replace drop_while and take_while
2010-09-30 haftmann 2010-09-30 take_while, drop_while
2010-09-22 wenzelm 2010-09-22 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-07-20 wenzelm 2010-07-20 tuned;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-26 wenzelm 2010-03-26 tuned white space;
2009-12-09 haftmann 2009-12-09 take and drop as projections of chop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-10-26 haftmann 2009-10-26 avoid upto if not needed
2009-10-23 haftmann 2009-10-23 merged
2009-10-22 haftmann 2009-10-22 restored accidentally deleted submultiset