src/Tools/jEdit/src/rendering.scala
Tue, 01 Apr 2014 17:26:32 +0200 wenzelm more frugal command_status, which is often used in a tight loop;
Thu, 27 Mar 2014 10:43:43 +0100 wenzelm more careful treatment of multiple command states (eval + prints): merge content that is actually required;
Wed, 26 Mar 2014 21:01:09 +0100 wenzelm tuned signature -- expose less intermediate information;
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Tue, 18 Mar 2014 12:25:17 +0100 wenzelm more markup for improper elements;
Mon, 17 Mar 2014 14:37:23 +0100 wenzelm tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;
Mon, 17 Mar 2014 12:24:00 +0100 wenzelm tuned signature;
Fri, 14 Mar 2014 15:41:29 +0100 wenzelm discontinued somewhat pointless "thy_script" keyword kind;
Thu, 13 Mar 2014 10:34:48 +0100 wenzelm clarified Path.smart_implode;
Wed, 12 Mar 2014 16:43:17 +0100 wenzelm clarified Markup.operator vs. Markup.delimiter;
Wed, 12 Mar 2014 16:11:47 +0100 wenzelm more explicit markup for Token.Literal;
Fri, 07 Mar 2014 14:37:25 +0100 wenzelm more detailed description of completion items;
Wed, 05 Mar 2014 16:13:24 +0100 wenzelm more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
Wed, 05 Mar 2014 13:11:08 +0100 wenzelm clarified init_assignable: make double-sure that initial values are reset;
Mon, 03 Mar 2014 12:24:14 +0100 wenzelm recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
Mon, 03 Mar 2014 11:58:07 +0100 wenzelm clarified path checks: avoid crash of rendering due to spurious errors;
Mon, 03 Mar 2014 11:37:06 +0100 wenzelm more precise navigation within open files;
Mon, 03 Mar 2014 10:59:33 +0100 wenzelm tuned signature;
Mon, 03 Mar 2014 10:41:58 +0100 wenzelm tuned signature;
Sun, 02 Mar 2014 19:00:45 +0100 wenzelm clarified names of antiquotations and markup;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Sat, 01 Mar 2014 19:39:27 +0100 wenzelm tuned signature -- separate module Font_Info;
Sat, 01 Mar 2014 18:33:49 +0100 wenzelm tuned;
Sat, 01 Mar 2014 16:34:30 +0100 wenzelm font size change with delay, to avoid GUI lagging behind user input;
Sat, 01 Mar 2014 12:07:26 +0100 wenzelm tuned signature -- more explicit Document.Elements;
Thu, 27 Feb 2014 17:56:59 +0100 wenzelm simplified rendering -- no need to over-emphasize "token_range";
Wed, 26 Feb 2014 11:58:35 +0100 wenzelm markup for method combinators;
Tue, 25 Feb 2014 20:57:57 +0100 wenzelm tuned signature;
Tue, 25 Feb 2014 20:15:47 +0100 wenzelm more completion rendering: active, semantic, syntactic;
less more (0) -100 -50 -30 tip