--- a/etc/options Sat Jun 20 05:56:28 2020 +0000
+++ b/etc/options Sat Jun 20 16:36:32 2020 +0200
@@ -153,9 +153,6 @@
option pide_session : bool = false
-- "build session heaps via PIDE"
-option pide_exports : bool = true
- -- "store PIDE export artifacts"
-
option pide_reports : bool = true
-- "report PIDE markup"
--- a/src/Pure/Admin/build_history.scala Sat Jun 20 05:56:28 2020 +0000
+++ b/src/Pure/Admin/build_history.scala Sat Jun 20 16:36:32 2020 +0200
@@ -240,11 +240,14 @@
val build_start = Date.now()
val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
- val build_result =
+
+ val build_isabelle =
Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
- user_home = user_home, progress = build_out_progress)(
- "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
- strict = false)
+ user_home = user_home, progress = build_out_progress)
+ val build_result =
+ build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions),
+ redirect = true, echo = true, strict = false)
+
val build_end = Date.now()
val build_info: Build_Log.Build_Info =
--- a/src/Pure/PIDE/protocol_handlers.scala Sat Jun 20 05:56:28 2020 +0000
+++ b/src/Pure/PIDE/protocol_handlers.scala Sat Jun 20 16:36:32 2020 +0200
@@ -16,7 +16,7 @@
sealed case class State(
session: Session,
handlers: Map[String, Session.Protocol_Handler] = Map.empty,
- functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
+ functions: Map[String, Session.Protocol_Function] = Map.empty)
{
def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
--- a/src/Pure/PIDE/prover.scala Sat Jun 20 05:56:28 2020 +0000
+++ b/src/Pure/PIDE/prover.scala Sat Jun 20 16:36:32 2020 +0200
@@ -77,7 +77,7 @@
private def protocol_output(props: Properties.T, bytes: Bytes)
{
- receiver(new Prover.Protocol_Output(props, bytes))
+ receiver(new Prover.Protocol_Output(xml_cache.props(props), bytes))
}
private def output(kind: String, props: Properties.T, body: XML.Body)
--- a/src/Pure/PIDE/session.scala Sat Jun 20 05:56:28 2020 +0000
+++ b/src/Pure/PIDE/session.scala Sat Jun 20 16:36:32 2020 +0200
@@ -111,11 +111,13 @@
/* protocol handlers */
+ type Protocol_Function = Prover.Protocol_Output => Boolean
+
abstract class Protocol_Handler
{
def init(session: Session): Unit = {}
def exit(): Unit = {}
- val functions: List[(String, Prover.Protocol_Output => Boolean)]
+ val functions: List[(String, Protocol_Function)]
}
}
@@ -501,11 +503,9 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
- if (session_options.bool("pide_exports")) {
- val id = Value.Long.unapply(args.id.get).get
- val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
- change_command(_.add_export(id, (args.serial, export)))
- }
+ val id = Value.Long.unapply(args.id.get).get
+ val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+ change_command(_.add_export(id, (args.serial, export)))
case List(Markup.Commands_Accepted.PROPERTY) =>
msg.text match {
--- a/src/Pure/Thy/sessions.scala Sat Jun 20 05:56:28 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Sat Jun 20 16:36:32 2020 +0200
@@ -1085,6 +1085,9 @@
{
override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
+ val xml_cache: XML.Cache = XML.make_cache()
+ val xz_cache: XZ.Cache = XZ.make_cache()
+
/* directories */
@@ -1199,9 +1202,6 @@
/* SQL database content */
- val xml_cache: XML.Cache = XML.make_cache()
- val xz_cache: XZ.Cache = XZ.make_cache()
-
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
db.using_statement(Session_Info.table.select(List(column),
Session_Info.session_name.where_equal(name)))(stmt =>
--- a/src/Pure/Tools/build.scala Sat Jun 20 05:56:28 2020 +0000
+++ b/src/Pure/Tools/build.scala Sat Jun 20 16:36:32 2020 +0200
@@ -218,7 +218,11 @@
if (options.bool("pide_session")) {
val resources = new Resources(sessions_structure, deps(parent))
- val session = new Session(options, resources)
+ val session =
+ new Session(options, resources) {
+ override val xml_cache: XML.Cache = store.xml_cache
+ override val xz_cache: XZ.Cache = store.xz_cache
+ }
val build_session_errors: Promise[List[String]] = Future.promise
val stdout = new StringBuilder(1000)
@@ -228,6 +232,18 @@
val runtime_statistics = new mutable.ListBuffer[Properties.T]
val task_statistics = new mutable.ListBuffer[Properties.T]
+ def fun(
+ name: String,
+ acc: mutable.ListBuffer[Properties.T],
+ unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
+ {
+ name -> ((msg: Prover.Protocol_Output) =>
+ unapply(msg.properties) match {
+ case Some(props) => acc += props; true
+ case _ => false
+ })
+ }
+
session.init_protocol_handler(new Session.Protocol_Handler
{
override def exit() { build_session_errors.cancel }
@@ -271,39 +287,15 @@
case _ => false
}
- private def command_timing(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Command_Timing(props) => command_timings += props; true
- case _ => false
- }
-
- private def theory_timing(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Theory_Timing(props) => theory_timings += props; true
- case _ => false
- }
-
- private def ml_stats(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.ML_Statistics(props) => runtime_statistics += props; true
- case _ => false
- }
-
- private def task_stats(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Task_Statistics(props) => task_statistics += props; true
- case _ => false
- }
-
val functions =
List(
Markup.Build_Session_Finished.name -> build_session_finished,
Markup.Loading_Theory.name -> loading_theory,
Markup.EXPORT -> export,
- Markup.Command_Timing.name -> command_timing,
- Markup.Theory_Timing.name -> theory_timing,
- Markup.ML_Statistics.name -> ml_stats,
- Markup.Task_Statistics.name -> task_stats)
+ fun(Markup.Command_Timing.name, command_timings, Markup.Command_Timing.unapply),
+ fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
+ fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply),
+ fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
})
session.all_messages += Session.Consumer[Any]("build_session_output")
@@ -492,7 +484,6 @@
"ML_statistics" +
"completion_limit=0" +
"editor_tracing_messages=0" +
- "pide_exports=false" +
"pide_reports=false"
val store = Sessions.store(build_options)