src/Pure/System/web_app.scala
changeset 80347 613ac8c77a84
parent 80315 a82db14570cd
child 80396 94875d8cc8bd
--- a/src/Pure/System/web_app.scala	Tue Jun 11 11:07:48 2024 +0200
+++ b/src/Pure/System/web_app.scala	Tue Jun 11 14:27:04 2024 +0200
@@ -297,12 +297,15 @@
 
       def get(key: Key): Option[String] = params.get(key)
       def apply(key: Key): String = get(key).getOrElse("")
-      def list(key: Key): List[Key] =
-        (for {
-          key1 <- params.keys.toList
-          key2 <- key1.get(key)
-          i <- key2.num
-        } yield key + i).distinct
+      def list(key: Key): List[Key] = {
+        val indexes =
+          for {
+            key1 <- params.keys.toList
+            key2 <- key1.get(key)
+            i <- key2.num
+          } yield i
+        indexes.distinct.sorted.map(key + _)
+      }
 
       def file(key: Key): Option[Bytes] = files.get(key)
     }