Dateiverwaltung für die WebBox
ulrich
2017-03-14 7ad1b750afbefb9904ce31a192ed6192b72691ee
web/ui/ui.js
@@ -869,6 +869,9 @@
      },
        "Esc": function(cm) {
        if (cm.getOption("fullScreen")) cm.setOption("fullScreen", false);
      },
        ".": function(cm) {
        console.log('dot pressed: perhaps look up class or method name');
      }
    }
  });
@@ -883,6 +886,9 @@
    //var marker = info.gutterMarkers.breakpoints;
    //$(marker).tooltip('toggle');
  });
  cm.on("keyHandled", function(theEditor, keyName, event){
    console.log('cm.keyHandled keyName: ' + keyName + ', event.type: ' + event.type);
  });
}
function fm_set_code_marker(lineNumber, message) {