Added module MatitaFilesystem, to be used for the management of the library

in matitaweb.

diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile
index a9018f16f10f7eb1cd56949278948fa7a78e830e..d0219f43002e2235814944857e0324dcc8e2820a 100644 (file)
--- a/matitaB/matita/Makefile
+++ b/matitaB/matita/Makefile
@@ -68,6 +68,7 @@ WMLI =                                \
        matitaExcPp.mli         \
        matitaInit.mli          \
        matitaAuthentication.mli \
+       matitaFilesystem.mli    \
        $(NULL)
 MAINCMLI =                     \
        matitaclean.mli         \
@@ -101,6 +102,13 @@ matitaAuthentication.cmo: matitaAuthentication.ml
        $(H)echo "  OCAMLC $<"
        $(H)$(OCAMLC) $(WPKGS) -c $<
 
+matitaFilesystem.cmi: matitaFilesystem.mli
+       $(H)echo "  OCAMLC $<"
+       $(H)$(OCAMLC) $(WPKGS) -c $<
+matitaFilesystem.cmo: matitaFilesystem.ml
+       $(H)echo "  OCAMLC $<"
+       $(H)$(OCAMLC) $(WPKGS) -c $<
+
 CMOS = $(ML:%.ml=%.cmo)
 CCMOS = $(CML:%.ml=%.cmo)
 WCMOS = $(WML:%.ml=%.cmo)

diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html
index f713edb177d71dd8b12a001b24d88bada9221673..223aefa3e7dde49aa79ce6ba0b486ba59f235a91 100644 (file)
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -24,9 +24,9 @@
           <A href="javascript:gotoBottom()"><IMG src="icons/bottom.png" 
                                                   id="bottom" alt="Bottom" title="Execute the whole script."></A>
        <INPUT type="TEXT" id="filename" value=""><INPUT type="BUTTON" value="Open" ONCLICK="openFile()"></p>
-          <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
+<!--      <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()">
+          <INPUT type="BUTTON" value="selection test" id="hideseq" ONCLICK="test()"> -->
 
 </td>
 <td style="width:33%; text-align:center;"><img src="icons/matita-text.png"></td>

diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml
new file mode 100644 (file)
index 0000000..1809627
--- /dev/null
+++ b/matitaB/matita/matitaFilesystem.ml
@@ -0,0 +1,57 @@
+(* Copyright (C) 2004-2011, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let exec_process cmd =
+  let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in
+  let outlines = ref [] in
+  let errlines = ref [] in
+  (try
+     while true do
+       outlines := input_line stdout :: !outlines;
+     done;
+     assert false
+   with End_of_file -> 
+   (try
+     while true do
+       errlines := input_line stderr :: !errlines;
+     done;
+     assert false
+    with End_of_file -> 
+     match (Unix.close_process_full chs) with
+     | Unix.WEXITED errno -> 
+        let output = "std out =\n" ^ String.concat "\n" (List.rev !outlines) in
+        let errors = "std err =\n" ^ String.concat "\n" (List.rev !errlines) in
+        errno, output ^ "\n\n" ^ errors
+     | _ -> assert false))
+
+let checkout user =
+  let rt_dir = Helm_registry.get "matita.rt_base_dir" in
+  let repo = Helm_registry.get "matita.weblib" in
+
+  let errno, outstr = 
+    exec_process ("svn co " ^ repo ^ " " ^ rt_dir ^ "/" ^ user ^ "/scripts")
+  in
+  if errno = 0 then "checkout successful!"
+  else "checkout error!\n\n" ^ outstr

diff --git a/matitaB/matita/matitaFilesystem.mli b/matitaB/matita/matitaFilesystem.mli
new file mode 100644 (file)
index 0000000..eba9d1d
--- /dev/null
+++ b/matitaB/matita/matitaFilesystem.mli
@@ -0,0 +1 @@
+val checkout : string -> string

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 492edd56e425ac73b9fcbee296021942f288aadb..840442665e9c047806a9d05243587f3e345ad314 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -492,6 +492,7 @@ let start() =
                 ; "logout", do_logout ]
       () in
   MatitaInit.initialize_all ();
+  prerr_endline (MatitaFilesystem.checkout "ricciott");
   MatitaAuthentication.deserialize ();
   Netplex_main.startup
     parallelizer