# HG changeset patch # User wenzelm # Date 1375869014 -7200 # Node ID 671421cef59003bb225fdcfcb5272d04a494f59e # Parent 98eac7b7eec3d996d635c1129654f448ad3e6b2f tuned; diff -r 98eac7b7eec3 -r 671421cef590 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Aug 07 11:44:17 2013 +0200 +++ b/src/Pure/General/symbol.scala Wed Aug 07 11:50:14 2013 +0200 @@ -193,7 +193,7 @@ if (min <= c && c <= max) { matcher.region(i, len).lookingAt val x = matcher.group - result.append(table.get(x) getOrElse x) + result.append(table.getOrElse(x, x)) i = matcher.end } else { result.append(c); i += 1 } @@ -255,7 +255,7 @@ } val groups: List[(String, List[Symbol])] = - symbols.map({ case (sym, props) => (sym, props.get("group") getOrElse "unsorted") }) + symbols.map({ case (sym, props) => (sym, props.getOrElse("group", "unsorted")) }) .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) }) .sortBy(_._1) diff -r 98eac7b7eec3 -r 671421cef590 src/Pure/Tools/ml_statistics.scala --- a/src/Pure/Tools/ml_statistics.scala Wed Aug 07 11:44:17 2013 +0200 +++ b/src/Pure/Tools/ml_statistics.scala Wed Aug 07 11:50:14 2013 +0200 @@ -85,7 +85,7 @@ // rising edges -- relative speed val speeds = for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield { - val (x0, y0, s0) = last_edge.get(a) getOrElse (0.0, 0.0, 0.0) + val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0)) val x1 = time val y1 = java.lang.Double.parseDouble(value) diff -r 98eac7b7eec3 -r 671421cef590 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Wed Aug 07 11:44:17 2013 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Aug 07 11:50:14 2013 +0200 @@ -167,7 +167,7 @@ case None => Document.Node.Name.empty case Some(doc_view) => doc_view.model.name } - val timing = nodes_timing.get(name) getOrElse Protocol.empty_node_timing + val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing) val theories = (for ((node_name, node_timing) <- nodes_timing.toList if !node_timing.commands.isEmpty)