tuned signature;
authorwenzelm
Sat Jan 12 17:28:07 2013 +0100 (2013-01-12)
changeset 5084778c40f1cc9b3
parent 50846 529e652d389d
child 50848 4e123d57c9b4
tuned signature;
src/Pure/General/properties.scala
src/Pure/Tools/build.scala
src/Pure/library.scala
     1.1 --- a/src/Pure/General/properties.scala	Sat Jan 12 16:43:38 2013 +0100
     1.2 +++ b/src/Pure/General/properties.scala	Sat Jan 12 17:28:07 2013 +0100
     1.3 @@ -126,8 +126,7 @@
     1.4    }
     1.5  
     1.6    def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] =
     1.7 -    for (line <- lines if line.startsWith(prefix))
     1.8 -      yield parse(line.substring(prefix.length))
     1.9 +    for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    1.10  
    1.11    def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] =
    1.12      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
     2.1 --- a/src/Pure/Tools/build.scala	Sat Jan 12 16:43:38 2013 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Sat Jan 12 17:28:07 2013 +0100
     2.3 @@ -488,8 +488,10 @@
     2.4        Simple_Thread.future("build") {
     2.5          Isabelle_System.bash_env(info.dir.file, env, script,
     2.6            out_progress = (line: String) =>
     2.7 -            if (line.startsWith(LOADING_THEORY))
     2.8 -              progress.theory(name, line.substring(LOADING_THEORY.length)))
     2.9 +            Library.try_unprefix("\floading_theory = ", line) match {
    2.10 +              case Some(theory) => progress.theory(name, theory)
    2.11 +              case None =>
    2.12 +            })
    2.13        }
    2.14  
    2.15      def terminate: Unit = thread.interrupt
    2.16 @@ -526,7 +528,6 @@
    2.17    private def log_gz(name: String): Path = log(name).ext("gz")
    2.18  
    2.19    private val SESSION_PARENT_PATH = "\fSession.parent_path = "
    2.20 -  private val LOADING_THEORY = "\floading_theory = "
    2.21  
    2.22    sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
    2.23  
     3.1 --- a/src/Pure/library.scala	Sat Jan 12 16:43:38 2013 +0100
     3.2 +++ b/src/Pure/library.scala	Sat Jan 12 17:28:07 2013 +0100
     3.3 @@ -82,6 +82,9 @@
     3.4      else ""
     3.5    }
     3.6  
     3.7 +
     3.8 +  /* strings */
     3.9 +
    3.10    def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
    3.11    def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
    3.12  
    3.13 @@ -89,6 +92,9 @@
    3.14      if (str.length == 0) str
    3.15      else uppercase(str.substring(0, 1)) + str.substring(1)
    3.16  
    3.17 +  def try_unprefix(prfx: String, s: String): Option[String] =
    3.18 +    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
    3.19 +
    3.20  
    3.21    /* quote */
    3.22