| Sat, 22 Feb 2014 15:07:33 +0100 |
wenzelm |
refined language context: antiquotes;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 16:55:54 +0100 |
wenzelm |
more markup -- complete symbols within antiquotation, notably with broken arguments;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 12:53:12 +0100 |
wenzelm |
completion of keywords and symbols based on language context;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 20:56:29 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 20:50:07 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 18:29:02 +0100 |
wenzelm |
more standard names for protocol and markup elements;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 17:03:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 16:34:02 +0100 |
wenzelm |
generic markup for embedded languages;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 11:14:26 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 18:28:18 +0100 |
wenzelm |
more uniform ML keyword markup;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 12:16:52 +0100 |
wenzelm |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 13:09:15 +0200 |
wenzelm |
cases: more position information and PIDE markup;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 22:15:45 +0200 |
wenzelm |
some protocol to determine provers according to ML;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 22:17:53 +0200 |
wenzelm |
more general Output.result: allow to update arbitrary properties;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 21:22:37 +0200 |
wenzelm |
less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 20:53:22 +0200 |
wenzelm |
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:25:42 +0200 |
wenzelm |
more explicit Markup.information for messages produced by "auto" tools;
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 13:17:22 +0200 |
wenzelm |
tuned protocol terminology;
|
file |
diff |
annotate
|
| Wed, 22 May 2013 14:10:45 +0200 |
wenzelm |
explicit management of Session.Protocol_Handlers, with protocol state and functions;
|
file |
diff |
annotate
|
| Tue, 14 May 2013 20:46:09 +0200 |
wenzelm |
more uniform Markup.print_real;
|
file |
diff |
annotate
|
| Tue, 14 May 2013 19:48:31 +0200 |
wenzelm |
more uniform Markup.parse_real;
|
file |
diff |
annotate
|
| Sun, 12 May 2013 20:46:17 +0200 |
wenzelm |
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 21:14:00 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2013 20:43:43 +0200 |
wenzelm |
unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 21:48:43 +0200 |
wenzelm |
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 15:36:45 +0100 |
wenzelm |
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
|
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 13:57:13 +0100 |
wenzelm |
support for build passing timings from Scala to ML;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 12:58:32 +0100 |
wenzelm |
support for prescient timing information within command transactions;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 10:55:11 +0100 |
wenzelm |
emit command_timing properties into build log;
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 17:51:50 +0100 |
wenzelm |
more systematic task statistics;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 20:41:29 +0100 |
wenzelm |
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 15:00:48 +0100 |
wenzelm |
immediate theory progress for build_dialog;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 14:47:17 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Jan 2013 13:38:57 +0100 |
wenzelm |
standardized treatment of timing properties;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 12:33:25 +0100 |
wenzelm |
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 13:50:59 +0100 |
wenzelm |
inline ML statistics into build log;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 12:55:11 +0100 |
wenzelm |
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 12:28:37 +0100 |
wenzelm |
fold main goal;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 20:05:08 +0100 |
wenzelm |
more subgoal markup information, which is potentially useful to manage proof state output;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 18:00:24 +0100 |
wenzelm |
enable Isabelle/ML to produce uninterpreted result messages as well;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:52:18 +0100 |
wenzelm |
identify dialogs via official serial and maintain as result message;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 23:36:07 +0100 |
wenzelm |
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:50:42 +0100 |
wenzelm |
support dialog via document content;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 17:18:53 +0100 |
wenzelm |
some support for ML runtime statistics;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
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
|
| Tue, 13 Mar 2012 11:21:26 +0100 |
wenzelm |
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 21:50:00 +0100 |
wenzelm |
clarified Time vs. Timing;
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 19:49:36 +0100 |
wenzelm |
rearranged files;
|
file |
diff |
annotate
| base
|