src/Pure/PIDE/rendering.scala
Mon, 17 Apr 2017 12:11:02 +0200 wenzelm tuned signature;
Tue, 14 Mar 2017 10:49:07 +0100 wenzelm more robust debugger initialization, e.g. required for GUI components before actual session startup;
Mon, 13 Mar 2017 20:33:42 +0100 wenzelm proper local debugger state, depending on session;
Sat, 11 Mar 2017 22:19:22 +0100 wenzelm tuned;
Fri, 10 Mar 2017 21:47:48 +0100 wenzelm suppress irrelevant markup for VSCode;
Wed, 08 Mar 2017 10:29:40 +0100 wenzelm clarified rendering;
Wed, 08 Mar 2017 10:25:47 +0100 wenzelm tuned;
Tue, 07 Mar 2017 18:12:59 +0100 wenzelm tuned;
Tue, 07 Mar 2017 17:56:57 +0100 wenzelm more generic colors;
Tue, 07 Mar 2017 17:21:41 +0100 wenzelm tuned;
Tue, 07 Mar 2017 14:33:14 +0100 wenzelm clarified modules: spell-checker in Pure;
Mon, 06 Mar 2017 17:48:22 +0100 wenzelm more robust;
less more (0) -12 tip