# HG changeset patch
# User wenzelm
# Date 1491324238 -7200
# Node ID ce09e947c1d50e490e1e417287ccdfd77761d678
# Parent  1324268c2f6ae72e53213c5a8a3c40807c20ccfb
tuned signature;

diff -r 1324268c2f6a -r ce09e947c1d5 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Tue Apr 04 18:43:47 2017 +0200
+++ b/src/Pure/General/linear_set.scala	Tue Apr 04 18:43:58 2017 +0200
@@ -78,7 +78,7 @@
             }
       }
 
-  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =  // FIXME reverse fold
+  def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] =  // FIXME reverse fold
     ((hook, this) /: elems) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
diff -r 1324268c2f6a -r ce09e947c1d5 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Apr 04 18:43:47 2017 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 04 18:43:58 2017 +0200
@@ -82,7 +82,7 @@
 
     def full: Perspective = Perspective(List(Range.full))
 
-    def apply(ranges: Seq[Range]): Perspective =
+    def apply(ranges: List[Range]): Perspective =
     {
       val result = new mutable.ListBuffer[Range]
       var last: Option[Range] = None
diff -r 1324268c2f6a -r ce09e947c1d5 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 04 18:43:47 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 18:43:58 2017 +0200
@@ -177,7 +177,7 @@
 
   object Tree
   {
-    def apply(infos: Seq[(String, Info)]): Tree =
+    def apply(infos: Traversable[(String, Info)]): Tree =
     {
       val graph1 =
         (Graph.string[Info] /: infos) {