# HG changeset patch
# User wenzelm
# Date 1443527644 -7200
# Node ID 8a4bd05c17351a6f216d850dc4456f5d690de685
# Parent  053ec04ea8661aed53f0e7f47605cb2a226ef15c
clarified modules;

diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/GUI/system_dialog.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -16,7 +16,7 @@
 import scala.swing.event.ButtonClicked
 
 
-class System_Dialog extends Build.Progress
+class System_Dialog extends Progress
 {
   /* component state -- owned by GUI thread */
 
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/PIDE/batch_session.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -24,7 +24,7 @@
     val parent_session =
       session_info.parent getOrElse error("No parent session for " + quote(session))
 
-    if (Build.build(options, new Build.Console_Progress(verbose),
+    if (Build.build(options, new Console_Progress(verbose),
         verbose = verbose, build_heap = true,
         dirs = dirs, sessions = List(parent_session)) != 0)
       new RuntimeException
@@ -36,7 +36,7 @@
       new Resources(content.loaded_theories, content.known_theories, content.syntax)
     }
 
-    val progress = new Build.Console_Progress(verbose)
+    val progress = new Console_Progress(verbose)
 
     val prover_session = new Session(resources)
     val batch_session = new Batch_Session(prover_session)
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/System/progress.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/progress.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -0,0 +1,33 @@
+/*  Title:      Pure/System/progress.scala
+    Author:     Makarius
+
+Progress context for system processes.
+*/
+
+package isabelle
+
+
+class Progress
+{
+  def echo(msg: String) {}
+  def theory(session: String, theory: String) {}
+  def stopped: Boolean = false
+  override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
+}
+
+object Ignore_Progress extends Progress
+
+class Console_Progress(verbose: Boolean = false) extends Progress
+{
+  override def echo(msg: String) { Console.println(msg) }
+  override def theory(session: String, theory: String): Unit =
+    if (verbose) echo(session + ": theory " + theory)
+
+  @volatile private var is_stopped = false
+  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
+  override def stopped: Boolean =
+  {
+    if (Thread.interrupted) is_stopped = true
+    is_stopped
+  }
+}
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/Tools/build.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -19,35 +19,6 @@
 
 object Build
 {
-  /** progress context **/
-
-  class Progress
-  {
-    def echo(msg: String) {}
-    def theory(session: String, theory: String) {}
-    def stopped: Boolean = false
-    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
-  }
-
-  object Ignore_Progress extends Progress
-
-  class Console_Progress(verbose: Boolean = false) extends Progress
-  {
-    override def echo(msg: String) { Console.println(msg) }
-    override def theory(session: String, theory: String): Unit =
-      if (verbose) echo(session + ": theory " + theory)
-
-    @volatile private var is_stopped = false
-    def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
-    override def stopped: Boolean =
-    {
-      if (Thread.interrupted) is_stopped = true
-      is_stopped
-    }
-  }
-
-
-
   /** session information **/
 
   // external version
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/Tools/build_console.scala
--- a/src/Pure/Tools/build_console.scala	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/Tools/build_console.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -13,7 +13,7 @@
 
   def build_console(
     options: Options,
-    progress: Build.Progress = Build.Ignore_Progress,
+    progress: Progress = Ignore_Progress,
     dirs: List[Path] = Nil,
     no_build: Boolean = false,
     system_mode: Boolean = false,
@@ -45,7 +45,7 @@
             val options = (Options.init() /: system_options)(_ + _)
             File.write(Path.explode(options_file), YXML.string_of_body(options.encode))
 
-            val progress = new Build.Console_Progress()
+            val progress = new Console_Progress()
             progress.interrupt_handler {
               build_console(options, progress,
                 dirs.map(Path.explode(_)), no_build, system_mode, session)
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/Tools/build_doc.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -16,7 +16,7 @@
 
   def build_doc(
     options: Options,
-    progress: Build.Progress = Build.Ignore_Progress,
+    progress: Progress = Ignore_Progress,
     all_docs: Boolean = false,
     max_jobs: Int = 1,
     system_mode: Boolean = false,
@@ -79,7 +79,7 @@
           Properties.Value.Boolean(system_mode) ::
           Command_Line.Chunks(docs) =>
             val options = Options.init()
-            val progress = new Build.Console_Progress()
+            val progress = new Console_Progress()
             progress.interrupt_handler {
               build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
             }
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/Tools/check_keywords.scala
--- a/src/Pure/Tools/check_keywords.scala	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/Tools/check_keywords.scala	Tue Sep 29 13:54:04 2015 +0200
@@ -32,7 +32,7 @@
   }
 
   def check_keywords(
-    progress: Build.Progress,
+    progress: Progress,
     keywords: Keyword.Keywords,
     check: Set[String],
     paths: List[Path])
diff -r 053ec04ea866 -r 8a4bd05c1735 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Sep 27 10:11:15 2015 +0200
+++ b/src/Pure/build-jars	Tue Sep 29 13:54:04 2015 +0200
@@ -82,6 +82,7 @@
   System/options.scala
   System/platform.scala
   System/posix_interrupt.scala
+  System/progress.scala
   System/system_channel.scala
   System/utf8.scala
   Thy/html.scala