From df4bdd480707d9807094c5b6d44b4d766cbbe37d Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Nov 2010 14:10:46 +0000
Subject: [PATCH] - dandling code (to be put somewhere) implementing recursive
 compilation

---
 matita/components/compile.ml | 38 ++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 matita/components/compile.ml

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
+;;
-- 
2.39.5