merged
authorwenzelm
Tue Mar 05 14:45:27 2019 +0100 (3 months ago ago)
changeset 70046c28da0820b8b
parent 70042 62e47f06d22c
parent 70045 d594997cdcf4
child 70047 01732226987a
merged
     1.1 --- a/src/Pure/General/rdf.scala	Tue Mar 05 07:00:21 2019 +0000
     1.2 +++ b/src/Pure/General/rdf.scala	Tue Mar 05 14:45:27 2019 +0100
     1.3 @@ -38,7 +38,11 @@
     1.4  
     1.5    def triples(args: List[Triple]): XML.Body =
     1.6      args.groupBy(_.subject).toList.map(
     1.7 -      { case (subject, ts) => description(subject, ts.map(_.property)) })
     1.8 +      { case (subject, ts) =>
     1.9 +          val nl = XML.Text("\n")
    1.10 +          val body = nl :: ts.flatMap(t => List(t.property, nl))
    1.11 +          description(subject, body)
    1.12 +      })
    1.13  
    1.14    def description(subject: String, body: XML.Body, attributes: XML.Attributes = Nil): XML.Elem =
    1.15      XML.Elem(Markup(rdf("Description"), (rdf("about"), subject) :: attributes), body)
     2.1 --- a/src/Pure/PIDE/document_status.scala	Tue Mar 05 07:00:21 2019 +0000
     2.2 +++ b/src/Pure/PIDE/document_status.scala	Tue Mar 05 14:45:27 2019 +0100
     2.3 @@ -179,22 +179,22 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* node timing */
     2.8 +  /* overall timing */
     2.9  
    2.10 -  object Node_Timing
    2.11 +  object Overall_Timing
    2.12    {
    2.13 -    val empty: Node_Timing = Node_Timing(0.0, Map.empty)
    2.14 +    val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
    2.15  
    2.16      def make(
    2.17        state: Document.State,
    2.18        version: Document.Version,
    2.19 -      node: Document.Node,
    2.20 -      threshold: Double): Node_Timing =
    2.21 +      commands: Iterable[Command],
    2.22 +      threshold: Double = 0.0): Overall_Timing =
    2.23      {
    2.24        var total = 0.0
    2.25 -      var commands = Map.empty[Command, Double]
    2.26 +      var command_timings = Map.empty[Command, Double]
    2.27        for {
    2.28 -        command <- node.commands.iterator
    2.29 +        command <- commands.iterator
    2.30          st <- state.command_states(version, command)
    2.31        } {
    2.32          val command_timing =
    2.33 @@ -203,13 +203,19 @@
    2.34              case (timing, _) => timing
    2.35            })
    2.36          total += command_timing
    2.37 -        if (command_timing >= threshold) commands += (command -> command_timing)
    2.38 +        if (command_timing > 0.0 && command_timing >= threshold) {
    2.39 +          command_timings += (command -> command_timing)
    2.40 +        }
    2.41        }
    2.42 -      Node_Timing(total, commands)
    2.43 +      Overall_Timing(total, command_timings)
    2.44      }
    2.45    }
    2.46  
    2.47 -  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
    2.48 +  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
    2.49 +  {
    2.50 +    def command_timing(command: Command): Double =
    2.51 +      command_timings.getOrElse(command, 0.0)
    2.52 +  }
    2.53  
    2.54  
    2.55    /* nodes status */
     3.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 07:00:21 2019 +0000
     3.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 14:45:27 2019 +0100
     3.3 @@ -150,7 +150,7 @@
     3.4  
     3.5    /* component state -- owned by GUI thread */
     3.6  
     3.7 -  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing]
     3.8 +  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
     3.9  
    3.10    private def make_entries(): List[Entry] =
    3.11    {
    3.12 @@ -161,13 +161,13 @@
    3.13          case None => Document.Node.Name.empty
    3.14          case Some(doc_view) => doc_view.model.node_name
    3.15        }
    3.16 -    val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty)
    3.17 +    val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
    3.18  
    3.19      val theories =
    3.20 -      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
    3.21 +      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
    3.22          yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
    3.23      val commands =
    3.24 -      (for ((command, command_timing) <- timing.commands.toList)
    3.25 +      (for ((command, command_timing) <- timing.command_timings.toList)
    3.26          yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
    3.27  
    3.28      theories.flatMap(entry =>
    3.29 @@ -191,8 +191,8 @@
    3.30            if (PIDE.resources.session_base.loaded_theory(name)) timing1
    3.31            else {
    3.32              val node_timing =
    3.33 -              Document_Status.Node_Timing.make(
    3.34 -                snapshot.state, snapshot.version, node, timing_threshold)
    3.35 +              Document_Status.Overall_Timing.make(
    3.36 +                snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
    3.37              timing1 + (name -> node_timing)
    3.38            }
    3.39        })