wenzelm [Sat, 02 Aug 2014 16:35:59 +0200] rev 57842
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm [Sat, 02 Aug 2014 12:24:30 +0200] rev 57841
always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
wenzelm [Sat, 02 Aug 2014 11:39:13 +0200] rev 57840
tuned output;
wenzelm [Fri, 01 Aug 2014 22:52:53 +0200] rev 57839
prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
blanchet [Fri, 01 Aug 2014 15:08:49 +0200] rev 57838
careful when calling 'Thm.proof_body_of' -- it can throw exceptions
wenzelm [Fri, 01 Aug 2014 20:43:23 +0200] rev 57837
removed unused stuff;
wenzelm [Fri, 01 Aug 2014 20:20:17 +0200] rev 57836
agree on keyword categories with ML;
wenzelm [Fri, 01 Aug 2014 20:15:00 +0200] rev 57835
more keyword categories (as in ML);
wenzelm [Thu, 31 Jul 2014 22:02:21 +0200] rev 57834
prefer dynamic ML_print_depth if context happens to be available;
wenzelm [Thu, 31 Jul 2014 21:29:31 +0200] rev 57833
completion popup supports both ENTER and TAB (default);