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('.'));
- // 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;
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 = $(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);
for (var i = 0; i < tlen; i++) {
tags[0].parentNode.removeChild(tags[0]);
}
+ */
}
function strip_interpr() {
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");
}
processResponse(xmlDoc);
} else {
- processResponse();
+ // in case of error, assume session has expired
+ window.location = "/login.html";
+ // processResponse();
}
}
};
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)) {
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";
}
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();
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();
init_autotraces();
hideSequent();
strip_anchors();
- unlocked.scrollIntoView(true);
+ // 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) {
init_hyperlinks();
} 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()
{
processor = function(xml) {
if (typeof xml != "undefined") {
init_hyperlinks();
init_autotraces();
strip_anchors();
- unlocked.scrollIntoView(true);
+ // unlocked.scrollIntoView(true);
+ smartScroll();
} else {
- debug("retract failed");
+ error("retract failed");
}
resume();
};
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;
init_hyperlinks();
init_autotraces();
+ } else {
+ error("file open failed");
+ }
} else {
- debug("file open failed");
+ window.location = "/login.html";
}
};
abortDialog("dialogBox");
function go_external_hyperlink(uri,thefile,id)
{
- var docWin = createDocWin(uri);
processor = function(xml)
{
if (is_defined(xml)) {
} 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");
'<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>');
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;
if (file) {
var reader = new FileReader();
reader.onerror = function (evt) {
- debug("file open failed");
+ error("file open failed");
}
reader.onload = function (evt) {
lockedbackup = "";
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() {
}
}
+function test()
+{
+ xx.onclick();
+}
projects / helm.git / blobdiff