<div class="toparea ui-layout-north" id="toparea">
<div class="titlebar" id="titlebar">
- <div class="mainTitle"><H2 id="matitaTitle">Matita - <<Filename>></H2></div>
+ <div class="mainTitle"><img src="icons/matita-32.png"><H2 id="matitaTitle"><<Filename>></H2></div>
<div class="mainRight" id="matitaLogout"><A id="hlogout" href="/logout.html">Log out</A></div>
</div>
color:black;
}
+h2#matitaTitle {
+ display: inline;
+ padding: 6px;
+ vertical-align: top;
+}
+
.smallmargin {
margin:4px !important;
}
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 strip_anchors() {
- strip_tags("INPUT","anchor");
+ strip_tags("IMG","anchor");
}
function keypress(e)
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);
- smartScroll();
+ 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)) {
if (is_defined(xml)) {
try {
var len = advOneStep(xml);
- if (offset <= len) {
+ if (len == 0 || offset <= len) {
init_hyperlinks();
init_autotraces();
populate_goalarray(metasenv);
function retractStep()
{
+ if (!is_nil(statements)) {
processor = function(xml) {
if (typeof xml != "undefined") {
// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
};
pause();
callServer("retract",processor);
+ }
}
function openFile()
strip_anchors();
init_hyperlinks();
init_autotraces();
-
+ unlocked.scrollIntoView(true);
} else {
error("file open failed");
}
$('#locked').html(doctext);
try {
// scroll to anchor (if it exists)
- $('#' + id).scrollIntoView(true);
+ $('#' + id).get(0).scrollIntoView(true);
} catch (e) { }
init_hyperlinks();
init_autotraces();
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();
};
List.filter (fun x -> String.sub x 0 1 <> ".")
(Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in
let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in
+ let subdirs = List.sort String.compare subdirs in
(* only .ma scripts, hidden files excluded *)
let scripts =
not (Sys.is_directory (gpath x)) &&
(String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
with Not_found | Invalid_argument _ -> false) dirlist in
+ let scripts = List.sort String.compare scripts in
let subdirtags =
String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
let scripttags =
Mutex.unlock mutex;
;;
-let do_global_commit () =
+let do_global_commit (* () *) uid =
prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
List.fold_left
(fun out u ->
(* XXX: at the moment, we don't keep track of the order in which users have
scheduled their commits, but we should, otherwise we will get a
"first come, random served" policy *)
- "" (* (List.rev !to_be_committed) *) (MatitaAuthentication.get_users ())
+ "" (* (List.rev !to_be_committed) *)
+ (* replace [uid] to commit all users:
+ (MatitaAuthentication.get_users ())
+ *)
+ [uid]
;;
(*** from matitaScript.ml ***)
let pre = Netconversion.ustring_sub `Enc_utf8 0 x !outstr in
let post = Netconversion.ustring_sub `Enc_utf8 x
(Netconversion.ustring_length `Enc_utf8 !outstr - x) !outstr in
- outstr := Printf.sprintf
- "%s\005input type=\"radio\" class=\"anchor\" id=\"%s\" /\006%s" pre objname post;
+ outstr := Printf.sprintf
+ "%s\005img class=\"anchor\" src=\"icons/tick.png\" id=\"%s\" /\006%s" pre objname post;
prerr_endline ("baseuri after advance = " ^ status#baseuri);
(* prerr_endline ("parser output: " ^ !outstr); *)
(status,!outstr, unparsed_txt'),parsed_text_len
cgi#out_channel#output_string "<response>ok</response>"
with
| File_already_exists ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
cgi#out_channel#output_string "<response>cancelled</response>"
| Sys_error _ ->
cgi # set_header
~content_type:"text/xml; charset=\"utf-8\""
()
| e ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
let estr = Printexc.to_string e in
cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
cgi#out_channel#commit_work()
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
let sid = HExtlib.unopt sid in
MatitaAuthentication.probe_commit_priv sid;
- let out = do_global_commit () in
+ let uid = MatitaAuthentication.user_of_session sid in
+ let out = do_global_commit (* () *) uid in
cgi # set_header
~cache:`No_cache
~content_type:"text/xml; charset=\"utf-8\""
cgi#out_channel#output_string ("<details>" ^ out ^ "</details>");
cgi#out_channel#output_string "</commit>"
with
+ | Failure _ ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<commit><error>no commit privileges</error></commit>"
| Not_found _ ->
cgi # set_header
~status:`Internal_server_error
cgi#out_channel#output_string ("<details>" ^ details ^ "</details>");
cgi#out_channel#output_string "</update>";
with
+ | Failure _ ->
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<commit><error>no commit privileges</error></commit>"
| Not_found _ ->
cgi # set_header
~status:`Internal_server_error
~content_type:"text/xml; charset=\"utf-8\""
();
cgi#out_channel#output_string body
+ | End_of_file _ ->
+ let body = "<response><parsed length=\"0\"></parsed></response>" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
| Not_found _ ->
cgi # set_header
~status:`Internal_server_error