src/Pure/System/options.scala
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;
Thu, 05 Nov 2015 00:02:30 +0100 wenzelm symbolic syntax "\<comment> text";
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Sat, 18 Apr 2015 23:43:30 +0200 wenzelm clarified keywords for quasi-command spans and Sidekick structure;
Wed, 25 Mar 2015 13:45:52 +0100 wenzelm clarified position;
Sun, 15 Mar 2015 20:35:47 +0100 wenzelm clarified span position;
Sat, 14 Mar 2015 16:56:11 +0100 wenzelm position parser as in ML;
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Thu, 13 Nov 2014 23:45:15 +0100 wenzelm uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
Wed, 05 Nov 2014 22:17:05 +0100 wenzelm tuned signature;
Sun, 02 Nov 2014 15:27:37 +0100 wenzelm uniform heading commands work in any context, even in theory header;
Fri, 02 May 2014 20:01:45 +0200 wenzelm prefer scala.Console with its support for thread-local redirection;
Tue, 22 Apr 2014 12:30:54 +0200 wenzelm tuned;
Thu, 17 Apr 2014 10:54:10 +0200 wenzelm capitalize more carefully, e.g. relevant for option "ML_exception_trace";
Wed, 16 Apr 2014 11:52:26 +0200 wenzelm more specific support for sequence of words;
Wed, 16 Apr 2014 09:38:40 +0200 wenzelm tuned signature -- separate module Word;
Sun, 13 Apr 2014 16:42:44 +0200 wenzelm added dictionaries_selector GUI;
Sat, 12 Apr 2014 21:38:38 +0200 wenzelm some case-mangling;
Tue, 08 Apr 2014 14:15:48 +0200 wenzelm more positions and markup;
Thu, 20 Feb 2014 14:36:17 +0100 wenzelm tuned imports;
less more (0) -50 -30 tip