1 dump('entering symbol/clipboard.js\n');
3 function $(id) { return document.getElementById(id); }
9 dojo.query('.plain').forEach(function(node,index,arr){
10 node.addEventListener("keypress", function(event) {
11 if (event.charCode == 115 && event.ctrlKey){
13 $('symbol-panel').openPopup(node, 'after_pointer' );
26 $('symbol-panel').hidePopup();
29 if (n.getAttribute('readonly')=='true') return;
32 var start = n.selectionStart;
33 var end = n.selectionEnd;
34 n.value = v.substring(0, start) + ins + v.substring(end, v.length);
35 n.setSelectionRange(start + ins.length,start + ins.length);