matita/components/compile.ml

   1 let rec assert_ng mapath ngpath =
   2  let to_be_compiled =
   3   if exists_file ngpath then
   4     let preamble = preamble_of_ngpath ngpath in
   5     let children_bad = List.exists assert_ng preamble in
   6      children_bad || date mapath > date ngpath
   7   else
   8    true
   9  in
  10   if to_be_compiled then
  11    if already_loaded ngpath then
  12      (* maybe recompiling it I would get the same... *)
  13      raise (AlreadyLoaded mapath)
  14    else
  15     begin
  16       compile mapath;
  17       true
  18     end
  19   else
  20    false
  21
  22 and compile mapath =
  23  let oldstatus = status in
  24  let status = toplevel (new status) (content_of mapath) in
  25   salva_su_disco status;
  26   oldstatus
  27
  28 and toplevel status testo =
  29  List.fold
  30   (fun status cmd ->
  31     match cmd with
  32       Include mapath ->
  33          let ngpath = ... mapath in
  34          assert_ng mapath ngpath;
  35          carico ngpath
  36     | -> ...
  37   ) status testo
  38 ;;