1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/System/build.ML Sat Jul 21 16:41:55 2012 +0200
1.3 @@ -0,0 +1,29 @@
1.4 +(* Title: Pure/System/build.ML
1.5 + Author: Makarius
1.6 +
1.7 +Build Isabelle sessions.
1.8 +*)
1.9 +
1.10 +signature BUILD =
1.11 +sig
1.12 + val build: string -> unit
1.13 +end;
1.14 +
1.15 +structure Build: BUILD =
1.16 +struct
1.17 +
1.18 +fun build args_file =
1.19 + let
1.20 + val (build_images, (parent, (name, theories))) =
1.21 + File.read (Path.explode args_file) |> YXML.parse_body |>
1.22 + let open XML.Decode in pair bool (pair string (pair string (list string))) end;
1.23 +
1.24 + val _ = Session.init false parent name; (* FIXME reset!? *)
1.25 + val _ = Thy_Info.use_thys theories;
1.26 + val _ = Session.finish ();
1.27 +
1.28 + val _ = if build_images then () else quit ();
1.29 + in () end
1.30 + handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
1.31 +
1.32 +end;