branch (Filename.basename path) (subdirtags ^ "\n" ^ scripttags)
in
- let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
+ let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
let res = aux basedir in
prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
res
let sid = HExtlib.unopt sid in
cgi # set_header
~cache:`No_cache
- ~content_type:"text/xml; charset=\"utf-8\""
+ ~content_type:"text/html; charset=\"utf-8\""
();
let uid = MatitaAuthentication.user_of_session sid in
let html = MatitaFilesystem.html_of_library uid in
cgi#out_channel#output_string
- ("<html><head></head><body>" ^ html ^ "</body></html>");
+ ("<html><head>\n" ^
+ "<title>XML Tree Control</title>\n" ^
+ "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
+ "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
+ "<body>\n" ^ html ^ "\n</body></html>");
cgi#out_channel#commit_work()
;;
--- /dev/null
+body{\r
+ font: 10pt Verdana,sans-serif;\r
+ color: navy;\r
+}\r
+.trigger{\r
+ cursor: pointer;\r
+ cursor: hand;\r
+ display: block;\r
+}\r
+.branch{\r
+ display: none;\r
+ margin-left: 16px;\r
+}\r
+a{\r
+ text-decoration: none;\r
+}\r
+a:hover{\r
+ text-decoration: underline;\r
+}\r
--- /dev/null
+var openImg = new Image();\r
+openImg.src = "open.gif";\r
+var closedImg = new Image();\r
+closedImg.src = "closed.gif";\r
+\r
+function showBranch(branch){\r
+ var objBranch = document.getElementById(branch).style;\r
+ if(objBranch.display=="block")\r
+ objBranch.display="none";\r
+ else\r
+ objBranch.display="block";\r
+ swapFolder('I' + branch);\r
+}\r
+\r
+function swapFolder(img){\r
+ objImg = document.getElementById(img);\r
+ if(objImg.src.indexOf('closed.gif')>-1)\r
+ objImg.src = openImg.src;\r
+ else\r
+ objImg.src = closedImg.src;\r
+}\r
projects / helm.git / commitdiff
