# 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)