X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=4b99a23a286a471ca341f67c8fd4f4da25f3d8be;hb=33e69ace76c39b928f8c38a1130dc54fa2255889;hp=81995bb803ed42d8579f05d07d773ca252844b62;hpb=7a440dcd035d1e5cb009098a57d5d935bcd342cf;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 81995bb80..4b99a23a2 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -40,12 +40,124 @@ 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 string_of_key(n)
+{
+    if (n == null) return 'undefined';
+    return String.fromCharCode(n);
+}
+
+function pressmesg(w,e)
+{
+   debug(w + '  keyCode=' + keyval(e.keyCode) +
+                 ' which=' + keyval(e.which) +
+                 ' charCode=' + keyval(e.charCode) +
+		 '\n          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);
+   var s = string_of_key(e.charCode);
+   if (s == " ") {
+	j = getCursorPos();
+	i = unlocked.innerHTML.lastIndexOf('\\',j);
+       	if (i >= 0) {
+	  match = unlocked.innerHTML.substring(i,j);
+	  pre = unlocked.innerHTML.substring(0,i);
+	  post = unlocked.innerHTML.substring(j);
+	  if (match == '\\to') {
+             unlocked.innerHTML = pre + "-> " + post;
+	     unlocked.focus();
+             if (savedRange != null) {
+                 if (window.getSelection)//non IE and there is already a selection
+                 {
+                     var s = window.getSelection();
+                     if (s.rangeCount > 0) 
+                         s.removeAllRanges();
+                     s.addRange(savedRange);
+                 }
+                 else 
+                     if (document.createRange)//non IE and no selection
+                     {
+                         window.getSelection().addRange(savedRange);
+                     }
+                     else 
+                         if (document.selection)//IE
+                         {
+                             savedRange.select();
+                         }
+             }
+
+ 	     return suppressdefault(e,true);
+	  }
+	  else return suppressdefault(e,false);
+	}
+	else return suppressdefault(e,false);
+   } else {
+	return suppressdefault(e,false);
+   }
+}
+ 
 function debug(txt)
 {
         // internet explorer (v.9) doesn't work with innerHTML
+	// but google chrome's innerText is, in a sense, "write only"
+	// what should we do?
         logarea.innerText = txt + "\n" + logarea.innerText;
 }
 
@@ -447,6 +559,21 @@ function openFile()
 	callServer("open",processor,"file=" + escape(filename.value)); 
 }
 
+function retrieveFile(thefile)
+{ 
+	processor = function(xml)
+	{
+	        if (is_defined(xml)) {	
+	        	locked.innerHTML = "";
+	                unlocked.innerHTML = xml.documentElement.textContent;
+		} else {
+			debug("file open failed");
+		}
+	};
+	dialogBox.style.display = "none";
+	callServer("open",processor,"file=" + escape(thefile)); 
+}
+
 function showLibrary()
 { 
 	var req = null; 
@@ -511,19 +638,21 @@ function removeElement(id) {
   element.parentNode.removeChild(element);
 } 
 
+var savedRange;
+
 function getCursorPos() {
   var cursorPos;
   if (window.getSelection) {
     var selObj = window.getSelection();
-    var selRange = selObj.getRangeAt(0);
+    savedRange = selObj.getRangeAt(0);
     //cursorPos =  findNode(selObj.anchorNode.parentNode.childNodes, selObj.anchorNode) + selObj.anchorOffset;
     cursorPos =  findNode(unlocked.childNodes, selObj.anchorNode,0) + selObj.anchorOffset;
     /* FIXME the following works wrong in Opera when the document is longer than 32767 chars */
     return(cursorPos);
   }
   else if (document.selection) {
-    var range = document.selection.createRange();
-    var bookmark = range.getBookmark();
+    savedRange = document.selection.createRange();
+    var bookmark = savedRange.getBookmark();
     /* FIXME the following works wrong when the document is longer than 65535 chars */
     cursorPos = bookmark.charCodeAt(2) - 11; /* Undocumented function [3] */
     return(cursorPos);