| Tue, 12 Aug 2014 13:18:17 +0200 |
wenzelm |
more compact representation of special string values;
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 15:45:06 +0200 |
wenzelm |
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
|
file |
diff |
annotate
|
| Thu, 31 Jul 2014 20:09:30 +0200 |
wenzelm |
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 22:14:53 +0100 |
wenzelm |
tuned messages -- in accordance to Isabelle/Scala;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Fri, 31 May 2013 09:30:32 +0200 |
haftmann |
combinator fold_range, corresponding to map_range
|
file |
diff |
annotate
|
| Tue, 14 May 2013 20:46:09 +0200 |
wenzelm |
more uniform Markup.print_real;
|
file |
diff |
annotate
|
| Thu, 07 Mar 2013 15:02:55 +0100 |
wenzelm |
tuned signature -- prefer terminology of Scala and Axiom;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 20:40:50 +0100 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 16:33:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 13:03:29 +0200 |
wenzelm |
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
|
file |
diff |
annotate
|
| Mon, 16 Jul 2012 15:57:21 +0200 |
wenzelm |
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 23:07:40 +0200 |
wenzelm |
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;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:00:34 +0100 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:16:19 +0100 |
wenzelm |
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:10:33 +0100 |
wenzelm |
moved some legacy stuff;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 23:16:02 +0100 |
wenzelm |
some support for grouped list operations;
|
file |
diff |
annotate
|
| Thu, 08 Mar 2012 21:35:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 22:27:30 +0100 |
wenzelm |
discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:15:20 +0100 |
wenzelm |
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 14:10:52 +0200 |
wenzelm |
more flexible sorting;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 20:13:27 +0200 |
wenzelm |
low-level tuning;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2011 16:51:45 +0200 |
wenzelm |
pervasive Basic_Library in Scala;
|
file |
diff |
annotate
|
| Thu, 30 Jun 2011 13:59:55 +0200 |
wenzelm |
getenv_strict in ML;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 15:03:55 +0200 |
wenzelm |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 15:58:05 +0200 |
wenzelm |
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
|
file |
diff |
annotate
|
| Wed, 12 Jan 2011 14:07:29 +0100 |
wenzelm |
smart_string_of_real: print integer values without fractional part;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:56:47 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:07:16 +0100 |
wenzelm |
tuned string_of_int to avoid allocation for small integers;
|
file |
diff |
annotate
|