clarified signature: more general types;
authorwenzelm
Tue Mar 05 13:11:01 2019 +0100 (3 months ago ago)
changeset 700449532d5b2e932
parent 70043 db622ada496d
child 70045 d594997cdcf4
clarified signature: more general types;
src/Pure/PIDE/document_status.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/PIDE/document_status.scala	Tue Mar 05 11:52:20 2019 +0100
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Tue Mar 05 13:11:01 2019 +0100
     1.3 @@ -179,22 +179,22 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* node timing */
     1.8 +  /* overall timing */
     1.9  
    1.10 -  object Node_Timing
    1.11 +  object Overall_Timing
    1.12    {
    1.13 -    val empty: Node_Timing = Node_Timing(0.0, Map.empty)
    1.14 +    val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
    1.15  
    1.16      def make(
    1.17        state: Document.State,
    1.18        version: Document.Version,
    1.19 -      node: Document.Node,
    1.20 -      threshold: Double): Node_Timing =
    1.21 +      commands: Iterable[Command],
    1.22 +      threshold: Double): Overall_Timing =
    1.23      {
    1.24        var total = 0.0
    1.25 -      var commands = Map.empty[Command, Double]
    1.26 +      var command_timings = Map.empty[Command, Double]
    1.27        for {
    1.28 -        command <- node.commands.iterator
    1.29 +        command <- commands.iterator
    1.30          st <- state.command_states(version, command)
    1.31        } {
    1.32          val command_timing =
    1.33 @@ -203,13 +203,13 @@
    1.34              case (timing, _) => timing
    1.35            })
    1.36          total += command_timing
    1.37 -        if (command_timing >= threshold) commands += (command -> command_timing)
    1.38 +        if (command_timing >= threshold) command_timings += (command -> command_timing)
    1.39        }
    1.40 -      Node_Timing(total, commands)
    1.41 +      Overall_Timing(total, command_timings)
    1.42      }
    1.43    }
    1.44  
    1.45 -  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
    1.46 +  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
    1.47  
    1.48  
    1.49    /* nodes status */
     2.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 11:52:20 2019 +0100
     2.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 13:11:01 2019 +0100
     2.3 @@ -150,7 +150,7 @@
     2.4  
     2.5    /* component state -- owned by GUI thread */
     2.6  
     2.7 -  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing]
     2.8 +  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
     2.9  
    2.10    private def make_entries(): List[Entry] =
    2.11    {
    2.12 @@ -161,13 +161,13 @@
    2.13          case None => Document.Node.Name.empty
    2.14          case Some(doc_view) => doc_view.model.node_name
    2.15        }
    2.16 -    val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty)
    2.17 +    val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
    2.18  
    2.19      val theories =
    2.20 -      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
    2.21 +      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
    2.22          yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
    2.23      val commands =
    2.24 -      (for ((command, command_timing) <- timing.commands.toList)
    2.25 +      (for ((command, command_timing) <- timing.command_timings.toList)
    2.26          yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
    2.27  
    2.28      theories.flatMap(entry =>
    2.29 @@ -191,8 +191,8 @@
    2.30            if (PIDE.resources.session_base.loaded_theory(name)) timing1
    2.31            else {
    2.32              val node_timing =
    2.33 -              Document_Status.Node_Timing.make(
    2.34 -                snapshot.state, snapshot.version, node, timing_threshold)
    2.35 +              Document_Status.Overall_Timing.make(
    2.36 +                snapshot.state, snapshot.version, node.commands, timing_threshold)
    2.37              timing1 + (name -> node_timing)
    2.38            }
    2.39        })