X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=fb6c0869da5b9c6afac25648187987195215b07c;hb=d8bc6fd4ab18f2995624c75e2889318237e9c17f;hp=8f77fe4f8d2eec714805d2afc63067b99a77c76e;hpb=9be9c82d734036f15089a4f6338c8a6e127a8523;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 8f77fe4f8..fb6c0869d 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -11,31 +11,172 @@ var advanceButton;
 var retractButton;
 var cursorButton;
 var bottomButton;
+var dialogBox;
+var dialogTitle;
+var dialogContent;
 var metasenv = "";
 
 function initialize()
 {
-  locked = document.getElementById("locked");
-  unlocked = document.getElementById("unlocked");
-  workarea = document.getElementById("workarea");
-  scriptcell = document.getElementById("scriptcell");
-  goalcell = document.getElementById("goalcell");
-  goals = document.getElementById("goals");
-  goalview = document.getElementById("goalview");
-  filename = document.getElementById("filename");
-  logarea = document.getElementById("logarea");
-  advanceButton = document.getElementById("advance");
-  retractButton = document.getElementById("retract");
-  cursorButton = document.getElementById("cursor");
-  bottomButton = document.getElementById("bottom");
+  if (readCookie("session") == null) {
+    window.location = "/login.html"
+  } else {
+    locked = document.getElementById("locked");
+    unlocked = document.getElementById("unlocked");
+    workarea = document.getElementById("workarea");
+    scriptcell = document.getElementById("scriptcell");
+    goalcell = document.getElementById("goalcell");
+    goals = document.getElementById("goals");
+    goalview = document.getElementById("goalview");
+    filename = document.getElementById("filename");
+    logarea = document.getElementById("logarea");
+    advanceButton = document.getElementById("advance");
+    retractButton = document.getElementById("retract");
+    cursorButton = document.getElementById("cursor");
+    bottomButton = document.getElementById("bottom");
+    dialogBox = document.getElementById("dialogBox");
+    dialogTitle = document.getElementById("dialogTitle");
+    dialogContent = document.getElementById("dialogContent");
+  
+    // hide sequent view at start
+    hideSequent();
+
+    // initialize keyboard events in the unlocked script
+    init_keyboard(unlocked);
+  }
+}
 
-  // hide sequent view at start
-  hideSequent();
+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 restoreSelection(adjust) {
+    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();
+	    range = document.createRange();
+	    range.setStart(savedsc,savedso + adjust);
+	    range.collapse(true);
+            s.addRange(range);
+        }
+        else 
+            if (document.createRange)//non IE and no selection
+            {
+                window.getSelection().addRange(savedRange);
+            }
+            else 
+                if (document.selection)//IE
+                {
+                    savedRange.select();
+                }
+    }
+}
+
+function lookup_tex(texmacro)
+{
+  texmacro = texmacro.substring(1);
+  return unescape(macro2utf8[texmacro]);
+}
+ 
+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);
+	  
+	  sym = lookup_tex(match);
+	  if (typeof sym != "undefined") {
+	     len1 = unlocked.innerText.length;
+             unlocked.innerHTML = pre + sym + post;
+	     len2 = unlocked.innerText.length;
+             restoreSelection(len2 - len1); 
+ 	     return suppressdefault(e,true);
+	  }
+	  else {
+             // restoreSelection(0); 
+	     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;
 }
 
@@ -208,15 +349,33 @@ String.prototype.sescape = function() {
 	return (result);
 }
 
-String.prototype.unescapeHTML = function()
+String.prototype.html_to_matita = function()
 {
 	var patt1 = /<br(\/|)>/gi;
-	var patt2 = /&lt;/gi;
-	var patt3 = /&gt;/gi;
+	var patt2 = /</gi
+	var patt3 = />/gi
+	var patt4 = /&lt;/gi;
+	var patt5 = /&gt;/gi;
 	var result = this;
 	result = result.replace(patt1,"\n");
-	result = result.replace(patt2,"<");
-	result = result.replace(patt3,">");
+	result = result.replace(patt2,"\005");
+	result = result.replace(patt3,"\006");
+	result = result.replace(patt4,"<");
+	result = result.replace(patt5,">");
+	return (unescape(result));
+}
+
+String.prototype.matita_to_html = function()
+{
+	var patt1 = /</gi
+	var patt2 = />/gi
+	var patt3 = /\005/gi;
+	var patt4 = /\006/gi;
+	var result = this;
+	result = result.replace(patt1,"&lt;");
+	result = result.replace(patt2,"&gt;");
+	result = result.replace(patt3,"<");
+	result = result.replace(patt4,">");
 	return (unescape(result));
 }
 
@@ -308,13 +467,15 @@ function advanceForm1()
 	processor = function(xml) {
 		if (is_defined(xml)) {
 			// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-			len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+			parsed = xml.getElementsByTagName("parsed")[0];
+			len = parseInt(parsed.getAttribute("length"));
 	                len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.unescapeHTML();
-			parsedtxt = unescaped.substr(0,len); 
+			unescaped = unlocked.innerHTML.html_to_matita();
+			parsedtxt = parsed.childNodes[0].nodeValue;
+			//parsedtxt = unescaped.substr(0,len); 
 			unparsedtxt = unescaped.substr(len);
-			locked.innerHTML = locked.innerHTML + parsedtxt;
-			unlocked.innerHTML = unparsedtxt;
+			locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+			unlocked.innerHTML = unparsedtxt.matita_to_html();
 			len1 = unlocked.innerHTML.length;
 			len2 = len0 - len1;
 			metasenv = xml.getElementsByTagName("meta");
@@ -327,7 +488,7 @@ function advanceForm1()
 		resume();
 	};
 	pause();
-        callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+        callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
   
 }
 
