src/Pure/General/graph.scala
changeset 46667 318b669fe660
parent 46666 b01b6977a5e8
child 46668 9034b44844bd
--- a/src/Pure/General/graph.scala	Sat Feb 25 13:00:32 2012 +0100
+++ b/src/Pure/General/graph.scala	Sat Feb 25 13:13:14 2012 +0100
@@ -20,6 +20,10 @@
 
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
+
+  def string[A]: Graph[String, A] = empty(Ordering.String)
+  def int[A]: Graph[Int, A] = empty(Ordering.Int)
+  def long[A]: Graph[Long, A] = empty(Ordering.Long)
 }