src/Pure/Isar/args.ML
Sat, 20 May 2023 17:18:44 +0200 wenzelm tuned signature;
Thu, 18 May 2023 17:21:29 +0200 wenzelm clarified signature: more explicit types;
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Wed, 20 Oct 2021 20:25:33 +0200 wenzelm clarified modules;
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;
Mon, 23 May 2016 21:30:30 +0200 wenzelm embedded content may be delimited via cartouches;
Wed, 09 Dec 2015 16:36:26 +0100 wenzelm clarified type Token.src: plain token list, with usual implicit value assignment;
Thu, 25 Jun 2015 16:56:04 +0200 wenzelm tuned signature;
Mon, 30 Mar 2015 20:51:11 +0200 wenzelm tuned signature;
Wed, 25 Mar 2015 11:39:52 +0100 wenzelm tuned signature;
Tue, 10 Mar 2015 13:55:10 +0100 wenzelm clarified Token.check_src: intern at most once;
Sun, 08 Mar 2015 13:45:11 +0100 wenzelm cartouche_declaration for Eisbach;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
Wed, 20 Aug 2014 17:23:47 +0200 wenzelm support for declaration within token source;
Wed, 20 Aug 2014 11:05:41 +0200 wenzelm support for nested Token.src within Token.T;
less more (0) -100 -15 tip