clarified signature;
authorwenzelm
Tue Mar 05 13:31:33 2019 +0100 (7 weeks ago ago)
changeset 70045d594997cdcf4
parent 70044 9532d5b2e932
child 70046 c28da0820b8b
clarified signature;
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 13:11:01 2019 +0100
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Tue Mar 05 13:31:33 2019 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4        state: Document.State,
     1.5        version: Document.Version,
     1.6        commands: Iterable[Command],
     1.7 -      threshold: Double): Overall_Timing =
     1.8 +      threshold: Double = 0.0): Overall_Timing =
     1.9      {
    1.10        var total = 0.0
    1.11        var command_timings = Map.empty[Command, Double]
    1.12 @@ -203,13 +203,19 @@
    1.13              case (timing, _) => timing
    1.14            })
    1.15          total += command_timing
    1.16 -        if (command_timing >= threshold) command_timings += (command -> command_timing)
    1.17 +        if (command_timing > 0.0 && command_timing >= threshold) {
    1.18 +          command_timings += (command -> command_timing)
    1.19 +        }
    1.20        }
    1.21        Overall_Timing(total, command_timings)
    1.22      }
    1.23    }
    1.24  
    1.25    sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
    1.26 +  {
    1.27 +    def command_timing(command: Command): Double =
    1.28 +      command_timings.getOrElse(command, 0.0)
    1.29 +  }
    1.30  
    1.31  
    1.32    /* nodes status */
     2.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 13:11:01 2019 +0100
     2.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 13:31:33 2019 +0100
     2.3 @@ -192,7 +192,7 @@
     2.4            else {
     2.5              val node_timing =
     2.6                Document_Status.Overall_Timing.make(
     2.7 -                snapshot.state, snapshot.version, node.commands, timing_threshold)
     2.8 +                snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
     2.9              timing1 + (name -> node_timing)
    2.10            }
    2.11        })