Matitaweb: Some changes in file selection dialogbox.

diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html
index 9a2343aa43c5ca32bc2d3b8da3949fc004cf6ffa..28e0ef68a304ca30b3360e04bbfb40d90234925a 100644 (file)
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -26,10 +26,10 @@
                                                id="cursor" alt="Play"
                                                title="Execute the script until the current position of the cursor."></A>
           <A href="javascript:gotoBottom()"><IMG src="icons/bottom.png" 
-                                                  id="bottom" alt="Bottom" title="Execute the whole script."></A>
+                                                 id="bottom" alt="Bottom" title="Execute the whole script."></A>
           <INPUT type="BUTTON" value="Browse library" id="showdialog" ONCLICK="showLibrary()">
           <INPUT type="BUTTON" value="Save" id="savebutton" ONCLICK="saveFile()">
-          <INPUT type="BUTTON" value="Commit" id="savebutton" ONCLICK="commitAll()"></p>
+          <INPUT type="BUTTON" value="Commit" id="commitbutton" ONCLICK="commitAll()"></p>
 <!--      <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
           <INPUT type="BUTTON" value="hide sequent" id="hideseq" ONCLICK="hideSequent()">
           <INPUT type="BUTTON" value="selection test" id="hideseq" ONCLICK="test()"> -->
@@ -65,6 +65,7 @@
 <div class="dialog" id="dialogBox" style="display: none;">
   <div class="diaTitle" id="dialogTitle"></div>
   <div class="scroll" id="dialogContent"></div>
+  <INPUT class="diaFile" type="text" id="dialogFilename">
 </div>
  </body>
  </html> 

diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml
index ffdf9bb0d1f7ca69e7f1d45fc10bcdd97295dafa..43fb985b984d2f1fda6a4539a5c6b437dacd496c 100644 (file)
--- a/matitaB/matita/matitaFilesystem.ml
+++ b/matitaB/matita/matitaFilesystem.ml
@@ -70,20 +70,20 @@ let html_of_library uid =
 
   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
 
-  let branch text acc =
+  let branch lpath children =
     let id = newid () in
-    let name = Filename.basename text in
+    let name = Filename.basename lpath in
     let name = if name <> "." then name else "cic:/matita" in
-    "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "')\">\n" ^
+    "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "')\">\n" ^
     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
     name ^ "<br/></span>\n" ^
     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
-    acc ^ "\n</span>"
+    children ^ "\n</span>"
   in
-  let leaf text =
+  let leaf lpath =
     "<img src=\"treeview/doc.gif\"/>\n" ^
-    "<a href=\"javascript:retrieveFile('" ^ text ^ "')\">" ^ 
-     (Filename.basename text) ^ "</a><br/>"
+    "<a href=\"javascript:retrieveFile('" ^ lpath ^ "')\">" ^ 
+     (Filename.basename lpath) ^ "</a><br/>"
   in
 
   let rec aux path =

diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css
index 5510ab677cb5d7036275ea2c0d73a16b69051d36..612c76b5a52704d213d71d5f1eea62a99a8f89e4 100644 (file)
--- a/matitaB/matita/matitaweb.css
+++ b/matitaB/matita/matitaweb.css
@@ -20,6 +20,12 @@ div.diaTitle {
        color: white;
 }
 
+input.diaFile {
+       margin-left: auto;
+       margin-right: auto;
+       width: 444px;
+}
+
 div.scroll {
        display: block;
        margin-left: auto;

diff --git a/matitaB/matita/treeview/xmlTree.js b/matitaB/matita/treeview/xmlTree.js
index 9fdbb34dddfea6706baaf1724fb9a0ff78744190..0f3547bad04894610d4f0cf4f237f538718291d1 100644 (file)
--- a/matitaB/matita/treeview/xmlTree.js
+++ b/matitaB/matita/treeview/xmlTree.js
@@ -3,13 +3,14 @@ openImg.src = "treeview/open.gif";
 var closedImg = new Image();\r
 closedImg.src = "treeview/closed.gif";\r
 \r
-function showBranch(branch){\r
+function showBranch(branch,path){\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
+       // codice per mostrare il path nella casella di testo\r
 }\r
 \r
 function swapFolder(img){\r