# HG changeset patch # User wenzelm # Date 1421242132 -3600 # Node ID 3b5da177ae6b74987c351065db7e5921bcc36ce4 # Parent 4660b0409096a24338b429a7eec2d735c9b10d3b clarified build_theories; diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/PIDE/batch_session.scala --- 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 => diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/PIDE/markup.ML --- 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)]; diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/PIDE/markup.scala --- 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 } diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/PIDE/protocol.ML --- 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" diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/PIDE/protocol.scala --- 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) + } } diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/PIDE/session.scala --- 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)) } } diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/Thy/thy_info.ML --- 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 *) diff -r 4660b0409096 -r 3b5da177ae6b src/Pure/Tools/build.ML --- 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")