# HG changeset patch # User wenzelm # Date 1592663792 -7200 # Node ID 9d98a39aa509b7185c5e4c35b959b2c2c02b822d # Parent e18e9ac8c2051910725631b7c9ab22833a3d8a26# Parent 34be842f35310ccfe8692f536c374024a54412d1 merged diff -r e18e9ac8c205 -r 9d98a39aa509 etc/options --- 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" diff -r e18e9ac8c205 -r 9d98a39aa509 src/Pure/Admin/build_history.scala --- 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 = diff -r e18e9ac8c205 -r 9d98a39aa509 src/Pure/PIDE/protocol_handlers.scala --- 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) diff -r e18e9ac8c205 -r 9d98a39aa509 src/Pure/PIDE/prover.scala --- 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) diff -r e18e9ac8c205 -r 9d98a39aa509 src/Pure/PIDE/session.scala --- 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 { diff -r e18e9ac8c205 -r 9d98a39aa509 src/Pure/Thy/sessions.scala --- 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 => diff -r e18e9ac8c205 -r 9d98a39aa509 src/Pure/Tools/build.scala --- 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)