# HG changeset patch
# User wenzelm
# Date 1484600024 -3600
# Node ID 8007f10195af4affa947b33d7c194ee447753af4
# Parent  f94ad67a0f6e7f642aa659683af5d0371672f46a
tuned signature;

diff -r f94ad67a0f6e -r 8007f10195af src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/Admin/build_doc.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -16,7 +16,7 @@
 
   def build_doc(
     options: Options,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     all_docs: Boolean = false,
     max_jobs: Int = 1,
     system_mode: Boolean = false,
diff -r f94ad67a0f6e -r 8007f10195af src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/Admin/build_history.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -102,7 +102,7 @@
 
   def build_history(
     hg: Mercurial.Repository,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     rev: String = default_rev,
     isabelle_identifier: String = default_isabelle_identifier,
     components_base: String = "",
@@ -372,7 +372,7 @@
     isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
     self_update: Boolean = false,
     push_isabelle_home: Boolean = false,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     options: String = "",
     args: String = ""): (List[(String, Bytes)], Process_Result) =
   {
diff -r f94ad67a0f6e -r 8007f10195af src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -63,7 +63,7 @@
   def build_polyml(
     root: Path,
     sha1_root: Option[Path] = None,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     arch_64: Boolean = false,
     options: List[String] = Nil,
     msys_root: Option[Path] = None,
diff -r f94ad67a0f6e -r 8007f10195af src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/Admin/build_release.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -37,7 +37,7 @@
   private val default_platform_families = List("linux", "windows", "windows64", "macos")
 
   def build_release(base_dir: Path,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     rev: String = "",
     afp_rev: String = "",
     official_release: Boolean = false,
diff -r f94ad67a0f6e -r 8007f10195af src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -318,7 +318,7 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val progress = if (verbose) new Console_Progress() else Ignore_Progress
+      val progress = if (verbose) new Console_Progress() else No_Progress
 
       if (force) cronjob(progress, exclude_task)
       else error("Need to apply force to do anything")
diff -r f94ad67a0f6e -r 8007f10195af src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/System/progress.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -15,6 +15,7 @@
   def echo(msg: String) {}
   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
   def theory(session: String, theory: String) {}
+
   def stopped: Boolean = false
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
@@ -30,7 +31,7 @@
   }
 }
 
-object Ignore_Progress extends Progress
+object No_Progress extends Progress
 
 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
 {
diff -r f94ad67a0f6e -r 8007f10195af src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -103,7 +103,7 @@
   }
 
   def dependencies(
-      progress: Progress = Ignore_Progress,
+      progress: Progress = No_Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
       list_files: Boolean = false,
@@ -387,7 +387,7 @@
 
   def build(
     options: Options,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
@@ -427,7 +427,7 @@
 
   def build_selection(
     options: Options,
-    progress: Progress = Ignore_Progress,
+    progress: Progress = No_Progress,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
diff -r f94ad67a0f6e -r 8007f10195af src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jan 16 21:33:09 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Jan 16 21:53:44 2017 +0100
@@ -50,7 +50,7 @@
 
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
 
-  def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
+  def session_build(progress: Progress = No_Progress, no_build: Boolean = false): Int =
   {
     val mode = session_build_mode()