| .. | 
		
		
			
			
			
			
				| applies-to-line-widget.js | Change: switch to msg.js | 2018-10-06 13:27:58 +08:00 | 
		
			
			
			
			
				| beautify.js | Change: add sections-editor | 2018-10-09 23:38:29 +08:00 | 
		
			
			
			
			
				| codemirror-default.css | draw fold marks in CSS since some fonts may not have them | 2018-05-06 13:11:19 +03:00 | 
		
			
			
			
			
				| codemirror-default.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| codemirror-editing-hooks.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| codemirror-factory.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| colorpicker-helper.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| edit.css | Change: add sections-editor | 2018-10-09 23:38:29 +08:00 | 
		
			
			
			
			
				| edit.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| editor-worker-body.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| editor-worker.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| global-search.css | toggle narrow width mode tooltips via html+css; code cosmetics | 2017-12-19 02:48:47 +03:00 | 
		
			
			
			
			
				| global-search.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| linter-config-dialog.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| linter-defaults.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| linter-engines.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| linter-help-dialog.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| linter-meta.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| linter-report.js | Fix: switch to editor | 2018-10-10 00:41:07 +08:00 | 
		
			
			
			
			
				| linter.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 | 
		
			
			
			
			
				| live-preview.js | Add: preview error | 2018-10-08 20:12:39 +08:00 | 
		
			
			
			
			
				| match-highlighter-helper.js | match-highlighter: always use originalToken | 2017-12-18 10:27:50 +03:00 | 
		
			
			
			
			
				| regexp-tester.js | more things made focusable | 2017-12-13 07:38:36 +03:00 | 
		
			
			
			
			
				| reroute-hotkeys.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| sections-editor.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| show-keymap-help.js | off-by-one in showKeyMapHelp: text after <mark> was lost | 2017-12-09 20:43:47 +03:00 | 
		
			
			
			
			
				| source-editor.js | Add: codemirror-factory | 2018-10-10 14:49:37 +08:00 | 
		
			
			
			
			
				| util.js | Rewrite linter system (#487) | 2018-10-01 09:03:17 -05:00 |