# HG changeset patch # User wenzelm # Date 1475429817 -7200 # Node ID 3f47fec9edfc000ff0a452e9e5f11dee95a1e045 # Parent 2e4d80723fb01c6eac31b6b48edf45df41895a8a tuned whitespace; diff -r 2e4d80723fb0 -r 3f47fec9edfc src/Pure/Concurrent/standard_thread.scala --- a/src/Pure/Concurrent/standard_thread.scala Sun Oct 02 17:05:48 2016 +0200 +++ b/src/Pure/Concurrent/standard_thread.scala Sun Oct 02 19:36:57 2016 +0200 @@ -51,7 +51,7 @@ /* delayed events */ - final class Delay private [Standard_Thread](first: Boolean, delay: => Time, event: => Unit) + final class Delay private[Standard_Thread](first: Boolean, delay: => Time, event: => Unit) { private var running: Option[Event_Timer.Request] = None diff -r 2e4d80723fb0 -r 3f47fec9edfc src/Pure/General/sqlite.scala --- a/src/Pure/General/sqlite.scala Sun Oct 02 17:05:48 2016 +0200 +++ b/src/Pure/General/sqlite.scala Sun Oct 02 19:36:57 2016 +0200 @@ -23,7 +23,7 @@ new Database(path0, connection) } - class Database private [SQLite](path: Path, val connection: Connection) + class Database private[SQLite](path: Path, val connection: Connection) { override def toString: String = path.toString diff -r 2e4d80723fb0 -r 3f47fec9edfc src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Sun Oct 02 17:05:48 2016 +0200 +++ b/src/Pure/System/bash.scala Sun Oct 02 19:36:57 2016 +0200 @@ -33,7 +33,7 @@ cleanup: () => Unit = () => ()): Process = new Process(script, cwd, env, redirect, cleanup) - class Process private [Bash]( + class Process private[Bash]( script: String, cwd: JFile, env: Map[String, String], diff -r 2e4d80723fb0 -r 3f47fec9edfc src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Oct 02 17:05:48 2016 +0200 +++ b/src/Pure/Thy/sessions.scala Sun Oct 02 19:36:57 2016 +0200 @@ -395,7 +395,7 @@ def store(system_mode: Boolean = false): Store = new Store(system_mode) - class Store private [Sessions](system_mode: Boolean) + class Store private[Sessions](system_mode: Boolean) { /* output */ diff -r 2e4d80723fb0 -r 3f47fec9edfc src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Oct 02 17:05:48 2016 +0200 +++ b/src/Pure/Tools/build.scala Sun Oct 02 19:36:57 2016 +0200 @@ -419,7 +419,7 @@ /** build with results **/ - class Results private [Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) + class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty