X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;h=248eeaa672b157072d771b7e4d89c9a32ee9488d;hb=bbb6dd07ecb430bf06bb52c2506626106449a5af;hp=20d0fec43dbcf9557da473af7fae857413b3d60e;hpb=b40e4e96e85103c7072985990c6b541371fd5a48;p=helm.git

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 20d0fec43..248eeaa67 100644
--- a/matitaB/matita/html/matitaweb.js
+++ b/matitaB/matita/html/matitaweb.js
@@ -49,6 +49,23 @@ function initialize()
   if (readCookie("session") == null) {
     window.location = "/login.html"
   } else {
+    matitaLayout = $('body').layout({ 
+	    applyDefaultStyles: true, 
+	    north : {
+		    closable: false,
+    		    resizable: false
+            },
+	    east : { 
+    		    onresize_end : resizeSide,
+                    resizable : true,
+    		    size: int_of_px($('body').width())/3
+            },
+    	    south : {
+		    closable: true,
+	    	    resizable: true,
+	   	    size: 80
+	    }
+    	}); 
     body = document.body;
     titlebar = document.getElementById("titlebar");
     matitaTitle = document.getElementById("matitaTitle");
@@ -81,14 +98,44 @@ function initialize()
     initializeLayout();
     updateSide();
 
-    changeFile("test.ma");
+    // hide log at start
+    matitaLayout.hide("south");
+
+    // changeFile("test.ma");
+    retrieveFile("test.ma");
 
     // initialize keyboard events in the unlocked script
     init_keyboard(unlocked);
 
+    init_hyperlinks();
     init_autotraces();
 
+  } 
+}
+
+function go_hyperlink(atag) {
+  var uri = atag.attr("href");
+  var mybaseuri = uri.substring(0,uri.lastIndexOf('/'));
+  var id = uri.substring(uri.lastIndexOf('/')+1,uri.lastIndexOf('.'));
+  // only non-notations
+  if (uri != "cic:/fakeuri.def(1)") {
+     if (mybaseuri == baseuri) {
+        try {
+		$('#'+id)[0].scrollIntoView(true);
+	} catch (e) { 
+		// best effort: if undefined, don't scroll
+	}
+     } else {
+	createDocWin(mybaseuri,id);
+     }
   }
+  return false;
+}
+
+function init_hyperlinks() {
+  $("#unlocked a").click(function () { return go_hyperlink($(this))});
+  $("#locked a").click(function () { return go_hyperlink($(this))});
+  $("#goalview a").click(function () { return go_hyperlink($(this))});
 }
 
 function init_autotraces() {
@@ -114,7 +161,8 @@ function trace_of(node) {
 
 function changeFile(name) {
     current_fname = name;
-    matitaTitle.innerHTML = "Matita - cic:/matita/" + name;
+    matitaTitle.innerHTML = "cic:/matita/" + name;
+    baseuri = "cic:/matita/" + name.substring(0,name.lastIndexOf('.'));
 }
 
 function init_keyboard(target)
@@ -160,6 +208,7 @@ function string_of_key(n)
 
 function pressmesg(w,e)
 {
+/* for debugging only
    debug(w + '  keyCode=' + keyval(e.keyCode) +
                  ' which=' + keyval(e.which) +
                  ' charCode=' + keyval(e.charCode) +
@@ -167,6 +216,7 @@ function pressmesg(w,e)
 	      + ' ctrlKey='+e.ctrlKey
 	      + ' altKey='+e.altKey
 	      + ' metaKey='+e.metaKey);
+*/
 }
  
 function suppressdefault(e,flag)
@@ -210,6 +260,23 @@ function lookup_tex(texmacro)
 
 function strip_tags(tagname,classname) 
 {
+    var tags;
+    if (is_defined(classname)) {
+      tags = $("#unlocked " + tagname + "." + classname);
+    } else {
+      tags = $("#unlocked " + tagname);
+    }
+    var tlen = tags.length; // preserving the value from removeChild operations
+    for (i = 0; i < tlen; i++) {
+        var children = tags[i].childNodes;
+        for (j = 0; j < children.length; j++) {
+            tags[i].parentNode.insertBefore(children[j],tags[i]);
+	}
+    }
+    tags.remove();
+
+    /*
+
     var tags = unlocked.getElementsByTagName(tagname);
     if (is_defined(classname)) {
 	tags = filterByClass(tags,classname);
@@ -224,11 +291,18 @@ function strip_tags(tagname,classname)
     for (var i = 0; i < tlen; i++) {
       tags[0].parentNode.removeChild(tags[0]);
     }
+    */
 }
 
 function strip_interpr() {
+	pause();
 	strip_tags("A");
-	alert("strip_interpr ended");
+	resume();
+	// alert("strip_interpr ended");
+}
+
+function strip_anchors() {
+	strip_tags("IMG","anchor");
 }
  
 function keypress(e)
@@ -283,9 +357,15 @@ function debug(txt)
         logtxt = /* logtxt + "\n" +*/ txt;
 }
 
+function error(txt)
+{
+	$('#bottomtext').children().first().text(txt);
+	matitaLayout.show("south");
+}
+
 function showLog() {
-  logWin = window.open( "", "Matita Log",
-     "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
+  var logWin = window.open( "", "Matita Log",
+     "width=600,height=450,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
   logWin.document.write('<html><head><title>Matita Log' + '</title></head>');	
   logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
     logtxt + '</textarea></body></html>');
@@ -552,7 +632,9 @@ function callServer(servicename,processResponse,reqbody)
                           } 	
 			  processResponse(xmlDoc);
 			} else {
-			  processResponse();
+			  // in case of error, assume session has expired
+                          window.location = "/login.html";
+			  // processResponse();
 			}
 		} 
 	};
