| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Mon, 10 Sep 2012 13:19:56 +0200 |
wenzelm |
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 22:10:27 +0200 |
wenzelm |
more accurate defining position of theory;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 20:47:33 +0200 |
wenzelm |
report source path and let front-end resolve implicit master location (e.g. URL);
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 13:05:14 +0200 |
wenzelm |
some markup for inlined files;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 14:58:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 13:55:27 +0200 |
wenzelm |
clarified type Token.file;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 12:33:42 +0200 |
wenzelm |
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 12:00:11 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 11:58:10 +0200 |
wenzelm |
simplified Thy_Load.provide: do not store full path;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 21:28:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 21:06:26 +0200 |
wenzelm |
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 21:02:02 +0200 |
wenzelm |
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 12:47:49 +0200 |
wenzelm |
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 12:17:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 11:56:13 +0200 |
wenzelm |
tuned errors;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 22:26:34 +0200 |
wenzelm |
prefer File.full_path in accordance to check_file;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 21:48:32 +0200 |
wenzelm |
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 20:32:33 +0200 |
wenzelm |
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 11:00:54 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2012 21:52:31 +0200 |
wenzelm |
more robust cleaning of "% tag" and "-- cmt";
|
file |
diff |
annotate
|
| Mon, 20 Aug 2012 17:05:53 +0200 |
wenzelm |
some support for inlining file content into outer syntax token language;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 14:42:11 +0100 |
wenzelm |
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 00:10:45 +0100 |
wenzelm |
some support for outer syntax keyword declarations within theory header;
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 16:02:14 +0100 |
wenzelm |
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
|
file |
diff |
annotate
|
| Wed, 29 Feb 2012 23:09:06 +0100 |
wenzelm |
clarified module Thy_Load;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
file |
diff |
annotate
|