Testing keyboard events handling.

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index a5c58c3a2e7995f3e85f668d53386fe4941c47fb..d0b5ce21768f22ae8ffaf6671f68fc2e8779a10d 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -40,9 +40,75 @@ function initialize()
   
     // hide sequent view at start
     hideSequent();
+
+    // initialize keyboard events in the unlocked script
+    init_keyboard(unlocked);
   }
 }
 
+function init_keyboard(target)
+{
+    if (target.addEventListener)
+    {
+//       target.addEventListener("keydown",keydown,false);
+       target.addEventListener("keypress",keypress,false);
+//       target.addEventListener("keyup",keyup,false);
+//       target.addEventListener("textInput",textinput,false);
+    }
+    else if (target.attachEvent)
+    {
+//       target.attachEvent("onkeydown", keydown);
+       target.attachEvent("onkeypress", keypress);
+//       target.attachEvent("onkeyup", keyup);
+//       target.attachEvent("ontextInput", textinput);
+    }
+    else
+    {
+//       target.onkeydown= keydown;
+       target.onkeypress= keypress;
+//       target.onkeyup= keyup;
+//       target.ontextinput= textinput;   // probably doesn't work
+    }
+ 
+}
+
+function keyval(n)
+{
+    if (n == null) return 'undefined';
+    var s= '' + n;
+    if (n >= 32 && n < 127) s+= ' (' + String.fromCharCode(n) + ')';
+    while (s.length < 9) s+= ' ';
+    return s;
+}
+ 
+function pressmesg(w,e)
+{
+   debug(w + '  keyCode=' + keyval(e.keyCode) +
+                 ' which=' + keyval(e.which) +
+                 ' charCode=' + keyval(e.charCode));
+   debug('          shiftKey='+e.shiftKey
+             + ' ctrlKey='+e.ctrlKey
+             + ' altKey='+e.altKey
+             + ' metaKey='+e.metaKey);
+}
+ 
+function suppressdefault(e,flag)
+{
+   if (flag)
+   {
+       if (e.preventDefault) e.preventDefault();
+       if (e.stopPropagation) e.stopPropagation();
+   }
+   return !flag;
+}
+ 
+function keypress(e)
+{
+   if (!e) e= event;
+   pressmesg('keypress',e);
+   return suppressdefault(e,/*document.testform.keypress.checked*/ false);
+}
+ 
 function debug(txt)
 {
         // internet explorer (v.9) doesn't work with innerHTML