Versuche mit dem Java-Compiler (in Arbeit)

ulrich

2017-03-14 d920b78320312112835e541012b17c54d0b843b3

 web/ui/ui.js

@@ -845,6 +845,7 @@
    lineNumbers: true,
    mode: m,
    viewportMargin : Infinity,
    tabSize: 2,
    extraKeys: {
        "F9": function(cm) {
        cm.setOption("fullScreen", !cm.getOption("fullScreen"));