@@ -570,23 +652,27 @@ function advOneStep(xml) {
         var parsed = xml.getElementsByTagName("parsed")[0];
 	var ambiguity = xml.getElementsByTagName("ambiguity")[0];
 	var disamberr = xml.getElementsByTagName("disamberror")[0];
+	var localized = xml.getElementsByTagName("localized")[0];
         if (is_defined(parsed)) {
 	// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
 	    var len = parseInt(parsed.getAttribute("length"));
-            // len0 = unlocked.innerHTML.length;
-	    var unescaped = unlocked.innerHTML.html_to_matita();
-	    var parsedtxt = parsed.childNodes[0].wholeText;
-	    //parsedtxt = unescaped.substr(0,len); 
-	    var unparsedtxt = unescaped.substr(len);
-	    lockedbackup += parsedtxt;
-	    locked.innerHTML = lockedbackup;
-	    unlocked.innerHTML = unparsedtxt.matita_to_html();
-	    // len1 = unlocked.innerHTML.length;
-	    // len2 = len0 - len1;
-	    var len2 = parsedtxt.length;
-	    metasenv = xml.getElementsByTagName("meta");
-	    statements = listcons(len2,statements);
-	    unlocked.scrollIntoView(true);
+	    if (len > 0) {
+              // len0 = unlocked.innerHTML.length;
+	      var unescaped = unlocked.innerHTML.html_to_matita();
+	      var parsedtxt = parsed.childNodes[0].wholeText;
+	      //parsedtxt = unescaped.substr(0,len); 
+	      var unparsedtxt = unescaped.substr(len);
+	      lockedbackup += parsedtxt;
+	      locked.innerHTML = lockedbackup;
+	      unlocked.innerHTML = unparsedtxt.matita_to_html();
+	      // len1 = unlocked.innerHTML.length;
+	      // len2 = len0 - len1;
+	      var len2 = parsedtxt.length;
+	      metasenv = xml.getElementsByTagName("meta");
+	      statements = listcons(len2,statements);
+	      //unlocked.scrollIntoView(true);
+	      smartScroll();
+	    }
 	    return len;
 	}
 	else if (is_defined(ambiguity)) {
@@ -658,12 +744,14 @@ function advOneStep(xml) {
               next_cp(0);
             }
 	    throw "Stop";
-	}
-        else {
-            var error = xml.getElementsByTagName("error")[0]; 
-	    unlocked.innerHTML = error.childNodes[0].wholeText;
-	    // debug(xml.childNodes[0].nodeValue);
+	} else if (is_defined(localized)) {
+	    unlocked.innerHTML = localized.childNodes[0].wholeText;
 	    throw "Stop";
+        }
+        else {
+            var err = xml.getElementsByTagName("error")[0]; 
+            error(err.childNodes[0].nodeValue);
+            throw "Stop";
 	}
 
 }
