1.1 --- a/src/Pure/library.scala	Wed Nov 10 20:21:55 2010 +0100
     1.2 +++ b/src/Pure/library.scala	Wed Nov 10 20:43:22 2010 +0100
     1.3 @@ -82,6 +82,13 @@
     1.4        }
     1.5    }
     1.6  
     1.7 +  def first_line(source: CharSequence): String =
     1.8 +  {
     1.9 +    val lines = chunks(source)
    1.10 +    if (lines.hasNext) lines.next.toString
    1.11 +    else ""
    1.12 +  }
    1.13 +
    1.14  
    1.15    /* simple dialogs */
    1.16