# HG changeset patch
# User wenzelm
# Date 1693320779 -7200
# Node ID 92b6958e87874b0b15d00c40bdb4f21f4fc060ed
# Parent  604a7377725c93bacd9cb9e16796583d1f9de93e
clarified signature: prefer enum types;

diff -r 604a7377725c -r 92b6958e8787 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Aug 29 16:49:17 2023 +0200
+++ b/src/Pure/Tools/phabricator.scala	Tue Aug 29 16:52:59 2023 +0200
@@ -841,7 +841,7 @@
     /* repository information */
 
     sealed case class Repository(
-      vcs: VCS.Value,
+      vcs: VCS,
       id: Long,
       phid: String,
       name: String,
@@ -853,12 +853,11 @@
       def is_hg: Boolean = vcs == VCS.hg
     }
 
-    object VCS extends Enumeration {
-      val hg, git, svn = Value
-      def read(s: String): Value =
-        try { withName(s) }
-        catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) }
-    }
+    enum VCS { case hg, git, svn }
+
+    def read_vcs(s: String): VCS =
+      try { VCS.valueOf(s) }
+      catch { case _: IllegalArgumentException => error("Unknown vcs type " + quote(s)) }
 
     def edits(typ: String, value: JSON.T): List[JSON.Object.T] =
       List(JSON.Object("type" -> typ, "value" -> value))
@@ -999,7 +998,7 @@
                 importing <- JSON.bool(fields, "isImporting")
               }
               yield {
-                val vcs = API.VCS.read(vcs_name)
+                val vcs = API.read_vcs(vcs_name)
                 val url_path =
                   if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name
                 val ssh_url =
@@ -1024,7 +1023,7 @@
       short_name: String = "",  // unique name
       description: String = "",
       public: Boolean = false,
-      vcs: API.VCS.Value = API.VCS.hg
+      vcs: API.VCS = API.VCS.hg
     ): API.Repository = {
       require(name.nonEmpty, "bad repository name")