src/Pure/System/options.scala
Sat, 05 Jun 2021 21:01:00 +0200 wenzelm clarified modules;
Mon, 17 May 2021 14:07:51 +0200 wenzelm clarified signature -- avoid odd warning about scala/bug#6675;
Mon, 17 May 2021 13:40:01 +0200 wenzelm clarified signature;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Wed, 20 Jan 2021 21:42:04 +0100 wenzelm proper message;
Sat, 28 Nov 2020 21:56:24 +0100 wenzelm added document antiquotation @{tool};
Mon, 05 Oct 2020 21:15:58 +0200 wenzelm clarified signature;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Wed, 28 Nov 2018 16:14:31 +0100 wenzelm clarified signature;
Wed, 26 Sep 2018 22:38:16 +0200 wenzelm tuned signature;
Wed, 26 Sep 2018 22:07:35 +0200 wenzelm tuned signature;
Wed, 29 Aug 2018 12:44:17 +0200 wenzelm clarified signature;
Tue, 13 Mar 2018 18:40:25 +0100 wenzelm tuned signature;
Tue, 13 Mar 2018 17:15:01 +0100 wenzelm more flexible preferences: avoid hardwired file;
Sun, 10 Dec 2017 20:29:00 +0100 wenzelm avoid println with its extra CR on Windows;
Sat, 04 Nov 2017 17:11:21 +0100 wenzelm clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
Wed, 01 Nov 2017 21:02:16 +0100 wenzelm init only once (see also c0f776b661fa);
Sat, 16 Sep 2017 16:19:34 +0200 wenzelm proper tool name (cf. c1410bcf6e87);
Tue, 14 Mar 2017 19:46:53 +0100 wenzelm afford early initialization of JEdit_Options, but it may lead to messy exception trace for malformed etc/preferences (see also 6eeaaefcea56);
Thu, 13 Oct 2016 11:54:06 +0200 wenzelm support for separate sub-system options, independent of main Isabelle options;
Tue, 11 Oct 2016 21:25:10 +0200 wenzelm tuned -- Date.Format.default used by toString;
Sun, 09 Oct 2016 14:19:46 +0200 wenzelm modernized;
Mon, 05 Sep 2016 22:09:52 +0200 wenzelm clarified modules;
Mon, 11 Jul 2016 16:36:29 +0200 wenzelm explicit kind "before_command";
Wed, 13 Apr 2016 17:00:02 +0200 wenzelm clarified syntax;
Sun, 03 Apr 2016 22:36:11 +0200 wenzelm prefer internal tool;
Sun, 28 Feb 2016 17:40:01 +0100 wenzelm tuned signature;
Sat, 27 Feb 2016 19:47:53 +0100 wenzelm moved getopts to Scala;
Thu, 21 Jan 2016 20:50:34 +0100 wenzelm clarified errors: more explicit treatment of uninitialized state;
less more (0) -50 -30 tip