| Wed, 10 Dec 2014 13:45:44 +0100 |
wenzelm |
more explicit markup for improper commands;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 11:37:51 +0100 |
wenzelm |
clarified token kind;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:09:18 +0100 |
wenzelm |
removed pointless markup;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:10:11 +0100 |
wenzelm |
discontinued obsolete tty and prompt;
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 17:58:36 +0200 |
wenzelm |
citation tooltip/hyperlink based on open buffers with .bib files;
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 16:05:17 +0200 |
wenzelm |
bibtex support in ML: document antiquotation @{cite} with markup;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 15:05:11 +0200 |
wenzelm |
support for sub-expression markup;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 14:54:32 +0200 |
wenzelm |
more explicit Method.modifier with reported position;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2014 13:39:59 +0200 |
wenzelm |
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
|
file |
diff |
annotate
|
| Mon, 21 Jul 2014 17:37:22 +0200 |
wenzelm |
regular message to refer to Simplifier Trace panel (unused);
|
file |
diff |
annotate
|
| Mon, 05 May 2014 15:17:07 +0200 |
wenzelm |
support print operations as asynchronous query;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:07:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 23:42:25 +0200 |
wenzelm |
manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 19:52:02 +0200 |
wenzelm |
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
|
file |
diff |
annotate
|
| Thu, 17 Apr 2014 13:21:36 +0200 |
wenzelm |
added protocol command "use_theories", with core functionality of batch build;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:46:54 +0200 |
wenzelm |
markup for prose words within formal comments;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:15:48 +0200 |
wenzelm |
more positions and markup;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:11:00 +0100 |
wenzelm |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 12:25:17 +0100 |
wenzelm |
more markup for improper elements;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 21:15:29 +0100 |
wenzelm |
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 20:27:08 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 16:12:26 +0100 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 16:13:24 +0100 |
wenzelm |
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 13:11:08 +0100 |
wenzelm |
clarified init_assignable: make double-sure that initial values are reset;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 19:00:45 +0100 |
wenzelm |
clarified names of antiquotations and markup;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:40:13 +0100 |
wenzelm |
method language markup, e.g. relevant to prevent outer keyword completion;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 21:32:26 +0100 |
wenzelm |
back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 17:03:55 +0100 |
wenzelm |
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 21:11:59 +0100 |
wenzelm |
clarified semantic completion: retain kind.full_name as official item name for history;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 14:39:51 +0100 |
wenzelm |
clarified completion names;
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 20:52:43 +0100 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
| 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
|