src/Pure/Tools/find_consts.ML
Tue, 27 Nov 2018 21:07:39 +0100 wenzelm more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
Sun, 20 May 2018 11:57:17 +0200 wenzelm prefer HTTPS;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Sun, 10 Jul 2016 11:18:35 +0200 wenzelm tuned signature: more uniform Keyword.spec;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Mon, 04 Apr 2016 17:02:34 +0200 wenzelm clarified bootstrap -- more uniform use of ML files;
Tue, 06 Oct 2015 11:29:00 +0200 wenzelm pretty_const: proper local name space;
Mon, 21 Sep 2015 23:22:11 +0200 wenzelm clarified markup;
Mon, 06 Jul 2015 16:10:00 +0200 wenzelm plain string output, without funny control chars;
Mon, 06 Jul 2015 15:34:45 +0200 wenzelm proper outer syntax category, e.g. relevant for PIDE markup;
Mon, 29 Jun 2015 20:55:46 +0200 wenzelm improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Mon, 06 Apr 2015 16:00:19 +0200 wenzelm more position information and PIDE markup for command keywords;
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Thu, 06 Nov 2014 13:44:14 +0100 wenzelm tuned signature;
Wed, 05 Nov 2014 21:10:38 +0100 wenzelm more frugal keywords;
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Tue, 12 Aug 2014 20:18:27 +0200 wenzelm tuned signature according to Scala version -- prefer explicit argument;
Thu, 08 May 2014 16:15:20 +0200 wenzelm some position markup to help locating the query context, e.g. from "Info" dockable;
Thu, 08 May 2014 13:47:17 +0200 wenzelm tuned message: more compact, imitate actual command line;
Wed, 07 May 2014 10:24:32 +0200 wenzelm tuned message -- more context for detached window etc.;
Sun, 27 Apr 2014 13:35:18 +0200 wenzelm tuned;
Sat, 26 Apr 2014 22:43:22 +0200 wenzelm tuned message;
Sat, 26 Apr 2014 21:49:31 +0200 wenzelm PIDE support for find_consts;
Wed, 12 Mar 2014 14:37:14 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Thu, 18 Jul 2013 22:32:00 +0200 wenzelm tuned messages -- avoid text folds stemming from Pretty.chunks;
less more (0) -50 -30 tip