src/Pure/PIDE/query_operation.scala
Thu, 07 Nov 2024 20:08:50 +0100 wenzelm clarified signature;
Tue, 29 Aug 2023 15:34:45 +0200 wenzelm clarified signature: prefer enum types;
Tue, 29 Aug 2023 12:53:28 +0200 wenzelm misc tuning: support "scalac -source 3.3";
Sun, 18 Dec 2022 16:01:37 +0100 wenzelm clarified signature;
Wed, 31 Aug 2022 15:05:28 +0200 wenzelm clarified signature;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sat, 05 Dec 2020 13:45:09 +0100 wenzelm tuned signature;
Sat, 17 Jun 2017 17:01:51 +0200 wenzelm more permissive: avoid situations where query is silently ignored;
Fri, 16 Jun 2017 15:59:27 +0200 wenzelm more general dispatcher operations;
Sun, 12 Mar 2017 13:48:10 +0100 wenzelm tuned;
Fri, 23 Dec 2016 16:20:42 +0100 wenzelm tuned;
Mon, 05 Sep 2016 22:09:52 +0200 wenzelm clarified modules;
Mon, 02 Nov 2015 18:31:57 +0100 wenzelm avoid premature flushing and thus flashing of text area;
Mon, 02 Nov 2015 18:09:14 +0100 wenzelm clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
less more (0) -15 tip