# HG changeset patch # User Adam Chlipala # Date 1342184461 14400 # Node ID 25824a0e8bf141e7c459d9a0020238717483bd90 # Parent 85a87f155e7b7c7d1b4b117422e8e407d8b5f438 Change propagation of source value to textarea diff -r 85a87f155e7b -r 25824a0e8bf1 lib/js/urweb.js --- a/lib/js/urweb.js Sat Jun 23 10:11:33 2012 -0400 +++ b/lib/js/urweb.js Fri Jul 13 09:01:01 2012 -0400 @@ -937,7 +937,7 @@ function tbx(s) { var x = input(document.createElement("textarea"), s, - function(x) { return function(v) { if (x.innerHTML != v) x.innerHTML = v; }; }); + function(x) { return function(v) { if (x.value != v) x.value = v; }; }); x.innerHTML = s.data; x.onkeyup = x.oninput = x.onchange = x.onpropertychange = function() { sv(s, x.value) };