diff --git a/tests/playground/webserver/README.md b/tests/playground/webserver/README.md
index 0e63822b82..783a7c7859 100644
--- a/tests/playground/webserver/README.md
+++ b/tests/playground/webserver/README.md
@@ -10,7 +10,7 @@ Content-Length: 19
Hello, me!
```
-Use with e.g. GNU netcat to test in a browser:
+Use with netcat to test in a browser at http://localhost:1234:
```bash
-$ nix-shell -p netcat-gnu --run "nc -lp 1234 -e ./build/bin/Webserver"
+bash -c 'coproc nc -lp 1234; ./build/bin/Webserver <&${COPROC[0]} >&${COPROC[1]}'
```
diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean
index 5058bc56ae..1514ef829a 100644
--- a/tests/playground/webserver/Webserver.lean
+++ b/tests/playground/webserver/Webserver.lean
@@ -1,4 +1,7 @@
+-- -*- origami-fold-style: triple-braces -*-
import Lean
+
+-- namespace Webserver {{{
namespace Webserver
structure State :=
@@ -58,6 +61,7 @@ partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
when (line != "") do
[verb, path, proto] ← pure $ line.splitOn " "
| panic! "failed to parse request: " ++ line;
+ stderr ← IO.stderr; stderr.putStrLn $ "=> " ++ verb ++ " " ++ path;
headers ← parseHeaders hIn;
handler::handlers ← handlersRef.get | panic! "no handlers";
(out, st) ← handlers.foldl (fun h₁ h₂ => h₁ <|> h₂) handler { verb := verb, path := path };
@@ -71,13 +75,13 @@ partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
run hIn hOut
end Webserver
+--}}}
new_frontend
open Lean
open Lean.Parser
-namespace LX
-
+-- declare_syntax_cat element {{{
declare_syntax_cat element
declare_syntax_cat child
@@ -85,21 +89,22 @@ syntax "<" ident "/>" : element
syntax "<" ident ">" child* "" : element
-- "JSXTextCharacter : SourceCharacter but not one of {, <, > or }"
-def text : Parser := withAntiquot (mkAntiquot "text" `LX.text) {
- fn := fun c s =>
- let startPos := s.pos;
- let s := takeWhile1Fn (fun c => not ("{<>}$".contains c)) "HTML text" c s;
- mkNodeToken `LX.text startPos c s }
+def text : Parser := -- {{{
+ withAntiquot (mkAntiquot "text" `LX.text) {
+ fn := fun c s =>
+ let startPos := s.pos;
+ let s := takeWhile1Fn (fun c => not ("{<>}$".contains c)) "HTML text" c s;
+ mkNodeToken `LX.text startPos c s } -- }}}
+syntax text : child
syntax "{" term "}" : child
syntax element : child
-syntax text : child
syntax element : term
macro_rules
| `(<$n/>) => mkStxStrLit ("<" ++ toString n.getId ++ ">")
-| `(<$n>$cs*) =>
+| `(<$n>$cs*) => -- {{{
if n.getId == m.getId then do
cs ← cs.mapM fun c => match_syntax c with
| `(child|$t:text) => pure $ mkStxStrLit (t.getArg 0).getAtomVal!
@@ -109,20 +114,13 @@ macro_rules
let cs := cs.push (mkStxStrLit (""));
cs.foldlM (fun s e => `($s ++ $e)) (mkStxStrLit ("<" ++ toString n.getId ++ ">"))
else Macro.throwError m ("expected ")
+-- }}}
+-- }}}
-end LX
-
-#eval
- let name := "PLDI";
-
- Hello, {name}!
-
-
-
---#eval oh no
-
+-- open Webserver {{{
open Webserver
+-- declare_syntax_cat pathItem {{{
declare_syntax_cat pathItem
declare_syntax_cat verb
@@ -139,22 +137,22 @@ syntax path := pathItem*
syntax "GET" : verb
syntax "POST" : verb
-macro v:verb p:path " => " t:term : command => do
+macro v:verb p:path " => " t:term : command => do -- {{{
t ← `(do checkPathConsumed; $t:term);
t ← p.getArgs.foldrM (fun pi t => match_syntax pi with
| `(pathItem|$l:pathLiteral) => `(do checkPathLiteral $(mkStxStrLit (l.getArg 0).getAtomVal!); $t:term)
| `(pathItem|{$id}) => `(do $id:ident ← getPathPart; $t:term)
| _ => unreachable!) t;
- `(
-def handler : Handler := do
-checkVerb $(mkStxStrLit (v.getArg 0).getAtomVal!);
-$t:term
+ `(def handler : Handler := do
+ checkVerb $(mkStxStrLit (v.getArg 0).getAtomVal!);
+ $t:term
-@[init] def reg : IO Unit := registerHandler handler
- )
+ @[init] def reg : IO Unit := registerHandler handler)
+-- }}}
+-- }}}
+
+GET / => redirect "/greet/stranger"
-GET / =>
- redirect "/greet/stranger"
GET /greet/{name} => pure
Hello, {name}!
@@ -164,3 +162,7 @@ def main : IO Unit := do
hIn ← IO.stdin;
hOut ← IO.stdout;
Webserver.run hIn hOut
+-- }}}
+
+#eval let name := "PLDI"; Hello, {name ++ name}!
+#eval hi