Subject: [PATCH] store only ID in command_timings of Node_Status: avoids keeping markup in memory;
---
Index: src/Tools/jEdit/src/timing_dockable.scala
IDEA additional info:
Subsystem: com.intellij.openapi.diff.impl.patch.CharsetEP
<+>UTF-8
===================================================================
diff --git a/src/Tools/jEdit/src/timing_dockable.scala b/src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	(revision 83821:174c4514438cbdd8489968869b026088ce382198)
+++ b/src/Tools/jEdit/src/timing_dockable.scala	(revision 83822:79d2779c890ff739d3dd94d174f190324296cd43)
@@ -133,7 +133,7 @@
 
   private var nodes_status = Document_Status.Nodes_Status.empty
 
-  private def make_entries(): List[Entry] = {
+  private def make_entries(snapshot: Document.Snapshot): List[Entry] = {
     GUI_Thread.require {}
 
     val name =
@@ -149,8 +149,10 @@
         for ((a, st) <- nodes_status.iterator if st.command_timings.nonEmpty)
           yield Theory_Entry(a, st.cumulated_time.seconds)).sorted(Entry.Ordering)
     val commands =
-      (for ((command, timings) <- nodes_status(name).command_timings.toList)
-        yield Command_Entry(command, timings.sum(now).seconds)).sorted(Entry.Ordering)
+      (for {
+        (command_id, timings) <- nodes_status(name).command_timings.toList
+        (_, command) <- snapshot.find_command(command_id)
+      } yield Command_Entry(command, timings.sum(now).seconds)).sorted(Entry.Ordering)
 
     theories.flatMap(entry =>
       if (entry.name == name) entry.make_current :: commands
@@ -172,7 +174,7 @@
         threshold = Time.seconds(timing_threshold),
         domain = Some(domain))
 
-    val entries = make_entries()
+    val entries = make_entries(snapshot)
     if (timing_view.listData.toList != entries) timing_view.listData = entries
   }
 
Index: src/Pure/PIDE/document_status.scala
IDEA additional info:
Subsystem: com.intellij.openapi.diff.impl.patch.CharsetEP
<+>UTF-8
===================================================================
diff --git a/src/Pure/PIDE/document_status.scala b/src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	(revision 83821:174c4514438cbdd8489968869b026088ce382198)
+++ b/src/Pure/PIDE/document_status.scala	(revision 83822:79d2779c890ff739d3dd94d174f190324296cd43)
@@ -270,7 +270,7 @@
       var terminated = true
       var cumulated_time = Time.zero
       var max_time = Time.zero
-      var command_timings = Map.empty[Command, Command_Timings]
+      var command_timings = Map.empty[Document_ID.Command, Command_Timings]
 
       for (command <- node.commands.iterator) {
         val status = state.command_status(version, command)
@@ -289,7 +289,7 @@
         val t = status.timings.sum(now)
         cumulated_time += t
         if (t > max_time) max_time = t
-        if (t.is_notable(threshold)) command_timings += (command -> status.timings)
+        if (t.is_notable(threshold)) command_timings += (command.id -> status.timings)
       }
 
       def percent(a: Int, b: Int): Int =
@@ -341,7 +341,7 @@
     cumulated_time: Time = Time.zero,
     max_time: Time = Time.zero,
     threshold: Time = Time.zero,
-    command_timings: Map[Command, Command_Timings] = Map.empty,
+    command_timings: Map[Document_ID.Command, Command_Timings] = Map.empty,
     percentage: Int = 0
   ) extends Theory_Status {
     def is_empty: Boolean = this == Node_Status.empty