X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fhtml%2Fmatitaweb.js;h=3948a730fb3906f9640cff860e5e0630171706ec;hb=98827f140349f91cbd546491b233d6d5d3f335c3;hp=6661cd04ad5959b28ae8f6d8ff49341dc441eeb7;hpb=71204a8e8d1084c94adfbcf9264f71ab85f3621e;p=helm.git
diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index 6661cd04a..3948a730f 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;
@@ -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 = $(tagname + "." + classname);
+ } else {
+ tags = $(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() {
@@ -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();
}
}
};
@@ -616,7 +668,8 @@ function advOneStep(xml) {
var len2 = parsedtxt.length;
metasenv = xml.getElementsByTagName("meta");
statements = listcons(len2,statements);
- unlocked.scrollIntoView(true);
+ //unlocked.scrollIntoView(true);
+ smartScroll();
return len;
}
else if (is_defined(ambiguity)) {
@@ -692,7 +745,7 @@ function advOneStep(xml) {
else {
var error = xml.getElementsByTagName("error")[0];
unlocked.innerHTML = error.childNodes[0].wholeText;
- // debug(xml.childNodes[0].nodeValue);
+ error(xml.childNodes[0].nodeValue);
throw "Stop";
}
@@ -708,7 +761,7 @@ function advanceForm1()
init_hyperlinks();
init_autotraces();
} else {
- debug("advance failed");
+ error("advance failed");
}
} catch (e) {
// nothing to do
@@ -930,7 +983,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 +1063,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 +1080,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 +1097,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,25 +1117,6 @@ 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) {
init_hyperlinks();
@@ -1099,7 +1135,8 @@ function gotoPos(offset)
} else {
init_hyperlinks();
init_autotraces();
- unlocked.scrollIntoView(true);
+ // unlocked.scrollIntoView(true);
+ smartScroll();
populate_goalarray(metasenv);
resume();
}
@@ -1108,7 +1145,7 @@ function gotoPos(offset)
callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
}
-function retract()
+function retractStep()
{
processor = function(xml) {
if (typeof xml != "undefined") {
@@ -1131,9 +1168,10 @@ function retract()
init_hyperlinks();
init_autotraces();
strip_anchors();
- unlocked.scrollIntoView(true);
+ // unlocked.scrollIntoView(true);
+ smartScroll();
} else {
- debug("retract failed");
+ error("retract failed");
}
resume();
};
@@ -1151,7 +1189,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 +1200,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;
@@ -1181,8 +1220,11 @@ function retrieveFile(thefile)
init_hyperlinks();
init_autotraces();
+ } else {
+ error("file open failed");
+ }
} else {
- debug("file open failed");
+ window.location = "/login.html";
}
};
abortDialog("dialogBox");
@@ -1191,7 +1233,6 @@ function retrieveFile(thefile)
function go_external_hyperlink(uri,thefile,id)
{
- var docWin = createDocWin(uri);
processor = function(xml)
{
if (is_defined(xml)) {
@@ -1205,16 +1246,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).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 +1270,7 @@ function createDocWin(uri) {
'' +
'' +
'' +
+ '' +
'' +
'' +
'');
@@ -1232,16 +1281,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 +1340,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 = "";
@@ -1368,7 +1407,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 +1418,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() {
@@ -1678,3 +1717,7 @@ function resume()
}
}
+function test()
+{
+ xx.onclick();
+}