X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;h=248eeaa672b157072d771b7e4d89c9a32ee9488d;hb=0e16720654c6667b94433e91dddc3c53b904e200;hp=6661cd04ad5959b28ae8f6d8ff49341dc441eeb7;hpb=5310bb693a61b4c2c51bbd05e5ef9a4b764012cd;p=helm.git

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 6661cd04a..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,7 +98,11 @@ 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);
@@ -89,20 +110,23 @@ function initialize()
     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('.'));
-  // 12 = position of the second '/' in mybaseuri (to strip off "cic:/matita/")
-  var thefile = mybaseuri.substring(12) + ".ma";
+  // only non-notations
   if (uri != "cic:/fakeuri.def(1)") {
      if (mybaseuri == baseuri) {
-        $('#'+id)[0].scrollIntoView(true);
+        try {
+		$('#'+id)[0].scrollIntoView(true);
+	} catch (e) { 
+		// best effort: if undefined, don't scroll
+	}
      } else {
-	go_external_hyperlink(mybaseuri,thefile,id);
+	createDocWin(mybaseuri,id);
      }
   }
   return false;
@@ -137,7 +161,7 @@ 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('.'));
 }
 
@@ -184,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) +
@@ -191,6 +216,7 @@ function pressmesg(w,e)
 	      + ' ctrlKey='+e.ctrlKey
 	      + ' altKey='+e.altKey
 	      + ' metaKey='+e.metaKey);
+*/
 }
  
 function suppressdefault(e,flag)
@@ -234,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);
@@ -248,6 +291,7 @@ function strip_tags(tagname,classname)
     for (var i = 0; i < tlen; i++) {
       tags[0].parentNode.removeChild(tags[0]);
     }
+    */
 }
 
 function strip_interpr() {
@@ -258,7 +302,7 @@ function strip_interpr() {
 }
 
 function strip_anchors() {
-	strip_tags("INPUT","anchor");
+	strip_tags("IMG","anchor");
 }
  
 function keypress(e)
@@ -313,6 +357,12 @@ function debug(txt)
         logtxt = /* logtxt + "\n" +*/ txt;
 }
 
+function error(txt)
+{
+	$('#bottomtext').children().first().text(txt);
+	matitaLayout.show("south");
+}
+
 function showLog() {
   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");
@@ -582,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();
 			}
 		} 
 	};
@@ -600,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)) {
@@ -688,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";
 	}
 
 }
@@ -708,7 +766,7 @@ function advanceForm1()
 		    init_hyperlinks();
 	            init_autotraces();
 		} else {
-			debug("advance failed");
+			error("advance failed");
 		}
 	    } catch (e) { 
 		    // nothing to do 
@@ -930,7 +988,8 @@ 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();
@@ -1009,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();
 	};
@@ -1026,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();
@@ -1043,9 +1102,10 @@ function gotoTop()
 			init_autotraces();
                         hideSequent();
 			strip_anchors();
-                        unlocked.scrollIntoView(true);
+                        // unlocked.scrollIntoView(true);
+	                smartScroll();
 		} else {
-			debug("goto top failed");
+			error("goto top failed");
 		} 
                 resume();
 	};
@@ -1062,27 +1122,8 @@ 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);
@@ -1099,7 +1140,8 @@ function gotoPos(offset)
 		} else {
 		        init_hyperlinks();
 			init_autotraces();
-			unlocked.scrollIntoView(true);
+			// unlocked.scrollIntoView(true);
+	                smartScroll();
 			populate_goalarray(metasenv);
 			resume();
 		}
@@ -1108,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");
@@ -1131,14 +1174,16 @@ function retract()
 		        init_hyperlinks();
 			init_autotraces();
 			strip_anchors();
-                        unlocked.scrollIntoView(true);
+                        // unlocked.scrollIntoView(true);
+	                smartScroll();
 		} else {
-			debug("retract failed");
+			error("retract failed");
 		}
 		resume();
 	};
 	pause();
         callServer("retract",processor);
+    }
 }
 
 function openFile()
@@ -1151,7 +1196,7 @@ function openFile()
 	                unlocked.innerHTML = xml.documentElement.wholeText;
 			strip_anchors();
 		} else {
-			debug("file open failed");
+			error("file open failed");
 		}
 	};
 	callServer("open",processor,"file=" + escape(filename.value)); 
@@ -1162,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;
@@ -1180,9 +1226,12 @@ function retrieveFile(thefile)
 			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");
@@ -1191,7 +1240,6 @@ function retrieveFile(thefile)
 
 function go_external_hyperlink(uri,thefile,id)
 { 
-	var docWin = createDocWin(uri);
 	processor = function(xml)
 	{
 	        if (is_defined(xml)) {	
@@ -1205,16 +1253,23 @@ function go_external_hyperlink(uri,thefile,id)
                         } else {
                           doctext= xml.childNodes[0].textContent;
                         }
-			showDoc(uri,doctext,id,docWin);
-
+                        $('#locked').html(doctext);
+                        try {
+			  // scroll to anchor (if it exists)
+                      	  $('#' + id).get(0).scrollIntoView(true);
+                        } catch (e) { }
+                        init_hyperlinks();
+                        init_autotraces();
 		} else {
-			debug("file open failed");
+			$('#locked').html("404 object not found");
 		}
 	};
 	callServer("open",processor,"file=" + escape(thefile) + "&readonly=true"); 
 }
 
-function createDocWin(uri) {
+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");
@@ -1222,6 +1277,7 @@ function createDocWin(uri) {
                         '<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>');	
@@ -1232,16 +1288,6 @@ function createDocWin(uri) {
   return docWin;
 }
 
-function showDoc(uri,doctext,id,docWin) {
-  var outarea = docWin.document.getElementById("locked");
-  outarea.innerHTML = doctext;
-  try {
-	  docWin.document.getElementById(id).scrollIntoView(true);
-  } catch (e) { }
-  docWin.init_hyperlinks();
-  docWin.init_autotraces();
-}
-
 function showLibrary(title,callback,reloadDialog)
 { 
 	var req = null;
@@ -1301,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 = "";
@@ -1338,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);
 }
@@ -1368,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();
 	};
@@ -1379,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() {
@@ -1394,6 +1442,7 @@ function createDir() {
 		} else {
                       alert("An error occurred :-(");
 		}
+                resume();
                 dialogBox.reload();
 	};
         pause();
@@ -1407,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();
 	};
@@ -1423,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();
 	};
@@ -1678,3 +1727,7 @@ function resume()
         }
 }
 
+function test()
+{
+	xx.onclick();
+}