clarified signature: prefer enum types;
authorwenzelm
Tue, 29 Aug 2023 17:00:12 +0200
changeset 78604 9ccd5e8737cb
parent 78603 2401b5d9cee9
child 78605 0bbbf8e26708
clarified signature: prefer enum types;
src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 29 16:55:49 2023 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 29 17:00:12 2023 +0200
@@ -239,14 +239,12 @@
 
   /* approximative syntax */
 
-  object Assoc extends Enumeration {
-    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
-  }
+  enum Assoc { case NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC }
 
   sealed abstract class Syntax
   case object No_Syntax extends Syntax
   case class Prefix(delim: String) extends Syntax
-  case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
+  case class Infix(assoc: Assoc, delim: String, pri: Int) extends Syntax
 
   def decode_syntax: XML.Decode.T[Syntax] =
     XML.Decode.variant(List(
@@ -255,7 +253,7 @@
       { case (Nil, body) =>
           import XML.Decode._
           val (ass, delim, pri) = triple(int, string, int)(body)
-          Infix(Assoc(ass), delim, pri) }))
+          Infix(Assoc.fromOrdinal(ass), delim, pri) }))
 
 
   /* types */