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