tuned whitespace;
authorwenzelm
Sun, 02 Oct 2016 19:36:57 +0200
changeset 63996 3f47fec9edfc
parent 63995 2e4d80723fb0
child 63997 e11ccb5aa82f
tuned whitespace;
src/Pure/Concurrent/standard_thread.scala
src/Pure/General/sqlite.scala
src/Pure/System/bash.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.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
 
--- 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
 
--- 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],
--- 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 */
 
--- 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