From 92fc70ae76ae4376b7976d1dff5c9b57d1b96056 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 6 Jul 2012 12:32:08 +0000 Subject: [PATCH] Bug fixing + cosmetic changes --- matitaB/matita/html/icons/matita-32.png | Bin 0 -> 651 bytes matitaB/matita/html/index.html | 2 +- matitaB/matita/html/matitaweb.css | 6 +++ matitaB/matita/html/matitaweb.js | 52 +++++++++++++----------- matitaB/matita/matitaFilesystem.ml | 2 + matitaB/matita/matitadaemon.ml | 44 +++++++++++++++++--- 6 files changed, 76 insertions(+), 30 deletions(-) create mode 100644 matitaB/matita/html/icons/matita-32.png diff --git a/matitaB/matita/html/icons/matita-32.png b/matitaB/matita/html/icons/matita-32.png new file mode 100644 index 0000000000000000000000000000000000000000..91d6e2a3e3618ebcabc6a5203d4b7f281f8cd31e GIT binary patch literal 651 zcmV;60(AX}P)Px#24YJ`L;(K){{a7>y{D4^000SaNLh0L01FcU01FcV0GgZ_00007bV*G`2iyk( z4iOvLpThhA00Ik1L_t(o!`)Xgj_NQFeTgU|(WK%4D{9g&<^ZOpMMAizrik5g0>qbS zen-m%asj(W8~`DxXsD394Isy{L$a`}{(n*wWt_~LcDr&H&7p(lkZC-~Se=2})^c8XD#fconIMn=fA)LVE^Y zNpAYJ*O4=Tp8}=SI~F<$Qn6wL0fHdF>2$(yI7GAAL>$MM&1L|A)tq-fh{xPQ_YJ23
-

Matita - <<Filename>>

+

<<Filename>>

diff --git a/matitaB/matita/html/matitaweb.css b/matitaB/matita/html/matitaweb.css index 84774427f..11fdb1717 100644 --- a/matitaB/matita/html/matitaweb.css +++ b/matitaB/matita/html/matitaweb.css @@ -148,6 +148,12 @@ div.matitaapparea { color:black; } +h2#matitaTitle { + display: inline; + padding: 6px; + vertical-align: top; +} + .smallmargin { margin:4px !important; } diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js index 3948a730f..1b97b15cf 100644 --- a/matitaB/matita/html/matitaweb.js +++ b/matitaB/matita/html/matitaweb.js @@ -161,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('.')); } @@ -302,7 +302,7 @@ function strip_interpr() { } function strip_anchors() { - strip_tags("INPUT","anchor"); + strip_tags("IMG","anchor"); } function keypress(e) @@ -655,21 +655,23 @@ function advOneStep(xml) { 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)) { @@ -1118,7 +1120,7 @@ function gotoPos(offset) if (is_defined(xml)) { try { var len = advOneStep(xml); - if (offset <= len) { + if (len == 0 || offset <= len) { init_hyperlinks(); init_autotraces(); populate_goalarray(metasenv); @@ -1147,6 +1149,7 @@ function gotoPos(offset) function retractStep() { + if (!is_nil(statements)) { processor = function(xml) { if (typeof xml != "undefined") { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); @@ -1177,6 +1180,7 @@ function retractStep() }; pause(); callServer("retract",processor); + } } function openFile() @@ -1219,7 +1223,7 @@ function retrieveFile(thefile) strip_anchors(); init_hyperlinks(); init_autotraces(); - + unlocked.scrollIntoView(true); } else { error("file open failed"); } @@ -1249,7 +1253,7 @@ function go_external_hyperlink(uri,thefile,id) $('#locked').html(doctext); try { // scroll to anchor (if it exists) - $('#' + id).scrollIntoView(true); + $('#' + id).get(0).scrollIntoView(true); } catch (e) { } init_hyperlinks(); init_autotraces(); @@ -1446,12 +1450,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(); }; @@ -1462,12 +1466,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(); }; diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml index 5d53a9c3e..8f969750b 100644 --- a/matitaB/matita/matitaFilesystem.ml +++ b/matitaB/matita/matitaFilesystem.ml @@ -250,6 +250,7 @@ let html_of_library uid ft = 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 = @@ -260,6 +261,7 @@ let html_of_library uid ft = 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 = diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 261811815..eba76597e 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -41,7 +41,7 @@ let add_user_for_commit uid = 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 -> @@ -146,7 +146,11 @@ let do_global_commit () = (* 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 ***) @@ -228,8 +232,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script 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 @@ -735,6 +739,10 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string "ok" with | File_already_exists -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string "cancelled" | Sys_error _ -> cgi # set_header @@ -743,6 +751,10 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~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 ("" ^ estr ^ "")); cgi#out_channel#commit_work() @@ -755,7 +767,8 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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\"" @@ -765,6 +778,13 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string ("
" ^ out ^ "
"); cgi#out_channel#output_string "" with + | Failure _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "no commit privileges" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -808,6 +828,13 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string ("
" ^ details ^ "
"); cgi#out_channel#output_string ""; with + | Failure _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "no commit privileges" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -863,6 +890,13 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body + | End_of_file _ -> + let body = "" 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 -- 2.39.2