# HG changeset patch
# User wenzelm
# Date 1592656587 -7200
# Node ID 842dd262540b8a49fa2c1f1ddbad762bd64c4095
# Parent  ec0ef3ebe75ec46e7ee8a57f6ae3c075597d8b14
more caching, notably for build/pide_session;

diff -r ec0ef3ebe75e -r 842dd262540b src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Jun 20 11:01:57 2020 +0200
+++ b/src/Pure/PIDE/prover.scala	Sat Jun 20 14:36:27 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)