From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 30 Sep 2011 12:38:25 +0000 (+0000)
Subject: Matitaweb: Some bugfixes concerning file flags.
X-Git-Tag: make_still_working~2260
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=92a81bb9f7e51807585feb00f102b1f02d6cf1d3

Matitaweb: Some bugfixes concerning file flags.
---

diff --git a/matitaB/matita/matitaAuthentication.ml b/matitaB/matita/matitaAuthentication.ml
index 566965851..86189fddf 100644
--- 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 b846c153c..77e658221 100644
--- 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 f1906b1e8..4d1bd50d8 100644
--- 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 3b37fc76b..349097719 100644
--- 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") {