# HG changeset patch # User wenzelm # Date 1358005418 -3600 # Node ID 529e652d389dea840c23dbfa8754eb17792afd8d # Parent 477ca927676f8a79ad0b4d3d3becd5596d9ded92 more uniform theory progress in build -v and build_dialog; diff -r 477ca927676f -r 529e652d389d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Jan 12 15:00:48 2013 +0100 +++ b/src/Pure/Tools/build.scala Sat Jan 12 16:43:38 2013 +0100 @@ -21,16 +21,20 @@ { /** progress context **/ - class Progress { - def theory(name: String) {} + class Progress + { def echo(msg: String) {} + def theory(session: String, theory: String) {} def stopped: Boolean = false } object Ignore_Progress extends Progress - object Console_Progress extends Progress { + class Console_Progress(verbose: Boolean) extends Progress + { override def echo(msg: String) { java.lang.System.out.println(msg) } + override def theory(session: String, theory: String): Unit = + if (verbose) echo(session + ": theory " + theory) } @@ -485,7 +489,7 @@ 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))) + progress.theory(name, line.substring(LOADING_THEORY.length))) } def terminate: Unit = thread.interrupt @@ -775,9 +779,9 @@ val dirs = select_dirs.map(d => (true, Path.explode(d))) ::: include_dirs.map(d => (false, Path.explode(d))) - build(Build.Console_Progress, options, requirements, all_sessions, build_heap, - clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode, - verbose, sessions) + build(new Build.Console_Progress(verbose), options, requirements, all_sessions, + build_heap, clean_build, dirs, session_groups, max_jobs, list_files, no_build, + system_mode, verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } } diff -r 477ca927676f -r 529e652d389d src/Pure/Tools/build_dialog.scala --- a/src/Pure/Tools/build_dialog.scala Sat Jan 12 15:00:48 2013 +0100 +++ b/src/Pure/Tools/build_dialog.scala Sat Jan 12 16:43:38 2013 +0100 @@ -83,8 +83,10 @@ 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 echo(msg: String): Unit = + Swing_Thread.later { text.append(msg + "\n") } + override def theory(session: String, theory: String): Unit = + echo(session + ": theory " + theory) override def stopped: Boolean = Swing_Thread.now { val b = is_stopped; is_stopped = false; b } }