| Tue, 29 Aug 2023 15:34:45 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 12:53:28 +0200 |
wenzelm |
misc tuning: support "scalac -source 3.3";
|
file |
diff |
annotate
|
| Sun, 18 Dec 2022 16:01:37 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 15:05:28 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 13:45:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2017 17:01:51 +0200 |
wenzelm |
more permissive: avoid situations where query is silently ignored;
|
file |
diff |
annotate
|
| Fri, 16 Jun 2017 15:59:27 +0200 |
wenzelm |
more general dispatcher operations;
|
file |
diff |
annotate
|
| Sun, 12 Mar 2017 13:48:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2016 16:20:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 22:09:52 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 18:31:57 +0100 |
wenzelm |
avoid premature flushing and thus flashing of text area;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 18:09:14 +0100 |
wenzelm |
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 15:55:29 +0200 |
wenzelm |
support for auto update via caret focus;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 13:53:35 +0200 |
wenzelm |
more specific name to reduce danger of clash with direct uses of plain Command.print_function;
|
file |
diff |
annotate
|
| Tue, 11 Aug 2015 17:00:16 +0200 |
wenzelm |
support hyperlinks with optional focus change;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 12:51:08 +0200 |
wenzelm |
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2014 23:49:15 +0200 |
wenzelm |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 20:22:12 +0200 |
wenzelm |
more explicit iterator terminology, in accordance to Scala 2.8 library;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 10:43:43 +0100 |
wenzelm |
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 14:36:17 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:55:29 +0100 |
wenzelm |
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2013 23:12:04 +0200 |
wenzelm |
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2013 20:45:21 +0200 |
wenzelm |
clarified Editor.current_command: allow outdated snapshot;
|
file |
diff |
annotate
|
| Mon, 07 Oct 2013 12:28:19 +0200 |
wenzelm |
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 11:12:59 +0200 |
wenzelm |
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:35:01 +0200 |
wenzelm |
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 14:09:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 11:57:42 +0200 |
wenzelm |
more cleanup;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 17:17:49 +0200 |
wenzelm |
moved generic module to its proper place;
|
file |
diff |
annotate
| base
|