more uniform theory progress in build -v and build_dialog;
authorwenzelm
Sat Jan 12 16:43:38 2013 +0100 (2013-01-12)
changeset 50846529e652d389d
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
     1.1 --- a/src/Pure/Tools/build.scala	Sat Jan 12 15:00:48 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Jan 12 16:43:38 2013 +0100
     1.3 @@ -21,16 +21,20 @@
     1.4  {
     1.5    /** progress context **/
     1.6  
     1.7 -  class Progress {
     1.8 -    def theory(name: String) {}
     1.9 +  class Progress
    1.10 +  {
    1.11      def echo(msg: String) {}
    1.12 +    def theory(session: String, theory: String) {}
    1.13      def stopped: Boolean = false
    1.14    }
    1.15  
    1.16    object Ignore_Progress extends Progress
    1.17  
    1.18 -  object Console_Progress extends Progress {
    1.19 +  class Console_Progress(verbose: Boolean) extends Progress
    1.20 +  {
    1.21      override def echo(msg: String) { java.lang.System.out.println(msg) }
    1.22 +    override def theory(session: String, theory: String): Unit =
    1.23 +      if (verbose) echo(session + ": theory " + theory)
    1.24    }
    1.25  
    1.26  
    1.27 @@ -485,7 +489,7 @@
    1.28          Isabelle_System.bash_env(info.dir.file, env, script,
    1.29            out_progress = (line: String) =>
    1.30              if (line.startsWith(LOADING_THEORY))
    1.31 -              progress.theory(line.substring(LOADING_THEORY.length)))
    1.32 +              progress.theory(name, line.substring(LOADING_THEORY.length)))
    1.33        }
    1.34  
    1.35      def terminate: Unit = thread.interrupt
    1.36 @@ -775,9 +779,9 @@
    1.37              val dirs =
    1.38                select_dirs.map(d => (true, Path.explode(d))) :::
    1.39                include_dirs.map(d => (false, Path.explode(d)))
    1.40 -            build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
    1.41 -              clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
    1.42 -              verbose, sessions)
    1.43 +            build(new Build.Console_Progress(verbose), options, requirements, all_sessions,
    1.44 +              build_heap, clean_build, dirs, session_groups, max_jobs, list_files, no_build,
    1.45 +              system_mode, verbose, sessions)
    1.46          case _ => error("Bad arguments:\n" + cat_lines(args))
    1.47        }
    1.48      }
     2.1 --- a/src/Pure/Tools/build_dialog.scala	Sat Jan 12 15:00:48 2013 +0100
     2.2 +++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 12 16:43:38 2013 +0100
     2.3 @@ -83,8 +83,10 @@
     2.4  
     2.5      val progress = new Build.Progress
     2.6      {
     2.7 -      override def theory(name: String): Unit = echo("  theory " + name)
     2.8 -      override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
     2.9 +      override def echo(msg: String): Unit =
    2.10 +        Swing_Thread.later { text.append(msg + "\n") }
    2.11 +      override def theory(session: String, theory: String): Unit =
    2.12 +        echo(session + ": theory " + theory)
    2.13        override def stopped: Boolean =
    2.14          Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }
    2.15      }