Wed, 22 Aug 2012 16:24:52 +0200 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm [Wed, 22 Aug 2012 16:24:52 +0200] rev 48884
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
Wed, 22 Aug 2012 16:10:23 +0200 pass syntax through check_thy;
wenzelm [Wed, 22 Aug 2012 16:10:23 +0200] rev 48883
pass syntax through check_thy;
Wed, 22 Aug 2012 15:53:17 +0200 use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
wenzelm [Wed, 22 Aug 2012 15:53:17 +0200] rev 48882
use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;
Wed, 22 Aug 2012 12:47:49 +0200 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
wenzelm [Wed, 22 Aug 2012 12:47:49 +0200] rev 48881
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
Wed, 22 Aug 2012 12:17:55 +0200 tuned;
wenzelm [Wed, 22 Aug 2012 12:17:55 +0200] rev 48880
tuned;
Wed, 22 Aug 2012 12:07:11 +0200 clarified bootstrapping of Pure;
wenzelm [Wed, 22 Aug 2012 12:07:11 +0200] rev 48879
clarified bootstrapping of Pure;
Wed, 22 Aug 2012 11:56:13 +0200 tuned errors;
wenzelm [Wed, 22 Aug 2012 11:56:13 +0200] rev 48878
tuned errors;
Tue, 21 Aug 2012 22:26:34 +0200 prefer File.full_path in accordance to check_file;
wenzelm [Tue, 21 Aug 2012 22:26:34 +0200] rev 48877
prefer File.full_path in accordance to check_file;
Tue, 21 Aug 2012 21:48:32 +0200 more standard Thy_Load.check_thy for Pure.thy, relying on its header;
wenzelm [Tue, 21 Aug 2012 21:48:32 +0200] rev 48876
more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;
Tue, 21 Aug 2012 21:25:45 +0200 updated Thy_Load.check_thy;
wenzelm [Tue, 21 Aug 2012 21:25:45 +0200] rev 48875
updated Thy_Load.check_thy;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip