# HG changeset patch
# User wenzelm
# Date 1551793527 -3600
# Node ID c28da0820b8b4ae3eed5d9b0ab1ef54282bb98a6
# Parent  62e47f06d22c02a0afbf3e555f50bf2f929e4857# Parent  d594997cdcf47a20b347c4496923df1f3887c794
merged

diff -r 62e47f06d22c -r c28da0820b8b src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Tue Mar 05 07:00:21 2019 +0000
+++ b/src/Pure/General/rdf.scala	Tue Mar 05 14:45:27 2019 +0100
@@ -38,7 +38,11 @@
 
   def triples(args: List[Triple]): XML.Body =
     args.groupBy(_.subject).toList.map(
-      { case (subject, ts) => description(subject, ts.map(_.property)) })
+      { case (subject, ts) =>
+          val nl = XML.Text("\n")
+          val body = nl :: ts.flatMap(t => List(t.property, nl))
+          description(subject, body)
+      })
 
   def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
     XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)
diff -r 62e47f06d22c -r c28da0820b8b src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Tue Mar 05 07:00:21 2019 +0000
+++ b/src/Pure/PIDE/document_status.scala	Tue Mar 05 14:45:27 2019 +0100
@@ -179,22 +179,22 @@
   }
 
 
-  /* node timing */
+  /* overall timing */
 
-  object Node_Timing
+  object Overall_Timing
   {
-    val empty: Node_Timing = Node_Timing(0.0, Map.empty)
+    val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
 
     def make(
       state: Document.State,
       version: Document.Version,
-      node: Document.Node,
-      threshold: Double): Node_Timing =
+      commands: Iterable[Command],
+      threshold: Double = 0.0): Overall_Timing =
     {
       var total = 0.0
-      var commands = Map.empty[Command, Double]
+      var command_timings = Map.empty[Command, Double]
       for {
-        command <- node.commands.iterator
+        command <- commands.iterator
         st <- state.command_states(version, command)
       } {
         val command_timing =
@@ -203,13 +203,19 @@
             case (timing, _) => timing
           })
         total += command_timing
-        if (command_timing >= threshold) commands += (command -> command_timing)
+        if (command_timing > 0.0 && command_timing >= threshold) {
+          command_timings += (command -> command_timing)
+        }
       }
-      Node_Timing(total, commands)
+      Overall_Timing(total, command_timings)
     }
   }
 
-  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
+  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
+  {
+    def command_timing(command: Command): Double =
+      command_timings.getOrElse(command, 0.0)
+  }
 
 
   /* nodes status */
diff -r 62e47f06d22c -r c28da0820b8b src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 07:00:21 2019 +0000
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 14:45:27 2019 +0100
@@ -150,7 +150,7 @@
 
   /* component state -- owned by GUI thread */
 
-  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing]
+  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
 
   private def make_entries(): List[Entry] =
   {
@@ -161,13 +161,13 @@
         case None => Document.Node.Name.empty
         case Some(doc_view) => doc_view.model.node_name
       }
-    val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty)
+    val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
 
     val theories =
-      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
+      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
         yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
     val commands =
-      (for ((command, command_timing) <- timing.commands.toList)
+      (for ((command, command_timing) <- timing.command_timings.toList)
         yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
 
     theories.flatMap(entry =>
@@ -191,8 +191,8 @@
           if (PIDE.resources.session_base.loaded_theory(name)) timing1
           else {
             val node_timing =
-              Document_Status.Node_Timing.make(
-                snapshot.state, snapshot.version, node, timing_threshold)
+              Document_Status.Overall_Timing.make(
+                snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
             timing1 + (name -> node_timing)
           }
       })