@@ -336,13 +497,15 @@ function gotoBottom()
 	processor = function(xml) {
 		if (is_defined(xml)) {
 			// debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
-			len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+			parsed = xml.getElementsByTagName("parsed")[0];
+			len = parseInt(parsed.getAttribute("length"));
 	                len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.unescapeHTML();
-			parsedtxt = unescaped.substr(0,len); 
+			unescaped = unlocked.innerHTML.html_to_matita();
+			parsedtxt = parsed.childNodes[0].nodeValue;
+			//parsedtxt = unescaped.substr(0,len); 
 			unparsedtxt = unescaped.substr(len);
-			locked.innerHTML = locked.innerHTML + parsedtxt;
-			unlocked.innerHTML = unparsedtxt;
+			locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+			unlocked.innerHTML = unparsedtxt.matita_to_html();
 			len1 = unlocked.innerHTML.length;
 			len2 = len0 - len1;
 			metasenv = xml.getElementsByTagName("meta");
@@ -355,7 +518,7 @@ function gotoBottom()
                 resume();
 	};
 	pause();
-	callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+	callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
   
 }
 
@@ -367,14 +530,15 @@ function gotoPos(offset)
         }
 	processor = function(xml) {
 		if (is_defined(xml)) {
-			// debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND");
-			len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+			parsed = xml.getElementsByTagName("parsed")[0];
+			len = parseInt(parsed.getAttribute("length"));
 	                len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.unescapeHTML();
-			parsedtxt = unescaped.substr(0,len); 
+			unescaped = unlocked.innerHTML.html_to_matita();
+			parsedtxt = parsed.childNodes[0].nodeValue;
+			//parsedtxt = unescaped.substr(0,len); 
 			unparsedtxt = unescaped.substr(len);
-			locked.innerHTML = locked.innerHTML + parsedtxt;
-			unlocked.innerHTML = unparsedtxt;
+			locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html();
+			unlocked.innerHTML = unparsedtxt.matita_to_html();
 			len1 = unlocked.innerHTML.length;
 			len2 = len0 - len1;
 			metasenv = xml.getElementsByTagName("meta");
@@ -395,7 +559,7 @@ function gotoPos(offset)
 		}
 	}
 	pause();
-	callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape());
+	callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 }
 
 function retract()
@@ -437,6 +601,64 @@ function openFile()
 	callServer("open",processor,"file=" + escape(filename.value)); 
 }
 
+function retrieveFile(thefile)
+{ 
+	processor = function(xml)
+	{
+	        if (is_defined(xml)) {	
+	        	locked.innerHTML = "";
+			debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
+	                unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
+
+		} else {
+			debug("file open failed");
+		}
+	};
+	dialogBox.style.display = "none";
+	callServer("open",processor,"file=" + escape(thefile)); 
+}
+
+function showLibrary()
+{ 
+	var req = null; 
+        // pause();
+	if (window.XMLHttpRequest)
+	{
+		req = new XMLHttpRequest();
+	} 
+	else if (window.ActiveXObject) 
+	{
+		try {
+				req = new ActiveXObject("Msxml2.XMLHTTP");
+		} catch (e)
+		{
+			try {
+				req = new ActiveXObject("Microsoft.XMLHTTP");
+				} catch (e) {}
+		}
+   	}
+	req.onreadystatechange = function()
+	{ 
+
+		rs = req.readyState;
+
+		if(rs == 4)
+		{
+			stat = req.status;
+			stxt = req.statusText;
+			if(stat == 200)
+			{
+			  debug(req.responseText);
+			  showDialog("<H2>Library</H2>",req.responseText);
+			} 
+		} 
+	};
+	req.open("POST", "viewlib"); // + escape(unlocked.innerHTML), true);
+        req.setRequestHeader("Content-type","application/x-www-form-urlencoded");	
+	req.send();
+  
+}
+
 var goalcell;
 
 function hideSequent() {
@@ -449,24 +671,35 @@ function showSequent() {
   workarea.appendChild(goalcell);
 }
 
+function showDialog(title,content) {
+  dialogTitle.innerHTML = title;
+  dialogContent.innerHTML = content;
+  dialogBox.style.display = "block";
+}
+
 function removeElement(id) {
   var element = document.getElementById(id);
   element.parentNode.removeChild(element);
 } 
 
+var savedsc;
+var savedso;
+
 function getCursorPos() {
   var cursorPos;
   if (window.getSelection) {
     var selObj = window.getSelection();
-    var selRange = selObj.getRangeAt(0);
+    savedRange = selObj.getRangeAt(0);
+    savedsc = savedRange.startContainer;
+    savedso = savedRange.startOffset;
     //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);
@@ -499,3 +732,26 @@ function findNode(list, node, acc) {
 function test () {
   debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
 }
+
+function readCookie(name) {
+	var nameEQ = name + "=";
+	var ca = document.cookie.split(';');
+	for(var i=0;i < ca.length;i++) {
+		var c = ca[i];
+		while (c.charAt(0)==' ') c = c.substring(1,c.length);
+		if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
+	}
+	return null;
+}
+
+function delete_cookie ( cookie_name )
+{
+  var cookie_date = new Date();  // current date & time
+  cookie_date.setTime ( cookie_date.getTime() - 1 );
+  document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
+}
+
+function delete_session()
+{
+	delete_cookie("session");
+}