author | Fabian Huch <huch@in.tum.de> |
Mon, 03 Jun 2024 19:21:22 +0200 | |
changeset 80243 | b2889dd54a2a |
parent 80206 | 3cf3ad092e3e |
child 80244 | 885fc1e837ed |
permissions | -rw-r--r-- |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
1 |
/* Title: Pure/System/web_app.scala |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Fabian Huch, TU Muenchen |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
3 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
4 |
Technical layer for web apps using server-side rendering with HTML forms. |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
5 |
*/ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
6 |
package isabelle |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
7 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
8 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
9 |
import scala.annotation.tailrec |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
10 |
import scala.collection.immutable.SortedMap |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
11 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
12 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
13 |
object Web_App { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
14 |
/* form html elements */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
15 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
16 |
object More_HTML { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
17 |
import HTML._ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
18 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
19 |
def css(s: String): Attribute = new Attribute("style", s) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
20 |
def name(n: String): Attribute = new Attribute("name", n) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
21 |
def value(v: String): Attribute = new Attribute("value", v) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
22 |
def placeholder(p: String): Attribute = new Attribute("placeholder", p) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
23 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
24 |
val fieldset = new Operator("fieldset") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
25 |
val button = new Operator("button") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
26 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
27 |
def legend(txt: String): XML.Elem = XML.Elem(Markup("legend", Nil), text(txt)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
28 |
def input(typ: String): XML.Elem = XML.Elem(Markup("input", List("type" -> typ)), Nil) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
29 |
def hidden(k: Params.Key, v: String): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
30 |
id(k.print)(name(k.print)(value(v)(input("hidden")))) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
31 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
32 |
def textfield(i: Params.Key, p: String, v: String): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
33 |
id(i.print)(name(i.print)(value(v)(placeholder(p)(input("text"))))) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
34 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
35 |
def browse(i: Params.Key, accept: List[String]): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
36 |
id(i.print)(name(i.print)(input("file"))) + ("accept" -> accept.mkString(",")) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
37 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
38 |
def label(`for`: Params.Key, txt: String): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
39 |
XML.Elem(Markup("label", List("for" -> `for`.print)), text(txt)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
40 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
41 |
def option(k: String, v: String): XML.Elem = value(k)(XML.elem("option", text(v))) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
42 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
43 |
def optgroup(txt: String, opts: XML.Body): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
44 |
XML.Elem(Markup("optgroup", List("label" -> txt)), opts) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
45 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
46 |
def select(i: Params.Key, opts: XML.Body): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
47 |
id(i.print)(name(i.print)(XML.elem("select", opts))) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
48 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
49 |
def textarea(i: Params.Key, v: String): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
50 |
id(i.print)(name(i.print)(value(v)(XML.elem("textarea", text(v + "\n"))))) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
51 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
52 |
def radio(i: Params.Key, v: Params.Key, values: List[(Params.Key, String)]): XML.Elem = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
53 |
def to_option(k: Params.Key): XML.Elem = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
54 |
val elem = id(i.print + k)(name(i.print)(value(k.print)(input("radio")))) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
55 |
if (v == k) elem + ("checked" -> "checked") else elem |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
56 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
57 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
58 |
span(values.map { case (k, v) => span(List(label(i + k, v), to_option(k))) }) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
59 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
60 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
61 |
def selection(i: Params.Key, selected: Option[String], opts: XML.Body): XML.Elem = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
62 |
def sel(elem: XML.Tree): XML.Tree = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
63 |
selected match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
64 |
case Some(value) => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
65 |
val Value = new Properties.String("value") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
66 |
elem match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
67 |
case XML.Elem(Markup("optgroup", props), body) => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
68 |
XML.Elem(Markup("optgroup", props), body.map(sel)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
69 |
case e@XML.Elem(Markup("option", Value(v)), _) if v == value => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
70 |
e + ("selected" -> "selected") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
71 |
case e => e |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
72 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
73 |
case None => elem |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
74 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
75 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
76 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
77 |
def is_empty_group(elem: XML.Tree): Boolean = elem match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
78 |
case XML.Elem(Markup("optgroup", _), body) if body.isEmpty => true |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
79 |
case _ => false |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
80 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
81 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
82 |
val default = if (selected.isEmpty) List(option("", "") + ("hidden" -> "hidden")) else Nil |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
83 |
select(i, default ::: opts.filterNot(is_empty_group).map(sel)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
84 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
85 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
86 |
def api_button(call: String, label: String): XML.Elem = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
87 |
button(text(label)) + ("formaction" -> call) + ("type" -> "submit") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
88 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
89 |
def submit_form(endpoint: String, body: XML.Body): XML.Elem = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
90 |
val default_button = css("display: none")(input("submit") + ("formaction" -> endpoint)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
91 |
val attrs = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
92 |
List("method" -> "post", "target" -> "iframe", "enctype" -> "multipart/form-data") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
93 |
XML.Elem(Markup("form", attrs), default_button :: body) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
94 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
95 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
96 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
97 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
98 |
/* form http handling */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
99 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
100 |
object Multi_Part { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
101 |
abstract class Data(name: String) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
102 |
case class Param(name: String, value: String) extends Data(name) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
103 |
case class File(name: String, file_name: String, content: Bytes) extends Data(name) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
104 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
105 |
def parse(body: Bytes): List[Data] = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
106 |
/* Seq for text with embedded bytes */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
107 |
case class Seq(text: String, bytes: Bytes) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
108 |
def split_one(sep: String): Option[(Seq, Seq)] = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
109 |
val text_i = text.indexOf(sep) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
110 |
if (text_i >= 0 && sep.nonEmpty) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
111 |
val (before_text, at_text) = text.splitAt(text_i) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
112 |
val after_text = at_text.substring(sep.length) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
113 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
114 |
// text might be shorter than bytes because of misinterpreted characters |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
115 |
var found = false |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
116 |
var bytes_i = 0 |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
117 |
while (!found && bytes_i < bytes.length) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
118 |
var sep_ok = true |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
119 |
var sep_i = 0 |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
120 |
while (sep_ok && sep_i < sep.length) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
121 |
if (bytes.charAt(bytes_i + sep_i) == sep.charAt(sep_i)) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
122 |
sep_i += 1 |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
123 |
} else { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
124 |
bytes_i += 1 |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
125 |
sep_ok = false |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
126 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
127 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
128 |
if (sep_ok) found = true |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
129 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
130 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
131 |
val before_bytes = bytes.subSequence(0, bytes_i) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
132 |
val after_bytes = bytes.subSequence(bytes_i + sep.length, bytes.length) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
133 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
134 |
Some(Seq(before_text, before_bytes), Seq(after_text, after_bytes)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
135 |
} else None |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
136 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
137 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
138 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
139 |
val s = Seq(body.text, body) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
140 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
141 |
def perhaps_unprefix(pfx: String, s: Seq): Seq = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
142 |
Library.try_unprefix(pfx, s.text) match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
143 |
case Some(text) => Seq(text, s.bytes.subSequence(pfx.length, s.bytes.length)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
144 |
case None => s |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
145 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
146 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
147 |
val Separator = """--(.*)""".r |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
148 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
149 |
s.split_one(HTTP.NEWLINE) match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
150 |
case Some(Seq(Separator(sep), _), rest) => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
151 |
val Param = """Content-Disposition: form-data; name="([^"]+)"""".r |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
152 |
val File = """Content-Disposition: form-data; name="([^"]+)"; filename="([^"]+)"""".r |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
153 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
154 |
def parts(body: Seq): Option[List[Data]] = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
155 |
for { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
156 |
(first_line, more) <- body.split_one(HTTP.NEWLINE) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
157 |
more1 = perhaps_unprefix(HTTP.NEWLINE, more) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
158 |
(value, rest) <- more1.split_one(HTTP.NEWLINE + "--" + sep) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
159 |
rest1 = perhaps_unprefix(HTTP.NEWLINE, rest) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
160 |
} yield first_line.text match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
161 |
case Param(name) => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
162 |
Multi_Part.Param(name, Line.normalize(value.text)) :: parts(rest1).getOrElse(Nil) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
163 |
case File(name, file_name) => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
164 |
value.split_one(HTTP.NEWLINE + HTTP.NEWLINE) match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
165 |
case Some(_, content) => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
166 |
Multi_Part.File(name, file_name, content.bytes) :: parts(rest1).getOrElse(Nil) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
167 |
case _ => parts(rest1).getOrElse(Nil) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
168 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
169 |
case _ => Nil |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
170 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
171 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
172 |
parts(rest).getOrElse(Nil) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
173 |
case _ => Nil |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
174 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
175 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
176 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
177 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
178 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
179 |
/* request parameters as structured data */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
180 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
181 |
object Params { |
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
182 |
def key(s: String): Key = Key(List(Key.elem(s))) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
183 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
184 |
object Key { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
185 |
sealed trait Elem { def print: String } |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
186 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
187 |
class Nested_Elem private[Key](val rep: String) extends Elem { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
188 |
override def equals(that: Any): Boolean = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
189 |
that match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
190 |
case other: Nested_Elem => rep == other.rep |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
191 |
case _ => false |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
192 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
193 |
override def hashCode(): Int = rep.hashCode |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
194 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
195 |
def print: String = rep |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
196 |
override def toString: String = print |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
197 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
198 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
199 |
class List_Elem private[Key](val rep: Int) extends Elem { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
200 |
override def equals(that: Any): Boolean = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
201 |
that match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
202 |
case other: List_Elem => rep == other.rep |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
203 |
case _ => false |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
204 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
205 |
override def hashCode(): Int = rep.hashCode |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
206 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
207 |
def print: String = rep.toString |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
208 |
override def toString: String = print |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
209 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
210 |
|
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
211 |
def elem(s: String): Elem = |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
212 |
if (s.contains('/')) error("Illegal separator in " + quote(s)) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
213 |
else { |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
214 |
for { |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
215 |
c <- s |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
216 |
if Symbol.is_ascii_blank(c) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
217 |
} error("Illegal blank character " + c.toInt + " in " + quote(s)) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
218 |
s match { |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
219 |
case Value.Int(i) => new List_Elem(i) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
220 |
case s => new Nested_Elem(s) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
221 |
} |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
222 |
} |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
223 |
|
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
224 |
def elem(i: Int): List_Elem = if (i < 0) error("Illegal list element") else new List_Elem(i) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
225 |
|
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
226 |
def is_blank(es: List[Elem]): Boolean = es.length <= 1 && es.forall(_.print.isBlank) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
227 |
def apply(es: List[Elem]): Key = if (is_blank(es)) error("Empty key") else new Key(es) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
228 |
|
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
229 |
def explode(s: String): Key = Key(space_explode('/', s).map(elem)) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
230 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
231 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
232 |
/* ordering */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
233 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
234 |
object Ordering extends scala.math.Ordering[Key] { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
235 |
def compare(key1: Key, key2: Key): Int = key1.print.compareTo(key2.print) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
236 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
237 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
238 |
|
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
239 |
class Key(private val rep: List[Key.Elem]) { |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
240 |
def +(elem: Key.Elem): Key = Key(rep :+ elem) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
241 |
def +(i: Int): Key = this + Key.elem(i) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
242 |
def +(s: String): Key = this + Key.elem(s) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
243 |
def +(key: Key) = Key(rep ++ key.rep) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
244 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
245 |
def num: Option[Int] = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
246 |
rep match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
247 |
case (e: Key.List_Elem) :: _ => Some(e.rep) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
248 |
case _ => None |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
249 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
250 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
251 |
def get(key: Key): Option[Key] = |
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
252 |
if (!rep.startsWith(key.rep)) None |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
253 |
else { |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
254 |
val rest = rep.drop(key.rep.length) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
255 |
if (Key.is_blank(rest)) None |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
256 |
else Some(Key(rest)) |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
257 |
} |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
258 |
|
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
259 |
def print = rep.map(_.print).mkString("/") |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
260 |
|
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
261 |
override def toString: String = print |
80104
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
262 |
override def equals(that: Any): Boolean = |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
263 |
that match { |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
264 |
case other: Key => rep == other.rep |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
265 |
case _ => false |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
266 |
} |
138b5172c7f8
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
Fabian Huch <huch@in.tum.de>
parents:
80059
diff
changeset
|
267 |
override def hashCode(): Int = rep.hashCode() |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
268 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
269 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
270 |
def indexed[A, B](key: Key, xs: List[A], f: (Key, A) => B): List[B] = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
271 |
for ((x, i) <- xs.zipWithIndex) yield f(key + i, x) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
272 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
273 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
274 |
object Data { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
275 |
def from_multipart(parts: List[Multi_Part.Data]): Data = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
276 |
val files = parts.collect { case f: Multi_Part.File => f } |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
277 |
val params = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
278 |
parts.collect { case Multi_Part.Param(name, value) => Key.explode(name) -> value } |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
279 |
val file_params = files.map(file => Key.explode(file.name) -> file.file_name) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
280 |
val file_files = files.map(file => Key.explode(file.name) -> file.content) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
281 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
282 |
new Data( |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
283 |
SortedMap.from(params ++ file_params)(Key.Ordering), |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
284 |
SortedMap.from(file_files)(Key.Ordering)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
285 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
286 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
287 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
288 |
class Data private(params: SortedMap[Key, String], files: SortedMap[Key, Bytes]) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
289 |
override def toString: String = "Data(" + params.toString() + "," + files.toString() + ")" |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
290 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
291 |
def get(key: Key): Option[String] = params.get(key) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
292 |
def apply(key: Key): String = get(key).getOrElse("") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
293 |
def list(key: Key): List[Key] = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
294 |
(for { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
295 |
key1 <- params.keys.toList |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
296 |
key2 <- key1.get(key) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
297 |
i <- key2.num |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
298 |
} yield key + i).distinct |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
299 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
300 |
def file(key: Key): Option[Bytes] = files.get(key) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
301 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
302 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
303 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
304 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
305 |
/* API with backend base path, and application url (e.g. for frontend links). */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
306 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
307 |
case class Paths( |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
308 |
frontend: Url, |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
309 |
api_base: Path, |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
310 |
serve_frontend: Boolean = false, |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
311 |
landing: Path = Path.current |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
312 |
) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
313 |
def api_path(path: Path, external: Boolean = true): Path = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
314 |
(if (serve_frontend) Path.explode("backend") else Path.current) + |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
315 |
(if (external) api_base else Path.current) + path |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
316 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
317 |
def route(path: Path, params: Properties.T = Nil): String = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
318 |
def param(p: Properties.Entry): String = Url.encode(p._1) + "=" + Url.encode(p._2) |
80206
3cf3ad092e3e
clarify routes: absolute in api and relative for frontend;
Fabian Huch <huch@in.tum.de>
parents:
80205
diff
changeset
|
319 |
if (params.isEmpty) path.implode else path.implode + "?" + params.map(param).mkString("&") |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
320 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
321 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
322 |
def api_route(path: Path, params: Properties.T = Nil, external: Boolean = true): String = |
80206
3cf3ad092e3e
clarify routes: absolute in api and relative for frontend;
Fabian Huch <huch@in.tum.de>
parents:
80205
diff
changeset
|
323 |
"/" + route(api_path(path, external = external), params) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
324 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
325 |
def frontend_url(path: Path, params: Properties.T = Nil): Url = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
326 |
frontend.resolve(route(path, params)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
327 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
328 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
329 |
abstract class Server[A]( |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
330 |
paths: Paths, |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
331 |
port: Int = 0, |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
332 |
verbose: Boolean = false, |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
333 |
progress: Progress = new Progress(), |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
334 |
) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
335 |
def render(model: A): XML.Body |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
336 |
val error_model: A |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
337 |
val endpoints: List[API_Endpoint] |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
338 |
val head: XML.Body |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
339 |
|
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
340 |
|
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
341 |
/* public-facing endpoints */ |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
342 |
|
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
343 |
sealed abstract class Endpoint(path: Path, method: String = "GET") |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
344 |
extends HTTP.Service(path.implode, method) { |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
345 |
|
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
346 |
def reply(request: HTTP.Request): HTTP.Response |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
347 |
|
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
348 |
def html(head: XML.Elem, body: XML.Elem): HTTP.Response = |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
349 |
HTTP.Response.html( |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
350 |
cat_lines( |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
351 |
List( |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
352 |
HTML.header, |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
353 |
HTML.output(head, hidden = true, structural = true), |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
354 |
HTML.output(body, hidden = true, structural = true), |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
355 |
HTML.footer))) |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
356 |
|
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
357 |
final def apply(request: HTTP.Request): Option[HTTP.Response] = |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
358 |
Exn.capture(reply(request)) match { |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
359 |
case Exn.Res(res) => Some(res) |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
360 |
case Exn.Exn(exn) => |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
361 |
val id = UUID.random_string() |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
362 |
progress.echo_error_message("Internal error <" + id + ">: " + exn) |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
363 |
error("Internal server error. ID: " + id) |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
364 |
} |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
365 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
366 |
|
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
367 |
class UI(path: Path) extends Endpoint(path, "GET") { |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
368 |
def reply(request: HTTP.Request): HTTP.Response = { |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
369 |
progress.echo_if(verbose, "GET ui") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
370 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
371 |
val on_load = """ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
372 |
(function() { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
373 |
window.addEventListener('message', (event) => { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
374 |
if (Number.isInteger(event.data)) { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
375 |
this.style.height=event.data + 32 + 'px' |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
376 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
377 |
}) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
378 |
}).call(this)""" |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
379 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
380 |
val set_src = """ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
381 |
const base = '""" + paths.frontend.toString.replace("/", "\\/") + """' |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
382 |
document.getElementById('iframe').src = base + '""" + paths.api_route(path).replace("/", "\\/") + """' + window.location.search""" |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
383 |
|
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
384 |
html( |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
385 |
XML.elem("head", HTML.head_meta :: head), |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
386 |
XML.Elem(Markup("body", List("style" -> "height: fit-content")), List( |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
387 |
XML.Elem( |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
388 |
Markup( |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
389 |
"iframe", |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
390 |
List( |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
391 |
"id" -> "iframe", |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
392 |
"name" -> "iframe", |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
393 |
"style" -> "border-style: none; width: 100%", |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
394 |
"onload" -> on_load)), |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
395 |
HTML.text("content")), |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
396 |
HTML.script(set_src)))) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
397 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
398 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
399 |
|
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
400 |
sealed abstract class API_Endpoint(path: Path, method: String = "GET") |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
401 |
extends Endpoint(paths.api_path(path, external = false), method) { |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
402 |
|
80205
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
403 |
def html_content(content: XML.Body, auto_reload: Boolean = false): HTTP.Response = { |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
404 |
val head1 = |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
405 |
if (!auto_reload) head |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
406 |
else HTML.script(""" |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
407 |
var state = null; |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
408 |
function heartbeat() { |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
409 |
fetch(window.location, { method: "HEAD" }).then((http_res) => { |
80243
b2889dd54a2a
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
Fabian Huch <huch@in.tum.de>
parents:
80206
diff
changeset
|
410 |
const new_state = http_res.headers.get("Content-Digest") |
80205
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
411 |
if (state === null) state = new_state |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
412 |
if (http_res.status === 200 && state !== new_state) { |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
413 |
state = new_state |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
414 |
window.location.reload() |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
415 |
} |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
416 |
setTimeout(heartbeat, 1000); |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
417 |
}) |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
418 |
} |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
419 |
setTimeout(heartbeat, 1000);""") :: head |
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
420 |
|
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
421 |
html( |
80205
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
422 |
XML.elem("head", HTML.head_meta :: head1), |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
423 |
XML.Elem( |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
424 |
Markup("body", List("onLoad" -> "parent.postMessage(document.body.scrollHeight, '*')")), |
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
425 |
content)) |
80205
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
426 |
} |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
427 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
428 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
429 |
private def query_params(request: HTTP.Request): Properties.T = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
430 |
def decode(s: String): Option[Properties.Entry] = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
431 |
s match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
432 |
case Properties.Eq(k, v) => Some(Url.decode(k) -> Url.decode(v)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
433 |
case _ => None |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
434 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
435 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
436 |
Library.try_unprefix(request.query, request.uri_name).toList.flatMap(params => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
437 |
space_explode('&', params).flatMap(decode)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
438 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
439 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
440 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
441 |
/* endpoint types */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
442 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
443 |
class Get(val path: Path, description: String, get: Properties.T => Option[A]) |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
444 |
extends API_Endpoint(path) { |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
445 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
446 |
def reply(request: HTTP.Request): HTTP.Response = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
447 |
progress.echo_if(verbose, "GET " + description) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
448 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
449 |
val params = query_params(request) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
450 |
progress.echo_if(verbose, "params: " + params.toString()) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
451 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
452 |
val model = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
453 |
get(params) match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
454 |
case Some(model) => model |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
455 |
case None => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
456 |
progress.echo_if(verbose, "Parsing failed") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
457 |
error_model |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
458 |
} |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
459 |
|
80205
fc2d791d28bd
add auto-reload for more interactive web apps;
Fabian Huch <huch@in.tum.de>
parents:
80204
diff
changeset
|
460 |
html_content(render(model), auto_reload = true) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
461 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
462 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
463 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
464 |
class Get_File(path: Path, description: String, download: Properties.T => Option[Path]) |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
465 |
extends API_Endpoint(path) { |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
466 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
467 |
def reply(request: HTTP.Request): HTTP.Response = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
468 |
progress.echo_if(verbose, "DOWNLOAD " + description) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
469 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
470 |
val params = query_params(request) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
471 |
progress.echo_if(verbose, "params: " + params.toString()) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
472 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
473 |
download(params) match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
474 |
case Some(path) => HTTP.Response.content(HTTP.Content.read(path)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
475 |
case None => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
476 |
progress.echo_if(verbose, "Fetching file path failed") |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
477 |
html_content(render(error_model)) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
478 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
479 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
480 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
481 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
482 |
class Post(path: Path, description: String, post: Params.Data => Option[A]) |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
483 |
extends API_Endpoint(path, method = "POST") { |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
484 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
485 |
def reply(request: HTTP.Request): HTTP.Response = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
486 |
progress.echo_if(verbose, "POST " + description) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
487 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
488 |
val parts = Multi_Part.parse(request.input) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
489 |
val params = Params.Data.from_multipart(parts) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
490 |
progress.echo_if(verbose, "params: " + params.toString) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
491 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
492 |
val model = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
493 |
post(params) match { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
494 |
case Some(model) => model |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
495 |
case None => |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
496 |
progress.echo_if(verbose, "Parsing failed") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
497 |
error_model |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
498 |
} |
80204
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
499 |
|
81f2fbf3975d
clarified web app endpoints;
Fabian Huch <huch@in.tum.de>
parents:
80104
diff
changeset
|
500 |
html_content(render(model)) |
80059
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
501 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
502 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
503 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
504 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
505 |
/* server */ |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
506 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
507 |
private def ui_endpoints = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
508 |
if (paths.serve_frontend) endpoints.collect { case page: Get => new UI(page.path) } else Nil |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
509 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
510 |
private lazy val server = |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
511 |
HTTP.server(port = port, name = "", services = endpoints ::: ui_endpoints) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
512 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
513 |
def run(): Unit = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
514 |
start() |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
515 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
516 |
@tailrec |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
517 |
def loop(): Unit = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
518 |
Thread.sleep(Long.MaxValue) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
519 |
loop() |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
520 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
521 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
522 |
Isabelle_Thread.interrupt_handler(_ => server.stop()) { loop() } |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
523 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
524 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
525 |
def start(): Unit = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
526 |
server.start() |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
527 |
progress.echo("Server started on " + paths.frontend_url(paths.landing)) |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
528 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
529 |
|
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
530 |
def stop(): Unit = { |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
531 |
server.stop() |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
532 |
progress.echo("Server stopped") |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
533 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
534 |
} |
37ea0727291f
moved web_app module from AFP (e.g., for building web services for the distributed build);
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
535 |
} |