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;
less more (0) -10 -4 tip