tuned signature;
authorwenzelm
Tue Apr 04 18:43:58 2017 +0200 (2017-04-04 ago)
changeset 65374ce09e947c1d5
parent 65373 1324268c2f6a
child 65375 b722ee40c26c
tuned signature;
src/Pure/General/linear_set.scala
src/Pure/PIDE/text.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/General/linear_set.scala	Tue Apr 04 18:43:47 2017 +0200
     1.2 +++ b/src/Pure/General/linear_set.scala	Tue Apr 04 18:43:58 2017 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4              }
     1.5        }
     1.6  
     1.7 -  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =  // FIXME reverse fold
     1.8 +  def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] =  // FIXME reverse fold
     1.9      ((hook, this) /: elems) {
    1.10        case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
    1.11      }._2
     2.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 04 18:43:47 2017 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 04 18:43:58 2017 +0200
     2.3 @@ -82,7 +82,7 @@
     2.4  
     2.5      def full: Perspective = Perspective(List(Range.full))
     2.6  
     2.7 -    def apply(ranges: Seq[Range]): Perspective =
     2.8 +    def apply(ranges: List[Range]): Perspective =
     2.9      {
    2.10        val result = new mutable.ListBuffer[Range]
    2.11        var last: Option[Range] = None
     3.1 --- a/src/Pure/Thy/sessions.scala	Tue Apr 04 18:43:47 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 18:43:58 2017 +0200
     3.3 @@ -177,7 +177,7 @@
     3.4  
     3.5    object Tree
     3.6    {
     3.7 -    def apply(infos: Seq[(String, Info)]): Tree =
     3.8 +    def apply(infos: Traversable[(String, Info)]): Tree =
     3.9      {
    3.10        val graph1 =
    3.11          (Graph.string[Info] /: infos) {