clarified modules;
authorwenzelm
Tue Sep 29 13:54:04 2015 +0200 (2015-09-29)
changeset 612768a4bd05c1735
parent 61275 053ec04ea866
child 61277 c9152a195899
clarified modules;
src/Pure/GUI/system_dialog.scala
src/Pure/PIDE/batch_session.scala
src/Pure/System/progress.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_console.scala
src/Pure/Tools/build_doc.scala
src/Pure/Tools/check_keywords.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/GUI/system_dialog.scala	Sun Sep 27 10:11:15 2015 +0200
     1.2 +++ b/src/Pure/GUI/system_dialog.scala	Tue Sep 29 13:54:04 2015 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  import scala.swing.event.ButtonClicked
     1.5  
     1.6  
     1.7 -class System_Dialog extends Build.Progress
     1.8 +class System_Dialog extends Progress
     1.9  {
    1.10    /* component state -- owned by GUI thread */
    1.11  
     2.1 --- a/src/Pure/PIDE/batch_session.scala	Sun Sep 27 10:11:15 2015 +0200
     2.2 +++ b/src/Pure/PIDE/batch_session.scala	Tue Sep 29 13:54:04 2015 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4      val parent_session =
     2.5        session_info.parent getOrElse error("No parent session for " + quote(session))
     2.6  
     2.7 -    if (Build.build(options, new Build.Console_Progress(verbose),
     2.8 +    if (Build.build(options, new Console_Progress(verbose),
     2.9          verbose = verbose, build_heap = true,
    2.10          dirs = dirs, sessions = List(parent_session)) != 0)
    2.11        new RuntimeException
    2.12 @@ -36,7 +36,7 @@
    2.13        new Resources(content.loaded_theories, content.known_theories, content.syntax)
    2.14      }
    2.15  
    2.16 -    val progress = new Build.Console_Progress(verbose)
    2.17 +    val progress = new Console_Progress(verbose)
    2.18  
    2.19      val prover_session = new Session(resources)
    2.20      val batch_session = new Batch_Session(prover_session)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/System/progress.scala	Tue Sep 29 13:54:04 2015 +0200
     3.3 @@ -0,0 +1,33 @@
     3.4 +/*  Title:      Pure/System/progress.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Progress context for system processes.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +class Progress
    3.14 +{
    3.15 +  def echo(msg: String) {}
    3.16 +  def theory(session: String, theory: String) {}
    3.17 +  def stopped: Boolean = false
    3.18 +  override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    3.19 +}
    3.20 +
    3.21 +object Ignore_Progress extends Progress
    3.22 +
    3.23 +class Console_Progress(verbose: Boolean = false) extends Progress
    3.24 +{
    3.25 +  override def echo(msg: String) { Console.println(msg) }
    3.26 +  override def theory(session: String, theory: String): Unit =
    3.27 +    if (verbose) echo(session + ": theory " + theory)
    3.28 +
    3.29 +  @volatile private var is_stopped = false
    3.30 +  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
    3.31 +  override def stopped: Boolean =
    3.32 +  {
    3.33 +    if (Thread.interrupted) is_stopped = true
    3.34 +    is_stopped
    3.35 +  }
    3.36 +}
     4.1 --- a/src/Pure/Tools/build.scala	Sun Sep 27 10:11:15 2015 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Tue Sep 29 13:54:04 2015 +0200
     4.3 @@ -19,35 +19,6 @@
     4.4  
     4.5  object Build
     4.6  {
     4.7 -  /** progress context **/
     4.8 -
     4.9 -  class Progress
    4.10 -  {
    4.11 -    def echo(msg: String) {}
    4.12 -    def theory(session: String, theory: String) {}
    4.13 -    def stopped: Boolean = false
    4.14 -    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    4.15 -  }
    4.16 -
    4.17 -  object Ignore_Progress extends Progress
    4.18 -
    4.19 -  class Console_Progress(verbose: Boolean = false) extends Progress
    4.20 -  {
    4.21 -    override def echo(msg: String) { Console.println(msg) }
    4.22 -    override def theory(session: String, theory: String): Unit =
    4.23 -      if (verbose) echo(session + ": theory " + theory)
    4.24 -
    4.25 -    @volatile private var is_stopped = false
    4.26 -    def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
    4.27 -    override def stopped: Boolean =
    4.28 -    {
    4.29 -      if (Thread.interrupted) is_stopped = true
    4.30 -      is_stopped
    4.31 -    }
    4.32 -  }
    4.33 -
    4.34 -
    4.35 -
    4.36    /** session information **/
    4.37  
    4.38    // external version
     5.1 --- a/src/Pure/Tools/build_console.scala	Sun Sep 27 10:11:15 2015 +0200
     5.2 +++ b/src/Pure/Tools/build_console.scala	Tue Sep 29 13:54:04 2015 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4  
     5.5    def build_console(
     5.6      options: Options,
     5.7 -    progress: Build.Progress = Build.Ignore_Progress,
     5.8 +    progress: Progress = Ignore_Progress,
     5.9      dirs: List[Path] = Nil,
    5.10      no_build: Boolean = false,
    5.11      system_mode: Boolean = false,
    5.12 @@ -45,7 +45,7 @@
    5.13              val options = (Options.init() /: system_options)(_ + _)
    5.14              File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
    5.15  
    5.16 -            val progress = new Build.Console_Progress()
    5.17 +            val progress = new Console_Progress()
    5.18              progress.interrupt_handler {
    5.19                build_console(options, progress,
    5.20                  dirs.map(Path.explode(_)), no_build, system_mode, session)
     6.1 --- a/src/Pure/Tools/build_doc.scala	Sun Sep 27 10:11:15 2015 +0200
     6.2 +++ b/src/Pure/Tools/build_doc.scala	Tue Sep 29 13:54:04 2015 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4  
     6.5    def build_doc(
     6.6      options: Options,
     6.7 -    progress: Build.Progress = Build.Ignore_Progress,
     6.8 +    progress: Progress = Ignore_Progress,
     6.9      all_docs: Boolean = false,
    6.10      max_jobs: Int = 1,
    6.11      system_mode: Boolean = false,
    6.12 @@ -79,7 +79,7 @@
    6.13            Properties.Value.Boolean(system_mode) ::
    6.14            Command_Line.Chunks(docs) =>
    6.15              val options = Options.init()
    6.16 -            val progress = new Build.Console_Progress()
    6.17 +            val progress = new Console_Progress()
    6.18              progress.interrupt_handler {
    6.19                build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
    6.20              }
     7.1 --- a/src/Pure/Tools/check_keywords.scala	Sun Sep 27 10:11:15 2015 +0200
     7.2 +++ b/src/Pure/Tools/check_keywords.scala	Tue Sep 29 13:54:04 2015 +0200
     7.3 @@ -32,7 +32,7 @@
     7.4    }
     7.5  
     7.6    def check_keywords(
     7.7 -    progress: Build.Progress,
     7.8 +    progress: Progress,
     7.9      keywords: Keyword.Keywords,
    7.10      check: Set[String],
    7.11      paths: List[Path])
     8.1 --- a/src/Pure/build-jars	Sun Sep 27 10:11:15 2015 +0200
     8.2 +++ b/src/Pure/build-jars	Tue Sep 29 13:54:04 2015 +0200
     8.3 @@ -82,6 +82,7 @@
     8.4    System/options.scala
     8.5    System/platform.scala
     8.6    System/posix_interrupt.scala
     8.7 +  System/progress.scala
     8.8    System/system_channel.scala
     8.9    System/utf8.scala
    8.10    Thy/html.scala