add Ctrl-Enter hotkey

services/web/app/views/project/editor/editor.jade

@@ -26,7 +26,8 @@ div.full-size(
 			goto-line="editor.gotoLine",
 			resize-on="layout:main:resize,layout:pdf:resize",
 			annotations="pdf.logEntryAnnotations[editor.open_doc_id]",
-			read-only="!permissions.write"
+			read-only="!permissions.write",
+			on-ctrl-enter="recompile"
 		)
 
 	.ui-layout-east

services/web/public/coffee/ide/editor/directives/aceEditor.coffee

@@ -34,7 +34,8 @@ define [
 				text: "="
 				readOnly: "="
 				annotations: "="
-				navigateHighlights: "="
+				navigateHighlights: "=",
+				onCtrlEnter: "="
 			}
 			link: (scope, element, attrs) ->
 				# Don't freak out if we're already in an apply callback
@@ -77,6 +78,15 @@ define [
 					readOnly: true
 				editor.commands.removeCommand "replace"
 				
+				scope.$watch "onCtrlEnter", (callback) ->
+					if callback?
+						editor.commands.addCommand 
+							name: "compile",
+							bindKey: win: "Ctrl-Enter", mac: "Command-Enter"
+							exec: (editor) =>
+								callback()
+							readOnly: true
+
 				# Make '/' work for search in vim mode.
 				editor.showCommandLine = (arg) =>
 					if arg == "/"

services/web/public/coffee/ide/pdf/controllers/PdfController.coffee

@@ -108,6 +108,9 @@ define [
 					$scope.pdf.compiling = false
 					$scope.pdf.error = true
 					
+		# This needs to be public.
+		ide.$scope.recompile = $scope.recompile
+
 		$scope.clearCache = () ->
 			$http {
 				url: "/project/#{$scope.project_id}/output"