Implement formatting in webdemo

[BinderDavid]

Fixes #356

[BinderDavid]

Does the right thing in principle: There is now a "Format document" option available in the webdemo, but the implementation in terms of the LSP is still stubbed out.

[BinderDavid]

Not working yet, but I am sure I am pretty close ^^

[BinderDavid]

It does work now. But it is a bit slow :/

[timsueberkrueb]

I can reproduce the slowness. Interestingly, if you watch the browser console, you can observe that the following lines appear almost instantly:

client -> server: {"jsonrpc":"2.0","id":19,"method":"textDocument/formatting","params":{"textDocument":{"version":0,"uri":"inmemory://demo.pol"},"options":{"tabSize":4,"insertSpaces":true}}} [editor.bundle.js:135878:41](http://localhost:9000/editor.bundle.js)
server -> client: {"jsonrpc":"2.0","method":"window/logMessage","params":{"message":"Formatting request: inmemory://demo.pol","type":3}} [editor.bundle.js:135878:150](http://localhost:9000/editor.bundle.js)
server -> client: {"jsonrpc":"2.0","result":[{"newText":"data Nat { Z, S(n: Nat) }\n\ndef Nat.add(y: Nat): Nat {\n    Z => y,\n    S(x') => S(x'.add(y))\n}\n\ndata Vec(n: Nat) {\n    Nil: Vec(Z),\n    Cons(n x: Nat, xs: Vec(n)): Vec(S(n))\n}\n\ncodata Stream { .head: Nat, .tail: Stream }\n\ncodata NatToNat { .ap(x: Nat): Nat }","range":{"end":{"character":4294967295,"line":4294967295},"start":{"character":0,"line":0}}}],"id":19} [editor.bundle.js:135878:150](http://localhost:9000/editor.bundle.js)
 [info] Formatting request: inmemory://demo.pol [editor.bundle.js:135892:602](http://localhost:9000/editor.bundle.js)

Note that this already includes the formatting result sent by the server. Then, after a noticeable delay, we see:

client -> server: {"jsonrpc":"2.0","method":"textDocument/didChange","params":{"textDocument":{"version":0,"uri":"inmemory://demo.pol"},"contentChanges":[{"range":{"start":{"line":0,"character":0},"end":{"line":14,"character":36}},"text":"data Nat { Z, S(n: Nat) }\n\ndef Nat.add(y: Nat): Nat {\n    Z => y,\n    S(x') => S(x'.add(y))\n}\n\ndata Vec(n: Nat) {\n    Nil: Vec(Z),\n    Cons(n x: Nat, xs: Vec(n)): Vec(S(n))\n}\n\ncodata Stream { .head: Nat, .tail: Stream }\n\ncodata NatToNat { .ap(x: Nat): Nat }"}]}} [editor.bundle.js:135878:41](http://localhost:9000/editor.bundle.js)
server -> client: {"jsonrpc":"2.0","method":"window/logMessage","params":{"message":"Changed file: inmemory://demo.pol","type":3}} [editor.bundle.js:135878:150](http://localhost:9000/editor.bundle.js)
server -> client: {"jsonrpc":"2.0","method":"textDocument/publishDiagnostics","params":{"diagnostics":[],"uri":"inmemory://demo.pol"}} [editor.bundle.js:135878:150](http://localhost:9000/editor.bundle.js)
 [info] Changed file: inmemory://demo.pol [editor.bundle.js:135892:602](http://localhost:9000/editor.bundle.js)
client -> server: {"jsonrpc":"2.0","id":20,"method":"textDocument/codeAction","params":{"textDocument":{"version":0,"uri":"inmemory://demo.pol"},"range":{"start":{"line":14,"character":35},"end":{"line":14,"character":36}},"context":{"diagnostics":[]}}} [editor.bundle.js:135878:41](http://localhost:9000/editor.bundle.js)
server -> client: {"jsonrpc":"2.0","method":"window/logMessage","params":{"message":"Code action request: inmemory://demo.pol","type":3}} [editor.bundle.js:135878:150](http://localhost:9000/editor.bundle.js)
server -> client: {"jsonrpc":"2.0","result":[{"edit":{"changes":{"inmemory://demo.pol":[{"newText":"data NatToNat { }\n\ndef NatToNat.ap(x: Nat): Nat { }","range":{"end":{"character":36,"line":14},"start":{"character":0,"line":14}}}]}},"kind":"refactor.rewrite","title":"Defunctionalize NatToNat"}],"id":20} [editor.bundle.js:135878:150](http://localhost:9000/editor.bundle.js)
 [info] Code action request: inmemory://demo.pol

Hence, it seems to be more of a client-side issue or an LSP client-server interaction bottleneck, but probably not a performance issue in the main polarity code.

[BinderDavid]

Let's observe if we have the same slowness on the version served by github.io. Unlikely, but we'll see :)