--- 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 */
--- 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)
--- /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
+ }
+}
--- 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
--- 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)
--- 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)
}
--- 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])
--- 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