src/Pure/library.scala

--- a/src/Pure/library.scala	Wed Nov 10 20:21:55 2010 +0100
+++ b/src/Pure/library.scala	Wed Nov 10 20:43:22 2010 +0100
@@ -82,6 +82,13 @@
       }
   }
 
+  def first_line(source: CharSequence): String =
+  {
+    val lines = chunks(source)
+    if (lines.hasNext) lines.next.toString
+    else ""
+  }
+
 
   /* simple dialogs */