Sat, 09 Nov 2013 11:24:21 +0100 tuned whitespace;
wenzelm [Sat, 09 Nov 2013 11:24:21 +0100] rev 54378
tuned whitespace;
Fri, 08 Nov 2013 17:34:37 +0100 added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm [Fri, 08 Nov 2013 17:34:37 +0100] rev 54377
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
Fri, 08 Nov 2013 15:10:16 +0100 transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
wenzelm [Fri, 08 Nov 2013 15:10:16 +0100] rev 54376
transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
Thu, 07 Nov 2013 19:35:57 +0100 Added tag Isabelle2013-1-RC4 for changeset 594628261376
wenzelm [Thu, 07 Nov 2013 19:35:57 +0100] rev 54375
Added tag Isabelle2013-1-RC4 for changeset 594628261376
Thu, 07 Nov 2013 19:17:53 +0100 updated to polyml-5.5.1-1 (fixes-5.5.1 version 1875);
wenzelm [Thu, 07 Nov 2013 19:17:53 +0100] rev 54374
updated to polyml-5.5.1-1 (fixes-5.5.1 version 1875);
Thu, 07 Nov 2013 13:38:44 +0100 tuned;
wenzelm [Thu, 07 Nov 2013 13:38:44 +0100] rev 54373
tuned;
Thu, 07 Nov 2013 13:34:04 +0100 misc tuning;
wenzelm [Thu, 07 Nov 2013 13:34:04 +0100] rev 54372
misc tuning;
Wed, 06 Nov 2013 21:20:20 +0100 updated to jedit_build-20131106 (Console.jar 5.1.3);
wenzelm [Wed, 06 Nov 2013 21:20:20 +0100] rev 54371
updated to jedit_build-20131106 (Console.jar 5.1.3);
Wed, 06 Nov 2013 20:58:11 +0100 join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm [Wed, 06 Nov 2013 20:58:11 +0100] rev 54370
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
Wed, 06 Nov 2013 20:46:00 +0100 tuned signature;
wenzelm [Wed, 06 Nov 2013 20:46:00 +0100] rev 54369
tuned signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip