Matitaweb: Some bugfixes concerning file flags.

diff --git a/matitaB/matita/matitaAuthentication.ml b/matitaB/matita/matitaAuthentication.ml
index 5669658513a13f1d0e03748abbca6157585c9b1c..86189fddf6ec54c8a20995c2b952b7271470e73a 100644 (file)
--- a/matitaB/matita/matitaAuthentication.ml
+++ b/matitaB/matita/matitaAuthentication.ml
@@ -136,7 +136,8 @@ let read_ft uid =
       [] 
 ;;
 
-let set_file_flag uid filename flag = 
+let set_file_flag uid filename flag =
+  let filename = MatitaFilesystem.normalize_qfn filename in 
   let ft = read_ft uid in
   let oldflag = 
     try List.assoc filename ft

diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml
index b846c153ca5274a7892c3c24ecfe4da231f10f64..77e65822163657ffc7af9fce3bb662999f41148e 100644 (file)
--- a/matitaB/matita/matitaFilesystem.ml
+++ b/matitaB/matita/matitaFilesystem.ml
@@ -154,45 +154,65 @@ let checkout user =
   if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files 
   else raise (SvnError (string_of_output outlines errlines))
 
+(* normalize qualified file name *)
+let normalize_qfn p = 
+  (* trim leading "./" *)
+  let p = 
+    try
+      if String.sub p 0 2 <> "./" then p
+      else String.sub p 2 (String.length p - 2)
+    with
+    | Invalid_argument _ -> p
+  in
+  (* trim trailing "/" *)
+  try
+    if String.sub p (String.length p - 1) 1 <> "/" then p
+    else String.sub p 0 (String.length p - 1)
+  with
+  | Invalid_argument _ -> p
+    
 let html_of_library uid ft =
   let i = ref 0 in
   let newid () = incr i; ("node" ^ string_of_int !i) in
 
   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
 
+
   let branch lpath children =
     let id = newid () in
     let name = Filename.basename lpath in
     let name = if name <> "." then name else "cic:/matita" in
-    let lpath =
-      try 
-        if String.sub lpath 0 2 <> "./" then lpath 
-        else String.sub lpath 2 (String.length lpath - 2)
-      with Invalid_argument _ -> lpath
-    in
     let flag = 
       try List.assoc lpath ft 
       with Not_found -> MSynchronized in
     let szflag = string_of_matita_flag flag in
-    "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "/')\">\n" ^
+    "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "')\">\n" ^
     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
     name ^ " " ^ szflag ^ "<br/></span>\n" ^
     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
     children ^ "\n</span>"
   in
   let leaf lpath =
+    let flag = 
+      try List.assoc lpath ft 
+      with Not_found -> MSynchronized in
+    let szflag = string_of_matita_flag flag in
     "<img src=\"treeview/doc.gif\"/>\n" ^
     "<a href=\"javascript:void(0)\" onClick=\"selectFile('" ^ lpath ^ "')\" onDblClick=\"dialogBox.callback('" ^ lpath ^ "')\">" ^ 
-     (Filename.basename lpath) ^ "</a><br/>"
+     (Filename.basename lpath) ^ " " ^ szflag ^ "</a><br/>"
   in
 
   let rec aux path =
     let lpath filename = path ^ "/" ^ filename in
     let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in
+
+    (* hide hidden dirs ... including svn stuff *)
     let dirlist = 
       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
+
+    (* only .ma scripts, hidden files excluded *)
     let scripts = 
       List.filter (fun x -> 
         try
@@ -202,10 +222,10 @@ let html_of_library uid ft =
           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
         with Not_found | Invalid_argument _ -> false) dirlist in
     let subdirtags = 
-      String.concat "\n" (List.map (fun x -> aux (lpath x)) subdirs) in
+      String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
     let scripttags =
       String.concat "\n" 
-       (List.map (fun x -> leaf (lpath x)) scripts)
+       (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts)
     in
     branch path (subdirtags ^ "\n" ^ scripttags)
   in

diff --git a/matitaB/matita/matitaFilesystem.mli b/matitaB/matita/matitaFilesystem.mli
index f1906b1e8bb40a938d081a04ac94dcd19619a0f2..4d1bd50d8d244562ff6533f373350e3aee3fa54c 100644 (file)
--- a/matitaB/matita/matitaFilesystem.mli
+++ b/matitaB/matita/matitaFilesystem.mli
@@ -33,3 +33,5 @@ val do_global_commit : unit -> string list
 val update_user : string -> (string * svn_flag list) list * string list
 
 val stat_user : string -> (string * svn_flag list) list * string list
+
+val normalize_qfn : string -> string

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 3b37fc76b0abf1537fc06203b5bda68274163b4a..349097719c405584c88f49a166e99c6ebac399e2 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -688,6 +688,7 @@ function retrieveFile(thefile)
        processor = function(xml)
        {
                if (is_defined(xml)) {  
+                       current_fname = thefile;
                        lockedbackup = ""
                        locked.innerHTML = lockedbackup;
                         // code originally used in google chrome (problems with mozilla)
@@ -701,7 +702,6 @@ function retrieveFile(thefile)
                }
        };
        dialogBox.style.display = "none";
-       current_fname = thefile;
        callServer("open",processor,"file=" + escape(thefile)); 
 }
 
@@ -816,6 +816,7 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
            // when force is true, reloadDialog is not needed 
         }
        processor = function(xml) {
+               current_fname = fname;
                if (is_defined(xml)) {
                  if (xml.childNodes[0].textContent != "ok") {
                     if (confirm("File already exists. All existing data will be lost.\nDo you want to proceed anyway?")) {
@@ -847,8 +848,6 @@ function createDir() {
    abortDialog();
    dirname = prompt("New directory name:\ncic:/matita/","newdir");
    if (dirname != null) {
-        if (dirname.substr(0,1) != "/")
-          dirname = "/" + dirname;
        processor = function(xml) {
                if (is_defined(xml)) {
                  if (xml.childNodes[0].textContent != "ok") {