# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1718108824 -7200
# Node ID 613ac8c77a84212408cba7d5bc65238ea3ab2f34
# Parent  b5b2f651a2634b9a9db128fd7466d4ec00de417a
sort web app parameters in list;

diff -r b5b2f651a263 -r 613ac8c77a84 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)
     }