sort web app parameters in list;
authorFabian Huch <huch@in.tum.de>
Tue, 11 Jun 2024 14:27:04 +0200
changeset 80347 613ac8c77a84
parent 80346 b5b2f651a263
child 80348 3b4f9e8b46cb
sort web app parameters in list;
src/Pure/System/web_app.scala
--- 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)
     }