# HG changeset patch
# User wenzelm
# Date 1667759148 -3600
# Node ID b45db80307945785bed3b9cd126f08144a41108c
# Parent  9a6459e72868f6f639e53609c0596fc7a9d924c2
minor performance tuning;

diff -r 9a6459e72868 -r b45db8030794 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 06 18:54:32 2022 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 06 19:25:48 2022 +0100
@@ -213,9 +213,9 @@
     exports: Exports = Exports.empty,
     markups: Markups = Markups.empty
   ) {
-    def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
-    def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
-    def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
+    lazy val initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
+    lazy val consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
+    lazy val consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
 
     lazy val maybe_consolidated: Boolean = {
       var touched = false