merged
authorwenzelm
Sat, 20 Jun 2020 16:36:32 +0200
changeset 72200 9d98a39aa509
parent 72199 e18e9ac8c205 (current diff)
parent 72197 34be842f3531 (diff)
child 72201 2108c0e7ce13
merged
--- 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)