src/Pure/Tools/build.ML
changeset 59366 e94df7f6b608
parent 59364 3b5da177ae6b
child 59368 100db5cf5be5
     1.1 --- a/src/Pure/Tools/build.ML	Wed Jan 14 16:23:33 2015 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Wed Jan 14 16:27:19 2015 +0100
     1.3 @@ -97,6 +97,28 @@
     1.4  
     1.5  (* build *)
     1.6  
     1.7 +fun build_theories last_timing master_dir (options, thys) =
     1.8 +  let
     1.9 +    val condition = space_explode "," (Options.string options "condition");
    1.10 +    val conds = filter_out (can getenv_strict) condition;
    1.11 +  in
    1.12 +    if null conds then
    1.13 +      (Options.set_default options;
    1.14 +        (Thy_Info.use_theories {
    1.15 +          document = Present.document_enabled (Options.string options "document"),
    1.16 +          last_timing = last_timing,
    1.17 +          master_dir = master_dir}
    1.18 +        |> Unsynchronized.setmp print_mode
    1.19 +            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    1.20 +        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    1.21 +        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    1.22 +        |> Multithreading.max_threads_setmp (Options.int options "threads")
    1.23 +        |> Unsynchronized.setmp Future.ML_statistics true) thys)
    1.24 +    else
    1.25 +      Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
    1.26 +        " (undefined " ^ commas conds ^ ")\n")
    1.27 +  end;
    1.28 +
    1.29  fun build args_file = Command_Line.tool0 (fn () =>
    1.30      let
    1.31        val _ = SHA1_Samples.test ();
    1.32 @@ -129,7 +151,7 @@
    1.33  
    1.34        val res1 =
    1.35          theories |>
    1.36 -          (List.app (Thy_Info.build_theories last_timing Path.current)
    1.37 +          (List.app (build_theories last_timing Path.current)
    1.38              |> session_timing name verbose
    1.39              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    1.40              |> Multithreading.max_threads_setmp (Options.int options "threads")
    1.41 @@ -141,4 +163,24 @@
    1.42        val _ = if do_output then () else exit 0;
    1.43      in () end);
    1.44  
    1.45 +
    1.46 +(* PIDE protocol *)
    1.47 +
    1.48 +val _ =
    1.49 +  Isabelle_Process.protocol_command "build_theories"
    1.50 +    (fn [id, master_dir, theories_yxml] =>
    1.51 +      let
    1.52 +        val theories =
    1.53 +          YXML.parse_body theories_yxml |>
    1.54 +            let open XML.Decode
    1.55 +            in list (pair Options.decode (list (string #> rpair Position.none))) end;
    1.56 +        val result =
    1.57 +          Exn.capture (fn () =>
    1.58 +            theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
    1.59 +        val ok =
    1.60 +          (case result of
    1.61 +            Exn.Res _ => true
    1.62 +          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    1.63 +    in Output.protocol_message (Markup.build_theories_result id ok) [] end);
    1.64 +
    1.65  end;