src/Pure/General/input.ML
Mon, 07 Dec 2020 15:54:07 +0100 wenzelm tuned signature --- more operations;
Fri, 14 Dec 2018 11:47:53 +0100 wenzelm unused;
Mon, 10 Dec 2018 22:38:03 +0100 wenzelm tuned signature;
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;
Sat, 03 Feb 2018 13:54:04 +0100 wenzelm clarified overall range: include delimiters;
Sat, 16 Dec 2017 15:11:19 +0100 wenzelm more operations;
Wed, 30 Mar 2016 14:52:23 +0200 wenzelm more operations;
Tue, 29 Mar 2016 21:17:29 +0200 wenzelm more position information for type mixfix;
Tue, 09 Dec 2014 18:29:45 +0100 wenzelm tuned signature;
Sun, 30 Nov 2014 13:15:04 +0100 wenzelm tuned signature;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
less more (0) tip