--- a/src/Pure/PIDE/batch_session.scala Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/PIDE/batch_session.scala Wed Jan 14 14:28:52 2015 +0100
@@ -44,11 +44,11 @@
prover_session.phase_changed +=
Session.Consumer[Session.Phase](getClass.getName) {
case Session.Ready =>
+ val id = Document_ID.make().toString
val master_dir = session_info.dir
- for ((_, thy_options, thy_files) <- session_info.theories) {
- val id = Document_ID.make().toString
- prover_session.use_theories(options, id, master_dir, thy_files) // FIXME proper check of result!?
- }
+ val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
+ prover_session.build_theories(id, master_dir, theories)
+ // FIXME proper check of result!?
case Session.Inactive | Session.Failed =>
result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
case Session.Shutdown =>
--- a/src/Pure/PIDE/markup.ML Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Jan 14 14:28:52 2015 +0100
@@ -186,7 +186,7 @@
val command_timing: Properties.entry
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
- val use_theories_result: string -> bool -> Properties.T
+ val build_theories_result: string -> bool -> Properties.T
val print_operationsN: string
val print_operations: Properties.T
val simp_trace_panelN: string
@@ -597,8 +597,8 @@
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
| dest_loading_theory _ = NONE;
-fun use_theories_result id ok =
- [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
+fun build_theories_result id ok =
+ [("function", "build_theories_result"), ("id", id), ("ok", print_bool ok)];
val print_operationsN = "print_operations";
val print_operations = [(functionN, print_operationsN)];
--- a/src/Pure/PIDE/markup.scala Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Jan 14 14:28:52 2015 +0100
@@ -467,11 +467,11 @@
}
}
- object Use_Theories_Result
+ object Build_Theories_Result
{
def unapply(props: Properties.T): Option[(String, Boolean)] =
props match {
- case List((FUNCTION, "use_theories_result"),
+ case List((FUNCTION, "build_theories_result"),
("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
case _ => None
}
--- a/src/Pure/PIDE/protocol.ML Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML Wed Jan 14 14:28:52 2015 +0100
@@ -111,19 +111,21 @@
handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
val _ =
- Isabelle_Process.protocol_command "use_theories"
- (fn options_yxml :: id :: master_dir :: thys =>
+ Isabelle_Process.protocol_command "build_theories"
+ (fn [id, master_dir, theories_yxml] =>
let
- val options = Options.decode (YXML.parse_body options_yxml);
+ val theories =
+ YXML.parse_body theories_yxml |>
+ let open XML.Decode
+ in list (pair Options.decode (list (string #> rpair Position.none))) end;
val result =
Exn.capture (fn () =>
- Thy_Info.use_thys_options (K NONE) (Path.explode master_dir) options
- (map (rpair Position.none) thys)) ();
+ theories |> List.app (Thy_Info.build_theories (K NONE) (Path.explode master_dir))) ();
val ok =
(case result of
Exn.Res _ => true
| Exn.Exn exn => (Runtime.exn_error_message exn; false));
- in Output.protocol_message (Markup.use_theories_result id ok) [] end);
+ in Output.protocol_message (Markup.build_theories_result id ok) [] end);
val _ =
Isabelle_Process.protocol_command "ML_System.share_common_data"
--- a/src/Pure/PIDE/protocol.scala Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Jan 14 14:28:52 2015 +0100
@@ -456,8 +456,8 @@
def remove_versions(versions: List[Document.Version])
{
val versions_yxml =
- { import XML.Encode._
- YXML.string_of_body(list(long)(versions.map(_.id))) }
+ { import XML.Encode._
+ YXML.string_of_body(list(long)(versions.map(_.id))) }
protocol_command("Document.remove_versions", versions_yxml)
}
@@ -468,10 +468,13 @@
protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
- /* use_theories */
+ /* build_theories */
- def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path]): Unit =
- protocol_command("use_theories",
- (YXML.string_of_body(Options.encode(options)) ::
- id :: master_dir.implode :: thys.map(_.implode)): _*)
+ def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
+ {
+ val theories_yxml =
+ { import XML.Encode._
+ YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) }
+ protocol_command("build_theories", id, master_dir.implode, theories_yxml)
+ }
}
--- a/src/Pure/PIDE/session.scala Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/PIDE/session.scala Wed Jan 14 14:28:52 2015 +0100
@@ -63,7 +63,7 @@
case object Caret_Focus
case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
- case class Use_Theories(options: Options, id: String, master_dir: Path, thys: List[Path])
+ case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
case class Commands_Changed(
assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -554,8 +554,8 @@
prover.get.dialog_result(serial, result)
handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
- case Session.Use_Theories(options, id, master_dir, thys) if prover.defined =>
- prover.get.use_theories(options, id, master_dir, thys)
+ case Session.Build_Theories(id, master_dir, theories) if prover.defined =>
+ prover.get.build_theories(id, master_dir, theories)
case Protocol_Command(name, args) if prover.defined =>
prover.get.protocol_command(name, args:_*)
@@ -620,6 +620,6 @@
def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
{ manager.send(Session.Dialog_Result(id, serial, result)) }
- def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path])
- { manager.send(Session.Use_Theories(options, id, master_dir, thys)) }
+ def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
+ { manager.send(Session.Build_Theories(id, master_dir, theories)) }
}
--- a/src/Pure/Thy/thy_info.ML Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Jan 14 14:28:52 2015 +0100
@@ -14,8 +14,8 @@
val remove_thy: string -> unit
val use_thys: (string * Position.T) list -> unit
val use_thy: string * Position.T -> unit
- val use_thys_options: (Toplevel.transition -> Time.time option) -> Path.T ->
- Options.T -> (string * Position.T) list -> unit
+ val build_theories: (Toplevel.transition -> Time.time option) -> Path.T ->
+ Options.T * (string * Position.T) list -> unit
val script_thy: Position.T -> string -> theory -> theory
val register_thy: theory -> unit
val finish: unit -> unit
@@ -342,18 +342,30 @@
val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
val use_thy = use_thys o single;
-fun use_thys_options last_timing master_dir options thys =
- (Options.set_default options;
- (use_theories {
- document = Present.document_enabled (Options.string options "document"),
- last_timing = last_timing,
- master_dir = master_dir}
- |> Unsynchronized.setmp print_mode
- (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
- |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
- |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
- |> Multithreading.max_threads_setmp (Options.int options "threads")
- |> Unsynchronized.setmp Future.ML_statistics true) thys);
+
+(* theories in batch build *)
+
+fun build_theories last_timing master_dir (options, thys) =
+ let
+ val condition = space_explode "," (Options.string options "condition");
+ val conds = filter_out (can getenv_strict) condition;
+ in
+ if null conds then
+ (Options.set_default options;
+ (use_theories {
+ document = Present.document_enabled (Options.string options "document"),
+ last_timing = last_timing,
+ master_dir = master_dir}
+ |> Unsynchronized.setmp print_mode
+ (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+ |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+ |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+ |> Multithreading.max_threads_setmp (Options.int options "threads")
+ |> Unsynchronized.setmp Future.ML_statistics true) thys)
+ else
+ Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
+ " (undefined " ^ commas conds ^ ")\n")
+ end;
(* toplevel scripting -- without maintaining database *)
--- a/src/Pure/Tools/build.ML Wed Jan 14 11:52:08 2015 +0100
+++ b/src/Pure/Tools/build.ML Wed Jan 14 14:28:52 2015 +0100
@@ -97,17 +97,6 @@
(* build *)
-fun use_theories last_timing master_dir (options, thys) =
- let val condition = space_explode "," (Options.string options "condition") in
- (case filter_out (can getenv_strict) condition of
- [] =>
- Thy_Info.use_thys_options last_timing master_dir options
- (map (rpair Position.none) thys)
- | conds =>
- Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
- " (undefined " ^ commas conds ^ ")\n"))
- end;
-
fun build args_file = Command_Line.tool0 (fn () =>
let
val _ = SHA1_Samples.test ();
@@ -118,7 +107,7 @@
let open XML.Decode in
pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string
- ((list (pair Options.decode (list string))))))))))))
+ ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
end;
val _ = Options.set_default options;
@@ -140,7 +129,7 @@
val res1 =
theories |>
- (List.app (use_theories last_timing Path.current)
+ (List.app (Thy_Info.build_theories last_timing Path.current)
|> session_timing name verbose
|> Unsynchronized.setmp Output.protocol_message_fn protocol_message
|> Multithreading.max_threads_setmp (Options.int options "threads")