src/Pure/System/build.ML
author wenzelm
Sat Jul 21 16:41:55 2012 +0200 (2012-07-21 ago)
changeset 48418 1a634f9614fb
child 48419 6d7b6e47f3ef
permissions -rw-r--r--
some actual build function on ML side;
further imitation of "usedir" shell script;
wenzelm@48418
     1
(*  Title:      Pure/System/build.ML
wenzelm@48418
     2
    Author:     Makarius
wenzelm@48418
     3
wenzelm@48418
     4
Build Isabelle sessions.
wenzelm@48418
     5
*)
wenzelm@48418
     6
wenzelm@48418
     7
signature BUILD =
wenzelm@48418
     8
sig
wenzelm@48418
     9
  val build: string -> unit
wenzelm@48418
    10
end;
wenzelm@48418
    11
wenzelm@48418
    12
structure Build: BUILD =
wenzelm@48418
    13
struct
wenzelm@48418
    14
wenzelm@48418
    15
fun build args_file =
wenzelm@48418
    16
  let
wenzelm@48418
    17
    val (build_images, (parent, (name, theories))) =
wenzelm@48418
    18
      File.read (Path.explode args_file) |> YXML.parse_body |>
wenzelm@48418
    19
        let open XML.Decode in pair bool (pair string (pair string (list string))) end;
wenzelm@48418
    20
wenzelm@48418
    21
    val _ = Session.init false parent name;  (* FIXME reset!? *)
wenzelm@48418
    22
    val _ = Thy_Info.use_thys theories;
wenzelm@48418
    23
    val _ = Session.finish ();
wenzelm@48418
    24
wenzelm@48418
    25
    val _ = if build_images then () else quit ();
wenzelm@48418
    26
  in () end
wenzelm@48418
    27
  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
wenzelm@48418
    28
wenzelm@48418
    29
end;