@@ -675,9 +763,10 @@ function advanceForm1()
 		if (is_defined(xml)) {
 		    advOneStep(xml);
                     populate_goalarray(metasenv);
+		    init_hyperlinks();
 	            init_autotraces();
 		} else {
-			debug("advance failed");
+			error("advance failed");
 		}
 	    } catch (e) { 
 		    // nothing to do 
@@ -899,8 +988,10 @@ function gotoBottom()
 		  	  var len2 = parsedtxt.length;
 		          statements = listcons(len2,statements);
 			}
-		  	unlocked.scrollIntoView(true);
+		  	// unlocked.scrollIntoView(true);
+	                smartScroll();
 		  	metasenv = xml.getElementsByTagName("meta");
+		        init_hyperlinks();
 			init_autotraces();
 	                populate_goalarray(metasenv);
 
@@ -977,10 +1068,10 @@ function gotoBottom()
 			    unlocked.innerHTML = localized.childNodes[0].wholeText;
 			}
 			else if (is_defined(generic_err)) {
-			    debug("Unmanaged error:\n" ^ generic_err.childNodes[0].wholeText);
+			    error("Unmanaged error:\n" + generic_err.childNodes[0].wholeText);
 			}
 		} else {
-			debug("goto bottom failed");
+			error("goto bottom failed");
 		} 
                 resume();
 	};
@@ -994,7 +1085,7 @@ function gotoTop()
 	processor = function(xml) {
 		if (is_defined(xml)) {
 		  if (xml.childNodes[0].textContent != "ok") {
-                     debug("goto top failed");
+                     error("goto top failed");
                   }
                   else
                         statements = listnil();
@@ -1007,11 +1098,14 @@ function gotoTop()
 			unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
 			lockedbackup = "";
                         locked.innerHTML = lockedbackup;
+		        init_hyperlinks();
 			init_autotraces();
                         hideSequent();
-                        unlocked.scrollIntoView(true);
+			strip_anchors();
+                        // unlocked.scrollIntoView(true);
+	                smartScroll();
 		} else {
-			debug("goto top failed");
+			error("goto top failed");
 		} 
                 resume();
 	};
