tuned signature;

--- a/src/Pure/General/properties.scala	Sat Jan 12 16:43:38 2013 +0100
+++ b/src/Pure/General/properties.scala	Sat Jan 12 17:28:07 2013 +0100
@@ -126,8 +126,7 @@
   }
 
   def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] =
-    for (line <- lines if line.startsWith(prefix))
-      yield parse(line.substring(prefix.length))
+    for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
 
   def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] =
     lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))

--- a/src/Pure/Tools/build.scala	Sat Jan 12 16:43:38 2013 +0100
+++ b/src/Pure/Tools/build.scala	Sat Jan 12 17:28:07 2013 +0100
@@ -488,8 +488,10 @@
       Simple_Thread.future("build") {
         Isabelle_System.bash_env(info.dir.file, env, script,
           out_progress = (line: String) =>
-            if (line.startsWith(LOADING_THEORY))
-              progress.theory(name, line.substring(LOADING_THEORY.length)))
+            Library.try_unprefix("\floading_theory = ", line) match {
+              case Some(theory) => progress.theory(name, theory)
+              case None =>
+            })
       }
 
     def terminate: Unit = thread.interrupt
@@ -526,7 +528,6 @@
   private def log_gz(name: String): Path = log(name).ext("gz")
 
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
-  private val LOADING_THEORY = "\floading_theory = "
 
   sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
 

--- a/src/Pure/library.scala	Sat Jan 12 16:43:38 2013 +0100
+++ b/src/Pure/library.scala	Sat Jan 12 17:28:07 2013 +0100
@@ -82,6 +82,9 @@
     else ""
   }
 
+
+  /* strings */
+
   def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
   def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
 
@@ -89,6 +92,9 @@
     if (str.length == 0) str
     else uppercase(str.substring(0, 1)) + str.substring(1)
 
+  def try_unprefix(prfx: String, s: String): Option[String] =
+    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
+
 
   /* quote */