| Wed, 03 Jul 2013 21:32:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 17:50:47 +0200 |
wenzelm |
allow multiple print functions;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:58:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:19:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 15:19:36 +0200 |
wenzelm |
tuned;
|
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
|
| Sun, 24 Feb 2013 17:29:55 +0100 |
wenzelm |
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 19:45:32 +0100 |
wenzelm |
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
|
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
|
| Thu, 18 Oct 2012 12:00:27 +0200 |
wenzelm |
more official Future.terminate;
|
file |
diff |
annotate
|
| Wed, 05 Sep 2012 20:54:40 +0200 |
wenzelm |
eliminated potentially confusing terminology of Scala "layer";
|
file |
diff |
annotate
|
| Sun, 02 Sep 2012 14:02:05 +0200 |
wenzelm |
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2012 19:27:28 +0200 |
wenzelm |
central management of forked goals wrt. transaction id;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 21:23:04 +0200 |
wenzelm |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 19:18:49 +0200 |
wenzelm |
some support for registering forked proofs within Proof.state, using its bottom context;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 16:39:50 +0200 |
wenzelm |
tuned signature;
|
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 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 19:34:36 +0200 |
wenzelm |
vacuous execution after first malformed command;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 15:14:45 +0200 |
wenzelm |
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 20:54:01 +0200 |
wenzelm |
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 15:01:48 +0200 |
wenzelm |
simplified Document.Node.Header -- internalized errors;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 23:16:46 +0200 |
wenzelm |
improved interleaving of start_execution vs. cancel_execution of the next update;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:48:48 +0200 |
wenzelm |
always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:51:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 20:21:22 +0200 |
wenzelm |
builtin timing for main operations;
|
file |
diff |
annotate
|
| Wed, 11 Apr 2012 14:20:51 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Apr 2012 11:44:21 +0200 |
wenzelm |
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 20:42:17 +0200 |
wenzelm |
tuned future priorities: print 0, goal ~1, execute ~2;
|
file |
diff |
annotate
|