# 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