--- 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)
}