clarified default;
authorwenzelm
Thu, 15 Mar 2018 11:20:17 +0100
changeset 67863 1805960b4a9f
parent 67862 20a0e0ea6237
child 67864 449ed1afa056
clarified default;
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")