src/Pure/library.ML
7 months ago wenzelm 2018-11-05 tuned (see map_index);
13 months ago wenzelm 2018-05-11 unused;
13 months ago wenzelm 2018-05-05 hexadecimal representation of byte string;
17 months ago wenzelm 2018-02-01 tuned signature: more operations;
17 months ago wenzelm 2018-01-28 clarified take/drop/chop prefix/suffix;
17 months ago wenzelm 2018-01-28 clarified signature;
18 months ago wenzelm 2017-12-10 clean log file on Windows;
20 months ago wenzelm 2017-10-26 use Poly/ML 5.7.1 test version as default;
2017-05-26 wenzelm 2017-05-26 store errors in build db;
2017-05-22 wenzelm 2017-05-22 permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
2016-10-17 wenzelm 2016-10-17 accomodate Poly/ML repository version, which treats singleton strings as boxed;
2016-06-14 haftmann 2016-06-14 non-deprecated char literals for Scala
2016-04-09 wenzelm 2016-04-09 clarified modules;
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-03-07 wenzelm 2016-03-07 discontinued cd, pwd;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2016-03-01 wenzelm 2016-03-01 clarified modules;
2016-02-29 wenzelm 2016-02-29 clarified modules;
2015-11-19 wenzelm 2015-11-19 tuned;
2015-08-18 wenzelm 2015-08-18 clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations); avoid patching of SML basis library;
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
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)