| Wed, 13 Mar 2013 21:25:08 +0100 |
wenzelm |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
|
file |
diff |
annotate
|
| Mon, 04 Mar 2013 15:03:46 +0100 |
wenzelm |
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
|
file |
diff |
annotate
|
| Mon, 04 Mar 2013 11:36:16 +0100 |
wenzelm |
join all proofs before scheduling present phase (ordered according to weight);
|
file |
diff |
annotate
|
| Sun, 03 Mar 2013 18:50:46 +0100 |
wenzelm |
prefer more systematic Future.flat;
|
file |
diff |
annotate
|
| Sun, 03 Mar 2013 13:43:57 +0100 |
wenzelm |
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 16:27:44 +0100 |
wenzelm |
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 12:45:19 +0100 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:52:27 +0100 |
wenzelm |
clarified Toplevel.element_result: scheduling policies happen here;
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 17:29:55 +0100 |
wenzelm |
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 15:22:22 +0100 |
wenzelm |
more tight representation of command timing;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 12:58:32 +0100 |
wenzelm |
support for prescient timing information within command transactions;
|
file |
diff |
annotate
|
| 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
|
| Sun, 21 Aug 2011 14:16:44 +0200 |
wenzelm |
discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 13:42:55 +0200 |
wenzelm |
discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 21:44:47 +0200 |
wenzelm |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 14:37:19 +0200 |
wenzelm |
more abstract Thy_Load.load_file/use_file for external theory resources;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 11:50:58 +0200 |
wenzelm |
clarified Thy_Load.digest_file -- read ML files only once;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 17:40:45 +0100 |
wenzelm |
replaced File.check by specific File.check_file, File.check_dir;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 13:49:21 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 20:56:00 +0100 |
wenzelm |
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 18:10:28 +0100 |
wenzelm |
discontinued legacy load path;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 13:58:07 +0100 |
wenzelm |
Thy_Load.begin_theory: maintain source specification of imports;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 18:18:42 +0100 |
wenzelm |
theory loader: implicit load path is considered legacy;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 13:51:17 +0100 |
wenzelm |
check_file: secondary load path is legacy feature;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 14:32:08 +0100 |
wenzelm |
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 14:19:04 +0100 |
wenzelm |
moved file identification to thy_load.ML (where it is actually used);
|
file |
diff |
annotate
|
| Fri, 19 Nov 2010 21:14:12 +0100 |
wenzelm |
do not export Thy_Load.required, to avoid confusion about the interface;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 15:48:08 +0200 |
wenzelm |
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|