From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 16 Jun 2011 14:52:19 +0000 (+0000)
Subject: Added module MatitaFilesystem, to be used for the management of the library
X-Git-Tag: make_still_working~2434
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0fe4fa6c136cc80037a9fbf1997cbb1d6763a3c;p=helm.git

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 a9018f16f..d0219f430 100644
--- 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 f713edb17..223aefa3e 100644
--- 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
index 000000000..1809627ca
--- /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
index 000000000..eba9d1dde
--- /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 492edd56e..840442665 100644
--- 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