From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 5 Nov 2010 16:25:03 +0000 (+0000)
Subject: now implemented in matitaEngine.ml
X-Git-Tag: make_still_working~2708
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03df2a0a7056751d7e82e111567af2f83ea41932;p=helm.git

now implemented in matitaEngine.ml
---

diff --git a/matita/components/compile.ml b/matita/components/compile.ml
deleted file mode 100644
index 0389a0394..000000000
--- a/matita/components/compile.ml
+++ /dev/null
@@ -1,38 +0,0 @@
-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
-;;