@@ -1028,27 +1122,9 @@ function gotoPos(offset)
 	processor = function(xml) {
 		if (is_defined(xml)) {
 	            try {
-			/*
-			parsed = xml.getElementsByTagName("parsed")[0];
-			len = parseInt(parsed.getAttribute("length"));
-	                // len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.html_to_matita();
-			parsedtxt = parsed.childNodes[0].wholeText;
-			//parsedtxt = unescaped.substr(0,len); 
-			unparsedtxt = unescaped.substr(len);
-			lockedbackup += parsedtxt;
-			locked.innerHTML = lockedbackup; //.matita_to_html();
-			unlocked.innerHTML = unparsedtxt.matita_to_html();
-			// len1 = unlocked.innerHTML.length;
-			len2 = parsedtxt.length;
-			metasenv = xml.getElementsByTagName("meta");
-	                // populate_goalarray(metasenv);
-			statements = listcons(len2,statements);
-			unlocked.scrollIntoView(true);
-			// la populate non andrebbe fatta a ogni passo
-			*/
 			var len = advOneStep(xml);
-	                if (offset <= len) {
+	                if (len == 0 || offset <= len) {
+		                init_hyperlinks();
 			        init_autotraces();
 				populate_goalarray(metasenv);
 				resume();
@@ -1056,13 +1132,16 @@ function gotoPos(offset)
 				gotoPos(offset - len);
 			}
 		    } catch (er) {
+		        init_hyperlinks();
 			init_autotraces();
 			populate_goalarray(metasenv);
 			resume();
 		    }
 		} else {
+		        init_hyperlinks();
 			init_autotraces();
-			unlocked.scrollIntoView(true);
+			// unlocked.scrollIntoView(true);
+	                smartScroll();
 			populate_goalarray(metasenv);
 			resume();
 		}
@@ -1071,8 +1150,9 @@ function gotoPos(offset)
 	callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
 }
 
-function retract()
+function retractStep()
 {
+    if (!is_nil(statements)) {
 	processor = function(xml) {
 		if (typeof xml != "undefined") {
 			// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
@@ -1090,16 +1170,20 @@ function retract()
                         locked.innerHTML = lockedbackup;
 			unlocked.innerHTML = statement + unlocked.innerHTML;
 			metasenv = xml.getElementsByTagName("meta");
-			init_autotraces();
                         populate_goalarray(metasenv);
-                        unlocked.scrollIntoView(true);
+		        init_hyperlinks();
+			init_autotraces();
+			strip_anchors();
+                        // unlocked.scrollIntoView(true);
+	                smartScroll();
 		} else {
-			debug("retract failed");
+			error("retract failed");
 		}
 		resume();
 	};
 	pause();
         callServer("retract",processor);
+    }
 }
 
 function openFile()
@@ -1110,8 +1194,9 @@ function openFile()
 			lockedbackup = "";
 	        	locked.innerHTML = lockedbackup;
 	                unlocked.innerHTML = xml.documentElement.wholeText;
+			strip_anchors();
 		} else {
-			debug("file open failed");
+			error("file open failed");
 		}
 	};
 	callServer("open",processor,"file=" + escape(filename.value)); 
@@ -1122,6 +1207,7 @@ function retrieveFile(thefile)
 	processor = function(xml)
 	{
 	        if (is_defined(xml)) {	
+                   if (!is_defined(xml.getElementsByTagName("error")[0])) {
 	                changeFile(thefile);
                         matita.disambMode = false;
                         matita.proofMode = false;
@@ -1137,16 +1223,71 @@ function retrieveFile(thefile)
                         } else {
                           unlocked.innerHTML = xml.childNodes[0].textContent;
                         }
+			strip_anchors();
+		        init_hyperlinks();
 			init_autotraces();
-
+			unlocked.scrollIntoView(true);
+		   } else {
+			error("file open failed");
+	           }
 		} else {
-			debug("file open failed");
+                   window.location = "/login.html";
 		}
 	};
 	abortDialog("dialogBox");
 	callServer("open",processor,"file=" + escape(thefile)); 
 }
 
