☰

GitHub Editor - Change Default Settings

change default settings for the github editor

Ekde 2016/08/16. Vidu La ĝisdata versio. 

  1. // ==UserScript==
  2. // @name         GitHub Editor - Change Default Settings
  3. // @namespace    https://greatest.deepsurf.us/users/649
  4. // @version      1.0.6
  5. // @description  change default settings for the github editor
  6. // @author       Adrien Pyke
  7. // @match        *://github.com/*/new/*
  8. // @match        *://github.com/*/edit/*
  9. // @grant        GM_getValue
  10. // @grant        GM_setValue
  11. // @grant        GM_registerMenuCommand
  12. // ==/UserScript==
  13.  
  14. (function() {
  15. 	'use strict';
  16.  
  17. 	var loadConfig = function() {
  18. 		var defaults = {
  19. 			indentMode: 'tab',
  20. 			indentWidth: 4,
  21. 			wrapMode: 'off'
  22. 		};
  23.  
  24. 		var cfg = GM_getValue('cfg');
  25. 		if (!cfg) return defaults;
  26.  
  27. 		return JSON.parse(cfg);
  28. 	};
  29.  
  30. 	var saveConfig = function (cfg) {
  31. 		GM_setValue('cfg', JSON.stringify(cfg));
  32. 	};
  33.  
  34. 	var setup = function() {
  35. 		var createContainer = function() {
  36. 			var div = document.createElement('div');
  37. 			div.style.backgroundColor = 'white';
  38. 			div.style.padding = '5px';
  39. 			div.style.border = '1px solid black';
  40. 			div.style.position = 'fixed';
  41. 			div.style.top = '0';
  42. 			div.style.right = '0';
  43. 			return div;
  44. 		};
  45.  
  46. 		var createSelect = function(label, options, value) {
  47. 			var select = document.createElement('select');
  48. 			select.style.margin = '2px';
  49. 			var optgroup = document.createElement('optgroup');
  50. 			if (label) {
  51. 				optgroup.setAttribute('label', label);
  52. 			}
  53. 			select.appendChild(optgroup);
  54. 			options.forEach(function(opt) {
  55. 				var option = document.createElement('option');
  56. 				option.setAttribute('value', opt.value);
  57. 				option.textContent = opt.text;
  58. 				optgroup.appendChild(option);
  59. 			});
  60. 			select.value = value;
  61. 			return select;
  62. 		};
  63.  
  64. 		var createButton = function(text, onclick) {
  65. 			var button = document.createElement('button');
  66. 			button.style.margin = '2px';
  67. 			button.textContent = text;
  68. 			button.onclick = onclick;
  69. 			return button;
  70. 		};
  71.  
  72. 		var createLineBreak = function() {
  73. 			return document.createElement('br');
  74. 		};
  75.  
  76. 		var init = function(cfg) {
  77. 			var div = createContainer();
  78.  
  79. 			var indentMode = createSelect('Indent mode', [
  80. 				{ value: 'space', text: 'Spaces' },
  81. 				{ value: 'tab', text: 'Tabs' }
  82. 			], cfg.indentMode);
  83. 			div.appendChild(indentMode);
  84.  
  85. 			var indentWidth = createSelect('Indent size', [
  86. 				{ value: 2, text: 2 },
  87. 				{ value: 4, text: 4 },
  88. 				{ value: 8, text: 8 }
  89. 			], cfg.indentWidth);
  90. 			div.appendChild(indentWidth);
  91.  
  92. 			var wrapMode = createSelect('Line wrap mode', [
  93. 				{ value: 'off', text: 'No wrap' },
  94. 				{ value: 'on', text: 'Soft wrap' }
  95. 			], cfg.wrapMode);
  96. 			div.appendChild(wrapMode);
  97.  
  98. 			div.appendChild(createLineBreak());
  99.  
  100. 			div.appendChild(createButton('Save', function(e) {
  101. 				var settings = {
  102. 					indentMode: indentMode.value,
  103. 					indentWidth: indentWidth.value,
  104. 					wrapMode: wrapMode.value
  105. 				};
  106. 				saveConfig(settings);
  107. 				div.remove();
  108. 			}));
  109.  
  110. 			div.appendChild(createButton('Cancel', function(e) {
  111. 				div.remove();
  112. 			}));
  113.  
  114. 			document.body.appendChild(div);
  115. 		};
  116. 		init(loadConfig());
  117. 	};
  118.  
  119. 	var updateDropdown = function(dropdown, value) {
  120. 		dropdown.value = value;
  121. 		var evt = document.createEvent('HTMLEvents');
  122. 		evt.initEvent('change', false, true);
  123. 		dropdown.dispatchEvent(evt);
  124. 	};
  125.  
  126. 	var applySettings = function(cfg) {
  127. 		var indentMode = document.querySelector('.js-code-indent-mode');
  128. 		var indentWidth = document.querySelector('.js-code-indent-width');
  129. 		var wrapMode = document.querySelector('.js-code-wrap-mode');
  130.  
  131. 		if (location.href.match(/^https?:\/\/github.com\/[^\/]*\/[^\/]*\/new\/.*/)) {
  132. 			// new file
  133. 			updateDropdown(indentMode, cfg.indentMode);
  134. 			updateDropdown(indentWidth, cfg.indentWidth);
  135. 			updateDropdown(wrapMode, cfg.wrapMode);
  136. 		} else if (location.href.match(/^https?:\/\/github.com\/[^\/]*\/[^\/]*\/edit\/.*/)) {
  137. 			// edit file
  138. 			// if the file is using space indentation we don't want to change it
  139. 			if (indentMode.value === 'tab') {
  140. 				updateDropdown(indentWidth, cfg.indentWidth);
  141. 			}
  142. 			updateDropdown(wrapMode, cfg.wrapMode);
  143. 		}
  144. 	};
  145.  
  146. 	GM_registerMenuCommand('GitHub Editor Settings', setup);
  147. 	var settings = loadConfig();
  148. 	applySettings(settings);
  149. })();