Wed, 22 Aug 2012 22:47:16 +0200 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm [Wed, 22 Aug 2012 22:47:16 +0200] rev 48890
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
Wed, 22 Aug 2012 21:43:17 +0200 add keywords of this node as well (e.g. relevant for Pure.thy);
wenzelm [Wed, 22 Aug 2012 21:43:17 +0200] rev 48889
add keywords of this node as well (e.g. relevant for Pure.thy);
Wed, 22 Aug 2012 21:28:33 +0200 tuned;
wenzelm [Wed, 22 Aug 2012 21:28:33 +0200] rev 48888
tuned;
Wed, 22 Aug 2012 21:06:26 +0200 tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
wenzelm [Wed, 22 Aug 2012 21:06:26 +0200] rev 48887
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
Wed, 22 Aug 2012 21:02:02 +0200 discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm [Wed, 22 Aug 2012 21:02:02 +0200] rev 48886
discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;
Wed, 22 Aug 2012 18:04:30 +0200 find files via load commands within theory text;
wenzelm [Wed, 22 Aug 2012 18:04:30 +0200] rev 48885
find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip