more keyboard events tests.

[helm.git] / matitaB / matita / matitaweb.js

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 1bebb6d3028fb97f09459bbdaeb6b8c4859bd7cc..a03858ae728cf0291154e8eff253e783562e825c 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -122,6 +122,7 @@ function keypress(e)
          post = unlocked.innerHTML.substring(j);
          if (match == '\\to') {
              unlocked.innerHTML = pre + "-> " + post;
+            unlocked.focus();
             return suppressdefault(e,true);
          }
          else return suppressdefault(e,false);