| Wed, 24 Jan 2018 19:50:00 +0100 |
wenzelm |
tuned: prefer list operations over Source.source;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 22:36:02 +0100 |
wenzelm |
clarified implicit Pure.thy;
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 16:46:01 +0100 |
wenzelm |
PIDE markup for session ROOT files;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 22:13:05 +0200 |
wenzelm |
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 14:06:24 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:20:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 15:20:32 +0200 |
wenzelm |
more informative task_statistics;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2017 22:36:32 +0200 |
wenzelm |
more qualifier treatment, but in the end it is still ignored;
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 13:39:13 +0200 |
wenzelm |
simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 12:06:34 +0200 |
wenzelm |
more IDE support for Isabelle/Pure bootstrap;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 19:30:15 +0200 |
wenzelm |
support ROOT0.ML as well -- independently of ROOT.ML;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 23:45:19 +0200 |
wenzelm |
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 23:10:23 +0200 |
wenzelm |
thread context for exceptions from forks, e.g. relevant when printing errors;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 19:42:35 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 10 Aug 2015 20:22:49 +0200 |
wenzelm |
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
|
file |
diff |
annotate
|
| Fri, 24 Apr 2015 20:33:10 +0200 |
wenzelm |
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:23:36 +0200 |
wenzelm |
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 16:00:19 +0200 |
wenzelm |
more position information and PIDE markup for command keywords;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:21:41 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 14:15:15 +0100 |
wenzelm |
more precises positions;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 13:32:31 +0100 |
wenzelm |
avoid duplicate header errors, more precise positions;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2015 19:21:15 +0100 |
wenzelm |
hybrid use of command blobs: inlined errors and auxiliary files;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 12:58:49 +0100 |
wenzelm |
simplified Command.resolve_files in ML, using blobs_index from Scala;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2015 11:47:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2015 22:00:51 +0100 |
wenzelm |
clarified markup for embedded files, early before execution;
|
file |
diff |
annotate
|
| Sun, 11 Jan 2015 12:46:19 +0100 |
wenzelm |
more explicit errors;
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 20:51:42 +0100 |
wenzelm |
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
|
file |
diff |
annotate
|
| Sun, 28 Dec 2014 21:34:45 +0100 |
wenzelm |
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
|
file |
diff |
annotate
|