1	# ezhttp/src/html: HTML escaping, the way markupsafe.escape and Jinja's
2	# autoescape do it. `&`, `<`, `>`, `"` and `'` are written as `&amp;`, `&lt;`,
3	# `&gt;`, `&#34;` and `&#39;`; every other character is written as itself.
4	# SPEC.md HTTP-HTML lists what is guaranteed.
5	import Base
6	
7	# one character that is not `&`, `<`, `>` or `"`, as `'` or as itself
8	def one.sq(+c: Char, rest: String, hit: Bool) -> String:
9	  match hit:
10	    case True{}:
11	      "&#39;" ++ rest
12	    case False{}:
13	      SCon{c, rest}
14	
15	# one character that is not `&`, `<` or `>`
16	def one.dq(+c: Char, rest: String, hit: Bool) -> String:
17	  match hit:
18	    case True{}:
19	      "&#34;" ++ rest
20	    case False{}:
21	      one.sq(c, rest, Char.is_eq(c, '\''))
22	
23	# one character that is not `&` or `<`
24	def one.gt(+c: Char, rest: String, hit: Bool) -> String:
25	  match hit:
26	    case True{}:
27	      "&gt;" ++ rest
28	    case False{}:
29	      one.dq(c, rest, Char.is_eq(c, '"'))
30	
31	# one character that is not `&`
32	def one.lt(+c: Char, rest: String, hit: Bool) -> String:
33	  match hit:
34	    case True{}:
35	      "&lt;" ++ rest
36	    case False{}:
37	      one.gt(c, rest, Char.is_eq(c, '>'))
38	
39	# one character, once it is known whether it is `&`
40	def one.amp(+c: Char, rest: String, hit: Bool) -> String:
41	  match hit:
42	    case True{}:
43	      "&amp;" ++ rest
44	    case False{}:
45	      one.lt(c, rest, Char.is_eq(c, '<'))
46	
47	# one character as it is escaped, followed by `rest`
48	def one(+c: Char, rest: String) -> String:
49	  one.amp(c, rest, Char.is_eq(c, '&'))
50	
51	# a string escaped, each character in turn, followed by `rest`
52	def escape.onto(s: String, rest: String) -> String:
53	  match s:
54	    case SNil{}:
55	      rest
56	    case SCon{+c, tail}:
57	      one(c, escape.onto(tail, rest))
58	
59	# a string escaped for HTML text or a quoted attribute value
60	def escape(s: String) -> String:
61	  escape.onto(s, "")