Mon, 07 Apr 2014 16:37:57 +0200 refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
wenzelm [Mon, 07 Apr 2014 16:37:57 +0200] rev 56450
refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
Mon, 07 Apr 2014 13:55:12 +0200 support for URL as file name, similar to treatment in jEdit.java;
wenzelm [Mon, 07 Apr 2014 13:55:12 +0200] rev 56449
support for URL as file name, similar to treatment in jEdit.java;
Mon, 07 Apr 2014 13:11:31 +0200 provide old-style ISABELLE_SCALA_SCRIPT for uniformity;
wenzelm [Mon, 07 Apr 2014 13:11:31 +0200] rev 56448
provide old-style ISABELLE_SCALA_SCRIPT for uniformity;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip