src/Pure/Tools/server_commands.scala
changeset 67940 b4e80f062fbf
parent 67937 91eb307511bb
child 67941 49a34b2fa788
     1.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:44:43 2018 +0100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:53:32 2018 +0100
     1.3 @@ -11,17 +11,6 @@
     1.4  {
     1.5    def default_preferences: String = Options.read_prefs()
     1.6  
     1.7 -  def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
     1.8 -    json match {
     1.9 -      case JSON.Value.String(name) => Some((name, Position.none))
    1.10 -      case JSON.Object(map) if map.keySet == Set("name", "pos") =>
    1.11 -      (map("name"), map("pos")) match {
    1.12 -        case (JSON.Value.String(name), Position.JSON(pos)) => Some((name, pos))
    1.13 -        case _ => None
    1.14 -      }
    1.15 -      case _ => None
    1.16 -    }
    1.17 -
    1.18    object Cancel
    1.19    {
    1.20      sealed case class Args(task: UUID)
    1.21 @@ -164,7 +153,7 @@
    1.22    {
    1.23      sealed case class Args(
    1.24        session_id: UUID,
    1.25 -      theories: List[(String, Position.T)],
    1.26 +      theories: List[String],
    1.27        master_dir: String = "",
    1.28        pretty_margin: Double = Pretty.default_margin,
    1.29        unicode_symbols: Boolean = false)
    1.30 @@ -172,7 +161,7 @@
    1.31      def unapply(json: JSON.T): Option[Args] =
    1.32        for {
    1.33          session_id <- JSON.uuid(json, "session_id")
    1.34 -        theories <- JSON.list(json, "theories", unapply_name_pos _)
    1.35 +        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
    1.36          master_dir <- JSON.string_default(json, "master_dir")
    1.37          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    1.38          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")