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");
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() {
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)
function pressmesg(w,e)
{
+/* for debugging only
debug(w + ' keyCode=' + keyval(e.keyCode) +
' which=' + keyval(e.which) +
' charCode=' + keyval(e.charCode) +
+ ' ctrlKey='+e.ctrlKey
+ ' altKey='+e.altKey
+ ' metaKey='+e.metaKey);
+*/
}
function suppressdefault(e,flag)
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);
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)
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>');
var tmp_goallist = "";
for (i = 0; i < menv.length; i++) {
metano = menv[i].getAttribute("number");
- metaname = menv[i].childNodes[0].childNodes[0].data;
- goal = menv[i].childNodes[1].childNodes[0].data;
+ // item 0 = <metaname>, item 1 = <goal>
+ metaname = menv[i].childNodes[0].childNodes[0].wholeText;
+ goal = menv[i].childNodes[1].childNodes[0].wholeText;
debug ("found meta n. " + metano);
debug ("found goal\nBEGIN" + goal + "\nEND");
goalarray[metano] = goal;
}
processResponse(xmlDoc);
} else {
- processResponse();
+ // in case of error, assume session has expired
+ window.location = "/login.html";
+ // processResponse();
}
}
};
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)) {
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";
}
}
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
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);
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();
};
processor = function(xml) {
if (is_defined(xml)) {
if (xml.childNodes[0].textContent != "ok") {
- debug("goto top failed");
+ error("goto top failed");
}
else
statements = listnil();
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();
};
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();
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();
}
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");
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()
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));
processor = function(xml)
{
if (is_defined(xml)) {
+ if (!is_defined(xml.getElementsByTagName("error")[0])) {
changeFile(thefile);
matita.disambMode = false;
matita.proofMode = false;
} 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;
if (file) {
var reader = new FileReader();
reader.onerror = function (evt) {
- debug("file open failed");
+ error("file open failed");
}
reader.onload = function (evt) {
lockedbackup = "";
{
callback = function (fname) {
abortDialog("dialogBox");
- saveFile(fname,"","",false,newDialog,true);
+ saveFile(fname,"",
+ "(* new script *)",
+ false,newDialog,true);
};
showLibrary("Create new file", callback, newDialog);
}
if (reloadFile) { retrieveFile(fname); }
}
} else {
- debug("save file failed");
+ error("save file failed");
}
resume();
};
"&unlocked=" + unlockedtxt +
"&force=" + force);
}
- else { debug("no file selected"); }
+ else { error("no file selected"); }
}
function createDir() {
} else {
alert("An error occurred :-(");
}
+ resume();
dialogBox.reload();
};
pause();
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();
};
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();
};
}
}
+function test()
+{
+ xx.onclick();
+}
projects / helm.git / blobdiff