Bug fixing + cosmetic changes

diff --git a/matitaB/matita/html/icons/matita-32.png b/matitaB/matita/html/icons/matita-32.png
new file mode 100644 (file)
index 0000000..91d6e2a
Binary files /dev/null and b/matitaB/matita/html/icons/matita-32.png differ

diff --git a/matitaB/matita/html/index.html b/matitaB/matita/html/index.html
index 7f921c69cd0f7eae5f1ba469dd2b03cc9b7ee1cc..b34fa6b8f1c287360cccb615b9b69f4bff323842 100644 (file)
--- a/matitaB/matita/html/index.html
+++ b/matitaB/matita/html/index.html
@@ -28,7 +28,7 @@
 
 <div class="toparea ui-layout-north" id="toparea">
 <div class="titlebar" id="titlebar">
-  <div class="mainTitle"><H2 id="matitaTitle">Matita - &lt;&lt;Filename&gt;&gt;</H2></div>
+  <div class="mainTitle"><img src="icons/matita-32.png"><H2 id="matitaTitle">&lt;&lt;Filename&gt;&gt;</H2></div>
   <div class="mainRight" id="matitaLogout"><A id="hlogout" href="/logout.html">Log out</A></div>
 </div>
 

diff --git a/matitaB/matita/html/matitaweb.css b/matitaB/matita/html/matitaweb.css
index 84774427f90a0d107ee71d8a5a56f4eddeca70d2..11fdb1717d7ed1400d1a19154c3f9a5044d7e39a 100644 (file)
--- 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 3948a730fb3906f9640cff860e5e0630171706ec..1b97b15cf893c9c42f513e34a533554d8336104b 100644 (file)
--- 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 5d53a9c3e3395b09695d81a6325034812a75e44e..8f969750ba78c34dfe59bddd4673b5da909bcb07 100644 (file)
--- 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 261811815d3c1705d41de529c789ac19cb9ad4a9..eba76597e9e896805d30cd92f511ee9b9d67bbd7 100644 (file)
--- 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 "<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
@@ -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 ("<response>" ^ estr ^ "</response>"));
   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 ("<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
@@ -808,6 +828,13 @@ let svn_update  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     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
@@ -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 = "<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