+function go_external_hyperlink(uri,thefile,id)
+{ 
+	processor = function(xml)
+	{
+	        if (is_defined(xml)) {	
+                        // code originally used in google chrome (problems with mozilla)
+			// debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue);
+	                // unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue;
+			// debug(xml.childNodes[0].textContent);
+			var doctext;
+                        if (document.all) { // IE
+                          doctext = xml.childNodes[0].text;
+                        } else {
+                          doctext= xml.childNodes[0].textContent;
+                        }
+                        $('#locked').html(doctext);
+                        try {
+			  // scroll to anchor (if it exists)
+                      	  $('#' + id).get(0).scrollIntoView(true);
+                        } catch (e) { }
+                        init_hyperlinks();
+                        init_autotraces();
+		} else {
+			$('#locked').html("404 object not found");
+		}
+	};
+	callServer("open",processor,"file=" + escape(thefile) + "&readonly=true"); 
+}
+
+function createDocWin(uri,id) {
+  // 12 = position of the second '/' in uri (to strip off "cic:/matita/")
+  var thefile = uri.substring(12) + ".ma";
+  var title = "Matita Browser - " + uri;
+  var docWin = window.open( "", "matitabrowser",
+     "width=800,height=600,location=no,menubar=no,status=no,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
+  docWin.document.write('<html><head><title>' + title + '</title>' +
+                        '<script type="text/javascript" src="jquery.js"></script>' +
+                        '<script type="text/javascript" src="jquery.tooltip.min.js"></script>' +
+                        '<script type="text/javascript" src="matitaweb.js"></script>' +
+			'<script type="text/javascript">go_external_hyperlink("' + uri + '","' + thefile + '","' + id + '");</script>' +
+                        '<link rel="stylesheet" type="text/css" href="matitaweb.css"/>' +
+                        '<link rel="stylesheet" type="text/css" href="jquery.tooltip.css"/>' +
+		        '</head>');	
+  docWin.document.write('<body><H1>'+ uri + '</H1>' + 
+		      '<pre id="locked"></pre></body></html>');
+  docWin.document.close();
+  docWin.baseuri = uri;
+  return docWin;
+}
+
 function showLibrary(title,callback,reloadDialog)
 { 
 	var req = null;
@@ -1206,7 +1347,7 @@ function uploadOK()
    if (file) { 
       var reader = new FileReader();
       reader.onerror = function (evt) {
-	   debug("file open failed");
+	   error("file open failed");
       }
       reader.onload = function (evt) {
 	   lockedbackup = "";
@@ -1243,7 +1384,9 @@ function newDialog()
 {
 	callback = function (fname) { 
 	  abortDialog("dialogBox");
-	  saveFile(fname,"","",false,newDialog,true);
+	  saveFile(fname,"",
+		   "(* new script *)",
+                   false,newDialog,true);
 	};
 	showLibrary("Create new file", callback, newDialog);
 }
@@ -1273,7 +1416,7 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
                     if (reloadFile) { retrieveFile(fname); }
 		  }
 		} else {
-			debug("save file failed");
+			error("save file failed");
 		}
 		resume();
 	};
@@ -1284,7 +1427,7 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
 			            "&unlocked=" + unlockedtxt +
 				    "&force=" + force);
 	}
-	else { debug("no file selected"); }
+	else { error("no file selected"); }
 }
 
 function createDir() {
@@ -1299,6 +1442,7 @@ function createDir() {
 		} else {
                       alert("An error occurred :-(");
 		}
+                resume();
                 dialogBox.reload();
 	};
         pause();
@@ -1312,12 +1456,12 @@ function createDir() {
 function commitAll()
 {
 	processor = function(xml) {
-		if (is_defined(xml)) {
+		if (xml.getElementsByTagName("details").length > 0) {
                         debug(xml.getElementsByTagName("details")[0].textContent);
 			alert("Commit executed: see details in the log.\n\n" +
                               "NOTICE: this message does NOT imply (yet) that the commit was successful.");
 		} else {
-			alert("Commit failed!");
+			alert("Commit denied.\nPermission to commit and update is provided by the Matita team upon request.");
 		}
 		resume();
 	};
@@ -1328,12 +1472,12 @@ function commitAll()
 function updateAll()
 {
 	processor = function(xml) {
-		if (is_defined(xml)) {
+		if (xml.getElementsByTagName("details").length > 0) {
 			alert("Update executed.\n\n" +
                               "Details:\n" +
                               xml.getElementsByTagName("details")[0].textContent);
 		} else {
-			alert("Update failed!");
+			alert("Update denied.\nPermission to commit and update is provided by the Matita team upon request.");
 		}
 		resume();
 	};
@@ -1583,3 +1727,7 @@ function resume()
         }
 }
 
+function test()
+{
+	xx.onclick();
+}