immediate theory progress for build_dialog;
authorwenzelm
Sat Jan 12 15:00:48 2013 +0100 (2013-01-12 ago)
changeset 50845477ca927676f
parent 50844 b95ff3744815
child 50846 529e652d389d
immediate theory progress for build_dialog;
more formal Bash_Result -- accumulate output as lines;
src/Pure/General/file.scala
src/Pure/PIDE/markup.ML
src/Pure/System/isabelle_system.scala
src/Pure/System/system_channel.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/build_dialog.scala
src/Pure/library.scala
     1.1 --- a/src/Pure/General/file.scala	Sat Jan 12 14:56:57 2013 +0100
     1.2 +++ b/src/Pure/General/file.scala	Sat Jan 12 15:00:48 2013 +0100
     1.3 @@ -75,6 +75,21 @@
     1.4    def read_gzip(path: Path): String = read_gzip(path.file)
     1.5  
     1.6  
     1.7 +  /* read lines */
     1.8 +
     1.9 +  def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
    1.10 +  {
    1.11 +    val result = new mutable.ListBuffer[String]
    1.12 +    var line: String = null
    1.13 +    while ({ line = reader.readLine; line != null }) {
    1.14 +      progress(line)
    1.15 +      result += line
    1.16 +    }
    1.17 +    reader.close
    1.18 +    result.toList
    1.19 +  }
    1.20 +
    1.21 +
    1.22    /* try_read */
    1.23  
    1.24    def try_read(paths: Seq[Path]): String =
     2.1 --- a/src/Pure/PIDE/markup.ML	Sat Jan 12 14:56:57 2013 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Sat Jan 12 15:00:48 2013 +0100
     2.3 @@ -133,6 +133,8 @@
     2.4    val invoke_scala: string -> string -> Properties.T
     2.5    val cancel_scala: string -> Properties.T
     2.6    val ML_statistics: Properties.entry
     2.7 +  val loading_theory: string -> Properties.T
     2.8 +  val dest_loading_theory: Properties.T -> string option
     2.9    val no_output: Output.output * Output.output
    2.10    val default_output: T -> Output.output * Output.output
    2.11    val add_mode: string -> (T -> Output.output * Output.output) -> unit
    2.12 @@ -408,6 +410,11 @@
    2.13  
    2.14  val ML_statistics = (functionN, "ML_statistics");
    2.15  
    2.16 +fun loading_theory name = [("function", "loading_theory"), ("name", name)];
    2.17 +
    2.18 +fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
    2.19 +  | dest_loading_theory _ = NONE;
    2.20 +
    2.21  
    2.22  
    2.23  (** print mode operations **)
     3.1 --- a/src/Pure/System/isabelle_system.scala	Sat Jan 12 14:56:57 2013 +0100
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Jan 12 15:00:48 2013 +0100
     3.3 @@ -16,7 +16,6 @@
     3.4  
     3.5  import scala.io.Source
     3.6  import scala.util.matching.Regex
     3.7 -import scala.collection.mutable
     3.8  
     3.9  
    3.10  object Isabelle_System
    3.11 @@ -331,24 +330,35 @@
    3.12  
    3.13    /* bash */
    3.14  
    3.15 -  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
    3.16 +  final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
    3.17 +  {
    3.18 +    def out: String = cat_lines(out_lines)
    3.19 +    def err: String = cat_lines(err_lines)
    3.20 +    def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
    3.21 +  }
    3.22 +
    3.23 +  def bash_env(cwd: JFile, env: Map[String, String], script: String,
    3.24 +    out_progress: String => Unit = (_: String) => (),
    3.25 +    err_progress: String => Unit = (_: String) => ()): Bash_Result =
    3.26    {
    3.27      File.with_tmp_file("isabelle_script") { script_file =>
    3.28        File.write(script_file, script)
    3.29        val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
    3.30  
    3.31        proc.stdin.close
    3.32 -      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }
    3.33 -      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read_stream(proc.stderr) }
    3.34 +      val (_, stdout) =
    3.35 +        Simple_Thread.future("bash_stdout") { File.read_lines(proc.stdout, out_progress) }
    3.36 +      val (_, stderr) =
    3.37 +        Simple_Thread.future("bash_stderr") { File.read_lines(proc.stderr, err_progress) }
    3.38  
    3.39        val rc =
    3.40          try { proc.join }
    3.41          catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
    3.42 -      (stdout.join, stderr.join, rc)
    3.43 +      Bash_Result(stdout.join, stderr.join, rc)
    3.44      }
    3.45    }
    3.46  
    3.47 -  def bash(script: String): (String, String, Int) = bash_env(null, null, script)
    3.48 +  def bash(script: String): Bash_Result = bash_env(null, null, script)
    3.49  
    3.50  
    3.51    /* system tools */
     4.1 --- a/src/Pure/System/system_channel.scala	Sat Jan 12 14:56:57 2013 +0100
     4.2 +++ b/src/Pure/System/system_channel.scala	Sat Jan 12 15:00:48 2013 +0100
     4.3 @@ -45,8 +45,8 @@
     4.4        "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
     4.5        "echo -n \"$FIFO\"\n" +
     4.6        "mkfifo -m 600 \"$FIFO\"\n"
     4.7 -    val (out, err, rc) = Isabelle_System.bash(script)
     4.8 -    if (rc == 0) out else error(err.trim)
     4.9 +    val result = Isabelle_System.bash(script)
    4.10 +    if (result.rc == 0) result.out else error(result.err)
    4.11    }
    4.12  
    4.13    private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete
     5.1 --- a/src/Pure/Thy/thy_info.ML	Sat Jan 12 14:56:57 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Jan 12 15:00:48 2013 +0100
     5.3 @@ -224,6 +224,7 @@
     5.4    let
     5.5      val _ = kill_thy name;
     5.6      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
     5.7 +    val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => ();
     5.8  
     5.9      val {master = (thy_path, _), imports} = deps;
    5.10      val dir = Path.dir thy_path;
     6.1 --- a/src/Pure/Tools/build.ML	Sat Jan 12 14:56:57 2013 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Sat Jan 12 15:00:48 2013 +0100
     6.3 @@ -22,7 +22,10 @@
     6.4  fun protocol_message props output =
     6.5    (case ML_statistics props output of
     6.6      SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
     6.7 -  | NONE => raise Fail "Undefined Output.protocol_message");
     6.8 +  | NONE =>
     6.9 +      (case Markup.dest_loading_theory props of
    6.10 +        SOME name => writeln ("\floading_theory = " ^ name)
    6.11 +      | NONE => raise Fail "Undefined Output.protocol_message"));
    6.12  
    6.13  
    6.14  (* build *)
     7.1 --- a/src/Pure/Tools/build.scala	Sat Jan 12 14:56:57 2013 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Sat Jan 12 15:00:48 2013 +0100
     7.3 @@ -22,6 +22,7 @@
     7.4    /** progress context **/
     7.5  
     7.6    class Progress {
     7.7 +    def theory(name: String) {}
     7.8      def echo(msg: String) {}
     7.9      def stopped: Boolean = false
    7.10    }
    7.11 @@ -412,7 +413,8 @@
    7.12  
    7.13    /* jobs */
    7.14  
    7.15 -  private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
    7.16 +  private class Job(progress: Build.Progress,
    7.17 +    name: String, val info: Session_Info, output: Path, do_output: Boolean,
    7.18      verbose: Boolean, browser_info: Path)
    7.19    {
    7.20      // global browser info dir
    7.21 @@ -479,7 +481,12 @@
    7.22        }
    7.23  
    7.24      private val (thread, result) =
    7.25 -      Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
    7.26 +      Simple_Thread.future("build") {
    7.27 +        Isabelle_System.bash_env(info.dir.file, env, script,
    7.28 +          out_progress = (line: String) =>
    7.29 +            if (line.startsWith(LOADING_THEORY))
    7.30 +              progress.theory(line.substring(LOADING_THEORY.length)))
    7.31 +      }
    7.32  
    7.33      def terminate: Unit = thread.interrupt
    7.34      def is_finished: Boolean = result.is_finished
    7.35 @@ -494,17 +501,16 @@
    7.36        }
    7.37        else None
    7.38  
    7.39 -    def join: (String, String, Int) = {
    7.40 -      val (out, err, rc) = result.join
    7.41 +    def join: Isabelle_System.Bash_Result =
    7.42 +    {
    7.43 +      val res = result.join
    7.44 +
    7.45        args_file.delete
    7.46        timer.map(_.cancel())
    7.47  
    7.48 -      val err1 =
    7.49 -        if (rc == 130)
    7.50 -          (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
    7.51 -          (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
    7.52 -        else err
    7.53 -      (out, err1, rc)
    7.54 +      if (res.rc == 130)
    7.55 +        res.add_err(if (timeout) "*** Timeout" else "*** Interrupt")
    7.56 +      else res
    7.57      }
    7.58    }
    7.59  
    7.60 @@ -516,6 +522,7 @@
    7.61    private def log_gz(name: String): Path = log(name).ext("gz")
    7.62  
    7.63    private val SESSION_PARENT_PATH = "\fSession.parent_path = "
    7.64 +  private val LOADING_THEORY = "\floading_theory = "
    7.65  
    7.66    sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
    7.67  
    7.68 @@ -634,22 +641,21 @@
    7.69            case Some((name, (parent_heap, job))) =>
    7.70              //{{{ finish job
    7.71  
    7.72 -            val (out, err, rc) = job.join
    7.73 -            val out_lines = split_lines(out)
    7.74 -            progress.echo(Library.trim_line(err))
    7.75 +            val res = job.join
    7.76 +            progress.echo(res.err)
    7.77  
    7.78              val (parent_path, heap) =
    7.79 -              if (rc == 0) {
    7.80 +              if (res.rc == 0) {
    7.81                  (output_dir + log(name)).file.delete
    7.82  
    7.83                  val sources = make_stamp(name)
    7.84                  val heap = heap_stamp(job.output_path)
    7.85                  File.write_gzip(output_dir + log_gz(name),
    7.86 -                  sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
    7.87 +                  sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
    7.88  
    7.89                  val parent_path =
    7.90                    if (job.info.options.bool("browser_info"))
    7.91 -                    out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
    7.92 +                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
    7.93                        line.substring(SESSION_PARENT_PATH.length))
    7.94                    else None
    7.95  
    7.96 @@ -659,11 +665,11 @@
    7.97                  (output_dir + Path.basic(name)).file.delete
    7.98                  (output_dir + log_gz(name)).file.delete
    7.99  
   7.100 -                File.write(output_dir + log(name), out)
   7.101 +                File.write(output_dir + log(name), res.out)
   7.102                  progress.echo(name + " FAILED")
   7.103 -                if (rc != 130) {
   7.104 +                if (res.rc != 130) {
   7.105                    progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
   7.106 -                  val lines = out_lines.filterNot(_.startsWith("\f"))
   7.107 +                  val lines = res.out_lines.filterNot(_.startsWith("\f"))
   7.108                    val tail = lines.drop(lines.length - 20 max 0)
   7.109                    progress.echo("\n" + cat_lines(tail))
   7.110                  }
   7.111 @@ -671,7 +677,7 @@
   7.112                  (None, no_heap)
   7.113                }
   7.114              loop(pending - name, running - name,
   7.115 -              results + (name -> Result(false, parent_path, heap, rc)))
   7.116 +              results + (name -> Result(false, parent_path, heap, res.rc)))
   7.117              //}}}
   7.118            case None if (running.size < (max_jobs max 1)) =>
   7.119              //{{{ check/start next job
   7.120 @@ -709,7 +715,7 @@
   7.121                  }
   7.122                  else if (parent_result.rc == 0) {
   7.123                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   7.124 -                  val job = new Job(name, info, output, do_output, verbose, browser_info)
   7.125 +                  val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
   7.126                    loop(pending, running + (name -> (parent_result.heap, job)), results)
   7.127                  }
   7.128                  else {
     8.1 --- a/src/Pure/Tools/build_dialog.scala	Sat Jan 12 14:56:57 2013 +0100
     8.2 +++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 12 15:00:48 2013 +0100
     8.3 @@ -83,6 +83,7 @@
     8.4  
     8.5      val progress = new Build.Progress
     8.6      {
     8.7 +      override def theory(name: String): Unit = echo("  theory " + name)
     8.8        override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
     8.9        override def stopped: Boolean =
    8.10          Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }
     9.1 --- a/src/Pure/library.scala	Sat Jan 12 14:56:57 2013 +0100
     9.2 +++ b/src/Pure/library.scala	Sat Jan 12 15:00:48 2013 +0100
     9.3 @@ -82,10 +82,6 @@
     9.4      else ""
     9.5    }
     9.6  
     9.7 -  def trim_line(str: String): String =
     9.8 -    if (str.endsWith("\n")) str.substring(0, str.length - 1)
     9.9 -    else str
    9.10 -
    9.11    def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
    9.12    def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
    9.13