# HG changeset patch
# User wenzelm
# Date 1521109217 -3600
# Node ID 1805960b4a9fa71cf89d6b53b0f4eea088da2930
# Parent  20a0e0ea6237bb1c5778a345fcddfb651634b329
clarified default;

diff -r 20a0e0ea6237 -r 1805960b4a9f src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Thu Mar 15 11:16:01 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Thu Mar 15 11:20:17 2018 +0100
@@ -9,11 +9,13 @@
 
 object Server_Commands
 {
+  def default_preferences: String = Options.read_prefs()
+
   object Session_Build
   {
     sealed case class Args(
       session: String,
-      preferences: String = "",
+      preferences: String = default_preferences,
       options: List[String] = Nil,
       dirs: List[String] = Nil,
       ancestor_session: String = "",
@@ -26,7 +28,7 @@
     def unapply(json: JSON.T): Option[Args] =
       for {
         session <- JSON.string(json, "session")
-        preferences <- JSON.string_default(json, "preferences")
+        preferences <- JSON.string_default(json, "preferences", default_preferences)
         options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
         dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
         ancestor_session <- JSON.string_default(json, "ancestor_session")