more uniform theory progress in build -v and build_dialog;
authorwenzelm
Sat, 12 Jan 2013 16:43:38 +0100
changeset 50846 529e652d389d
parent 50845 477ca927676f
child 50847 78c40f1cc9b3
more uniform theory progress in build -v and build_dialog;
src/Pure/Tools/build.scala
src/Pure/Tools/build_dialog.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))
       }
     }
--- 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  }
     }