# HG changeset patch # User wenzelm # Date 1357999248 -3600 # Node ID 477ca927676f8a79ad0b4d3d3becd5596d9ded92 # Parent b95ff374481529985e45b79f47ac3f2f7bc5b867 immediate theory progress for build_dialog; more formal Bash_Result -- accumulate output as lines; diff -r b95ff3744815 -r 477ca927676f src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/General/file.scala Sat Jan 12 15:00:48 2013 +0100 @@ -75,6 +75,21 @@ def read_gzip(path: Path): String = read_gzip(path.file) + /* read lines */ + + def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = + { + val result = new mutable.ListBuffer[String] + var line: String = null + while ({ line = reader.readLine; line != null }) { + progress(line) + result += line + } + reader.close + result.toList + } + + /* try_read */ def try_read(paths: Seq[Path]): String = diff -r b95ff3744815 -r 477ca927676f src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Jan 12 15:00:48 2013 +0100 @@ -133,6 +133,8 @@ val invoke_scala: string -> string -> Properties.T val cancel_scala: string -> Properties.T val ML_statistics: Properties.entry + val loading_theory: string -> Properties.T + val dest_loading_theory: Properties.T -> string option val no_output: Output.output * Output.output val default_output: T -> Output.output * Output.output val add_mode: string -> (T -> Output.output * Output.output) -> unit @@ -408,6 +410,11 @@ val ML_statistics = (functionN, "ML_statistics"); +fun loading_theory name = [("function", "loading_theory"), ("name", name)]; + +fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name + | dest_loading_theory _ = NONE; + (** print mode operations **) diff -r b95ff3744815 -r 477ca927676f src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/System/isabelle_system.scala Sat Jan 12 15:00:48 2013 +0100 @@ -16,7 +16,6 @@ import scala.io.Source import scala.util.matching.Regex -import scala.collection.mutable object Isabelle_System @@ -331,24 +330,35 @@ /* bash */ - def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) = + final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int) + { + def out: String = cat_lines(out_lines) + def err: String = cat_lines(err_lines) + def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s)) + } + + def bash_env(cwd: JFile, env: Map[String, String], script: String, + out_progress: String => Unit = (_: String) => (), + err_progress: String => Unit = (_: String) => ()): Bash_Result = { File.with_tmp_file("isabelle_script") { script_file => File.write(script_file, script) val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file)) proc.stdin.close - val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) } - val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read_stream(proc.stderr) } + val (_, stdout) = + Simple_Thread.future("bash_stdout") { File.read_lines(proc.stdout, out_progress) } + val (_, stderr) = + Simple_Thread.future("bash_stderr") { File.read_lines(proc.stderr, err_progress) } val rc = try { proc.join } catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 } - (stdout.join, stderr.join, rc) + Bash_Result(stdout.join, stderr.join, rc) } } - def bash(script: String): (String, String, Int) = bash_env(null, null, script) + def bash(script: String): Bash_Result = bash_env(null, null, script) /* system tools */ diff -r b95ff3744815 -r 477ca927676f src/Pure/System/system_channel.scala --- a/src/Pure/System/system_channel.scala Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/System/system_channel.scala Sat Jan 12 15:00:48 2013 +0100 @@ -45,8 +45,8 @@ "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" + "echo -n \"$FIFO\"\n" + "mkfifo -m 600 \"$FIFO\"\n" - val (out, err, rc) = Isabelle_System.bash(script) - if (rc == 0) out else error(err.trim) + val result = Isabelle_System.bash(script) + if (result.rc == 0) result.out else error(result.err) } private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete diff -r b95ff3744815 -r 477ca927676f src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Jan 12 15:00:48 2013 +0100 @@ -224,6 +224,7 @@ let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); + val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => (); val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; diff -r b95ff3744815 -r 477ca927676f src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/Tools/build.ML Sat Jan 12 15:00:48 2013 +0100 @@ -22,7 +22,10 @@ fun protocol_message props output = (case ML_statistics props output of SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats) - | NONE => raise Fail "Undefined Output.protocol_message"); + | NONE => + (case Markup.dest_loading_theory props of + SOME name => writeln ("\floading_theory = " ^ name) + | NONE => raise Fail "Undefined Output.protocol_message")); (* build *) diff -r b95ff3744815 -r 477ca927676f src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/Tools/build.scala Sat Jan 12 15:00:48 2013 +0100 @@ -22,6 +22,7 @@ /** progress context **/ class Progress { + def theory(name: String) {} def echo(msg: String) {} def stopped: Boolean = false } @@ -412,7 +413,8 @@ /* jobs */ - private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean, + private class Job(progress: Build.Progress, + name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean, browser_info: Path) { // global browser info dir @@ -479,7 +481,12 @@ } private val (thread, result) = - Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) } + Simple_Thread.future("build") { + Isabelle_System.bash_env(info.dir.file, env, script, + out_progress = (line: String) => + if (line.startsWith(LOADING_THEORY)) + progress.theory(line.substring(LOADING_THEORY.length))) + } def terminate: Unit = thread.interrupt def is_finished: Boolean = result.is_finished @@ -494,17 +501,16 @@ } else None - def join: (String, String, Int) = { - val (out, err, rc) = result.join + def join: Isabelle_System.Bash_Result = + { + val res = result.join + args_file.delete timer.map(_.cancel()) - val err1 = - if (rc == 130) - (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") + - (if (timeout) "*** Timeout\n" else "*** Interrupt\n") - else err - (out, err1, rc) + if (res.rc == 130) + res.add_err(if (timeout) "*** Timeout" else "*** Interrupt") + else res } } @@ -516,6 +522,7 @@ 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) @@ -634,22 +641,21 @@ case Some((name, (parent_heap, job))) => //{{{ finish job - val (out, err, rc) = job.join - val out_lines = split_lines(out) - progress.echo(Library.trim_line(err)) + val res = job.join + progress.echo(res.err) val (parent_path, heap) = - if (rc == 0) { + if (res.rc == 0) { (output_dir + log(name)).file.delete val sources = make_stamp(name) val heap = heap_stamp(job.output_path) File.write_gzip(output_dir + log_gz(name), - sources + "\n" + parent_heap + "\n" + heap + "\n" + out) + sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out) val parent_path = if (job.info.options.bool("browser_info")) - out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line => + res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line => line.substring(SESSION_PARENT_PATH.length)) else None @@ -659,11 +665,11 @@ (output_dir + Path.basic(name)).file.delete (output_dir + log_gz(name)).file.delete - File.write(output_dir + log(name), out) + File.write(output_dir + log(name), res.out) progress.echo(name + " FAILED") - if (rc != 130) { + if (res.rc != 130) { progress.echo("(see also " + (output_dir + log(name)).file.toString + ")") - val lines = out_lines.filterNot(_.startsWith("\f")) + val lines = res.out_lines.filterNot(_.startsWith("\f")) val tail = lines.drop(lines.length - 20 max 0) progress.echo("\n" + cat_lines(tail)) } @@ -671,7 +677,7 @@ (None, no_heap) } loop(pending - name, running - name, - results + (name -> Result(false, parent_path, heap, rc))) + results + (name -> Result(false, parent_path, heap, res.rc))) //}}} case None if (running.size < (max_jobs max 1)) => //{{{ check/start next job @@ -709,7 +715,7 @@ } else if (parent_result.rc == 0) { progress.echo((if (do_output) "Building " else "Running ") + name + " ...") - val job = new Job(name, info, output, do_output, verbose, browser_info) + val job = new Job(progress, name, info, output, do_output, verbose, browser_info) loop(pending, running + (name -> (parent_result.heap, job)), results) } else { diff -r b95ff3744815 -r 477ca927676f src/Pure/Tools/build_dialog.scala --- a/src/Pure/Tools/build_dialog.scala Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/Tools/build_dialog.scala Sat Jan 12 15:00:48 2013 +0100 @@ -83,6 +83,7 @@ val progress = new Build.Progress { + override def theory(name: String): Unit = echo(" theory " + name) override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") } override def stopped: Boolean = Swing_Thread.now { val b = is_stopped; is_stopped = false; b } diff -r b95ff3744815 -r 477ca927676f src/Pure/library.scala --- a/src/Pure/library.scala Sat Jan 12 14:56:57 2013 +0100 +++ b/src/Pure/library.scala Sat Jan 12 15:00:48 2013 +0100 @@ -82,10 +82,6 @@ else "" } - def trim_line(str: String): String = - if (str.endsWith("\n")) str.substring(0, str.length - 1) - else str - def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH) def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)