From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Nov 2010 14:10:46 +0000 (+0000)
Subject: - dandling code (to be put somewhere) implementing recursive compilation
X-Git-Tag: make_still_working~2736
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df4bdd480707d9807094c5b6d44b4d766cbbe37d;p=helm.git

- dandling code (to be put somewhere) implementing recursive compilation
---

diff --git a/matita/components/compile.ml b/matita/components/compile.ml
new file mode 100644
index 000000000..0389a0394
--- /dev/null
+++ b/matita/components/compile.ml
@@ -0,0 +1,38 @@
+let rec assert_ng mapath ngpath =
+ let to_be_compiled =
+  if exists_file ngpath then
+    let preamble = preamble_of_ngpath ngpath in
+    let children_bad = List.exists assert_ng preamble in
+     children_bad || date mapath > date ngpath
+  else
+   true
+ in
+  if to_be_compiled then
+   if already_loaded ngpath then
+     (* maybe recompiling it I would get the same... *)
+     raise (AlreadyLoaded mapath)
+   else
+    begin
+      compile mapath;
+      true
+    end
+  else
+   false
+
+and compile mapath =
+ let oldstatus = status in
+ let status = toplevel (new status) (content_of mapath) in
+  salva_su_disco status;
+  oldstatus
+
+and toplevel status testo =
+ List.fold
+  (fun status cmd ->
+    match cmd with
+      Include mapath ->
+         let ngpath = ... mapath in
+         assert_ng mapath ngpath;
+         carico ngpath
+    | -> ...
+  ) status testo
+;;