on master help sign in
Insert spaces such that line breaks still happen. Fix string displaying in buttons.
3584556evancz
core-js/Value.js+35−8
@@ -32,14 +32,41 @@ var Value = function(){
32 return arr;
32 return arr;
33 };
33 };
34
34
35+ function makeSpaces(s) {
36+ var arr = s.split('');
37+ if (arr[0] == ' ') { arr[0] = " " }
38+ for (var i = arr.length; --i; ) {
39+ if (arr[i][0] == ' ' && arr[i-1] == ' ') {
40+ arr[i-1] = arr[i-1] + arr[i];
41+ arr[i] = '';
42+ }
43+ }
44+ for (var i = arr.length; i--; ) {
45+ if (arr[i].length > 1 && arr[i][0] == ' ') {
46+ var spaces = arr[i].split('');
47+ for (var j = spaces.length - 2; j >= 0; j -= 2) {
48+ spaces[j] = ' ';
49+ }
50+ arr[i] = spaces.join('');
51+ }
52+ }
53+ return arr.join('');
54+ }
55+
35− var properEscape = function(str) {
56+ function properEscape(str) {
57+ if (str.length == 0) return str;
36− return str.replace(/&/g, "&")
58+ str = str //.replace(/&/g, "&")
37− .replace(/"/g, /*"*/ """)
59+ .replace(/"/g, /*"*/ """)
38− .replace(/'/g, /*'*/ "'")
60+ .replace(/'/g, /*'*/ "'")
39− .replace(/</g, "&#60;")
61+ .replace(/</g, "&#60;")
40− .replace(/>/g, "&#62;")
62+ .replace(/>/g, "&#62;")
41− .replace(/\n/g, "<br/>");
63+ .replace(/\n/g, "<br/>");
64+ var arr = str.split('<br/>');
65+ for (var i = arr.length; i--; ) {
66+ arr[i] = makeSpaces(arr[i]);
42− };
67+ }
68+ return arr.join('<br/>');
69+ }
43
70
44 var toText = function(elmList) {
71 var toText = function(elmList) {
45 if (typeof elmList === "string") return properEscape(elmList);
72 if (typeof elmList === "string") return properEscape(elmList);
core-js/runtime/Signal.js+1−1
@@ -274,7 +274,7 @@ var Signal = function() {
274 var button = function(name) {
274 var button = function(name) {
275 var b = newElement('input');
275 var b = newElement('input');
276 b.type = "button";
276 b.type = "button";
277− b.value = Text.toText(name);
277+ b.value = Foreign.JavaScript.castStringToJSString(name);
278 var press = Elm.Input(false);
278 var press = Elm.Input(false);
279 addListener(b, 'click', function(e) {
279 addListener(b, 'click', function(e) {
280 Dispatcher.notify(press.id, true);
280 Dispatcher.notify(press.id, true);