--- 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)
--- 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 */
--- 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)
}
})