From db6451caad44785887bb9c9a1781bd861a3a46ce Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Tue, 23 Oct 2018 15:51:29 -0400
Subject: Fix a manual typo

---
 doc/manual.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 857539db..d2db4816 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2453,7 +2453,7 @@ It is most convenient to encapsulate an FFI binding with a new \texttt{.urp} fil
 \item \texttt{clientOnly Module.ident} registers a value as being allowed only in client-side code.
 \item \texttt{clientToServer Module.ident} declares a type as OK to marshal between clients and servers.  By default, abstract FFI types are not allowed to be marshalled, since your library might be maintaining invariants that the simple serialization code doesn't check.
 \item \texttt{effectful Module.ident} registers a function that can have side effects.  This is the default for \texttt{transaction}-based types, and, actually, this directive is mostly present for legacy compatibility reasons, since it used to be required explicitly for each \texttt{transaction}al function.
-\item \texttt{ffi FILE.urs} names the file giving your library's signature.  You can include multiple such files in a single \texttt{.urp} file, and each file \texttt{mod.urp} defines an FFI module \texttt{Mod}.
+\item \texttt{ffi FILE.urs} names the file giving your library's signature.  You can include multiple such files in a single \texttt{.urp} file, and each file \texttt{mod.urs} defines an FFI module \texttt{Mod}.
 \item \texttt{include FILE} requests inclusion of a C header file.
 \item \texttt{jsFile FILE} requests inclusion of a JavaScript source file.
 \item \texttt{jsFunc Module.ident=name} gives a mapping from an Ur name for a value to a JavaScript name.
-- 
cgit v1.2.3


From c1932084390aca19c748da024b7b168c160a3aea Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Fri, 14 Dec 2018 15:42:59 -0500
Subject: New .urp option: safeGetDefault

---
 doc/manual.tex   | 1 +
 src/compiler.sig | 1 +
 src/compiler.sml | 7 +++++++
 src/demo.sml     | 1 +
 src/settings.sig | 1 +
 src/settings.sml | 4 +++-
 6 files changed, 14 insertions(+), 1 deletion(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index d2db4816..e064e59e 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -190,6 +190,7 @@ Here is the complete list of directive forms.  ``FFI'' stands for ``foreign func
 \item \texttt{profile} generates an executable that may be used with gprof.
 \item \texttt{rewrite KIND FROM TO} gives a rule for rewriting canonical module paths.  For instance, the canonical path of a page may be \texttt{Mod1.Mod2.mypage}, while you would rather the page were accessed via a URL containing only \texttt{page}.  The directive \texttt{rewrite url Mod1/Mod2/mypage page} would accomplish that.  The possible values of \texttt{KIND} determine which kinds of objects are affected.  The kind \texttt{all} matches any object, and \texttt{url} matches page URLs.  The kinds \texttt{table}, \texttt{sequence}, and \texttt{view} match those sorts of SQL entities, and \texttt{relation} matches any of those three.  \texttt{cookie} matches HTTP cookies, and \texttt{style} matches CSS class names.  If \texttt{FROM} ends in \texttt{/*}, it is interpreted as a prefix matching rule, and rewriting occurs by replacing only the appropriate prefix of a path with \texttt{TO}.  The \texttt{TO} field may be left empty to express the idea of deleting a prefix.  For instance, \texttt{rewrite url Main/*} will strip all \texttt{Main/} prefixes from URLs.  While the actual external names of relations and styles have parts separated by underscores instead of slashes, all rewrite rules must be written in terms of slashes.  An optional suffix of \cd{[-]} for a \cd{rewrite} directive asks to additionally replace all \cd{\_} characters with \cd{-} characters, which can be handy for, e.g., interfacing with an off-the-shelf CSS library that prefers hyphens over underscores.
 \item \texttt{safeGet URI} asks to allow the page handler assigned this canonical URI prefix to cause persistent side effects, even if accessed via an HTTP \cd{GET} request.
+\item \texttt{safeGetDefault} asks to allow \emph{any} page handler to cause side effects, even if accessed via an HTTP \cd{GET} request.
 \item \texttt{script URL} adds \texttt{URL} to the list of extra JavaScript files to be included at the beginning of any page that uses JavaScript.  This is most useful for importing JavaScript versions of functions found in new FFI modules.
 \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server.
 \item \texttt{sigfile PATH} sets a path where your application should look for a key to use in cryptographic signing.  This is used to prevent cross-site request forgery attacks for any form handler that both reads a cookie and creates side effects.  If the referenced file doesn't exist, an application will create it and read its saved data on future invocations.  You can also initialize the file manually with any contents at least 16 bytes long; the first 16 bytes will be treated as the key.
diff --git a/src/compiler.sig b/src/compiler.sig
index bcf69fd4..7922393d 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -61,6 +61,7 @@ signature COMPILER = sig
          dbms : string option,
          sigFile : string option,
          fileCache : string option,
+         safeGetDefault : bool,
          safeGets : string list,
          onError : (string * string list * string) option,
          minHeap : int,
diff --git a/src/compiler.sml b/src/compiler.sml
index f724bf56..271cf2f1 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -65,6 +65,7 @@ type job = {
      dbms : string option,
      sigFile : string option,
      fileCache : string option,
+     safeGetDefault : bool,
      safeGets : string list,
      onError : (string * string list * string) option,
      minHeap : int,
@@ -385,6 +386,7 @@ fun institutionalizeJob (job : job) =
      Settings.setMetaRules (#filterMeta job);
      Option.app Settings.setProtocol (#protocol job);
      Option.app Settings.setDbms (#dbms job);
+     Settings.setSafeGetDefault (#safeGetDefault job);
      Settings.setSafeGets (#safeGets job);
      Settings.setOnError (#onError job);
      Settings.setMinHeap (#minHeap job);
@@ -470,6 +472,7 @@ fun parseUrp' accLibs fname =
                         dbms = NONE,
                         sigFile = NONE,
                         fileCache = NONE,
+                        safeGetDefault = false,
                         safeGets = [],
                         onError = NONE,
                         minHeap = 0,
@@ -605,6 +608,7 @@ fun parseUrp' accLibs fname =
                      val dbms = ref NONE
                      val sigFile = ref (Settings.getSigFile ())
                      val fileCache = ref (Settings.getFileCache ())
+                     val safeGetDefault = ref false
                      val safeGets = ref []
                      val onError = ref NONE
                      val minHeap = ref 0
@@ -645,6 +649,7 @@ fun parseUrp' accLibs fname =
                                  dbms = !dbms,
                                  sigFile = !sigFile,
                                  fileCache = !fileCache,
+                                 safeGetDefault = !safeGetDefault,
                                  safeGets = rev (!safeGets),
                                  onError = !onError,
                                  minHeap = !minHeap,
@@ -708,6 +713,7 @@ fun parseUrp' accLibs fname =
                                  dbms = mergeO #2 (#dbms old, #dbms new),
                                  sigFile = mergeO #2 (#sigFile old, #sigFile new),
                                  fileCache = mergeO #2 (#fileCache old, #fileCache new),
+                                 safeGetDefault = #safeGetDefault old orelse #safeGetDefault new,
                                  safeGets = #safeGets old @ #safeGets new,
                                  onError = mergeO #2 (#onError old, #onError new),
                                  minHeap = Int.max (#minHeap old, #minHeap new),
@@ -829,6 +835,7 @@ fun parseUrp' accLibs fname =
                                    | "include" => headers := relifyA arg :: !headers
                                    | "script" => scripts := arg :: !scripts
                                    | "clientToServer" => clientToServer := ffiS () :: !clientToServer
+                                   | "safeGetDefault" => safeGetDefault := true
                                    | "safeGet" => safeGets := arg :: !safeGets
                                    | "effectful" => effectful := ffiS () :: !effectful
                                    | "benignEffectful" => benignEffectful := ffiS () :: !benignEffectful
diff --git a/src/demo.sml b/src/demo.sml
index 1e58e2f8..eaec38bb 100644
--- a/src/demo.sml
+++ b/src/demo.sml
@@ -124,6 +124,7 @@ fun make' {prefix, dirname, guided} =
             dbms = mergeWith #2 (#dbms combined, #dbms urp),
             sigFile = mergeWith #2 (#sigFile combined, #sigFile urp),
             fileCache = mergeWith #2 (#fileCache combined, #fileCache urp),
+            safeGetDefault = #safeGetDefault combined orelse #safeGetDefault urp,
             safeGets = #safeGets combined @ #safeGets urp,
             onError = NONE,
             minHeap = 0,
diff --git a/src/settings.sig b/src/settings.sig
index 986d6ed7..6ba7e96a 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -258,6 +258,7 @@ signature SETTINGS = sig
     val getFileCache : unit -> string option
 
     (* Which GET-able functions should be allowed to have side effects? *)
+    val setSafeGetDefault : bool -> unit
     val setSafeGets : string list -> unit
     val isSafeGet : string -> bool
 
diff --git a/src/settings.sml b/src/settings.sml
index cfbe98a5..3772fc04 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -740,9 +740,11 @@ structure SS = BinarySetFn(struct
                            val compare = String.compare
                            end)
 
+val safeGetDefault = ref false
 val safeGet = ref SS.empty
+fun setSafeGetDefault b = safeGetDefault := b
 fun setSafeGets ls = safeGet := SS.addList (SS.empty, ls)
-fun isSafeGet x = SS.member (!safeGet, x)
+fun isSafeGet x = !safeGetDefault orelse SS.member (!safeGet, x)
 
 val onError = ref (NONE : (string * string list * string) option)
 fun setOnError x = onError := x
-- 
cgit v1.2.3


From ffcf765623b2da7ca330916eda404ac210eb513e Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 19 Dec 2018 11:38:46 -0500
Subject: Follow-up to #146: update documentation

---
 demo/prose     | 3 ++-
 doc/manual.tex | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/demo/prose b/demo/prose
index ce12aba1..75c80169 100644
--- a/demo/prose
+++ b/demo/prose
@@ -5,12 +5,13 @@
 <h6>Install System Dependencies</h6>
 
 <p>
-<blockquote><pre>sudo apt-get install build-essential \
+<blockquote><pre>sudo apt install build-essential \
   emacs-goodies-el \
   libgmp-dev \
   libssl-dev \
   libpq-dev \
   libsqlite3-dev \
+  libicu-dev \
   mlton \
   sqlite3</blockquote></pre></p>
 
diff --git a/doc/manual.tex b/doc/manual.tex
index e064e59e..59727099 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -59,9 +59,9 @@ make
 sudo make install
 \end{verbatim}
 
-Some other packages must be installed for the above to work.  At a minimum, you need a standard UNIX shell, with standard UNIX tools like sed and GCC (or an alternate C compiler) in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the development files for the OpenSSL C library.  As of this writing, in the ``testing'' version of Debian Linux, this command will install the more uncommon of these dependencies:
+Some other packages must be installed for the above to work.  At a minimum, you need a standard UNIX shell, with standard UNIX tools like sed and GCC (or an alternate C compiler) in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the development files for the OpenSSL C library and the ICU C library.  As of this writing, in the ``testing'' version of Debian Linux, this command will install the more uncommon of these dependencies:
 \begin{verbatim}
-apt-get install mlton libssl-dev
+apt-get install mlton libssl-dev libicu-dev
 \end{verbatim}
 
 Note that, like the Ur/Web compiler, MLton is a whole-program optimizing compiler, so it frequently requires much more memory than old-fashioned compilers do.  Expect building Ur/Web with MLton to require not much less than a gigabyte of RAM.  If a \texttt{mlton} invocation ends suspiciously, the most likely explanation is that it has exhausted available memory.
-- 
cgit v1.2.3


From 15105e3e62d595fe620d019a7ef9aeeb0197d24d Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 26 Jan 2019 14:24:48 -0500
Subject: Clarifying security model in the manual

---
 doc/manual.tex | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 59727099..8f7787fc 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2400,7 +2400,7 @@ A web application is built from a series of modules, with one module, the last o
 
 Elements of modules beside the main module, including page handlers, will only be included in the final application if they are transitive dependencies of the handlers in the main module.
 
-Normal links are accessible via HTTP \texttt{GET}, which the relevant standard says should never cause side effects.  To export a page which may cause side effects, accessible only via HTTP \texttt{POST}, include one argument of the page handler of type $\mt{Basis.postBody}$.  When the handler is called, this argument will receive a value that can be deconstructed into a MIME type (with $\mt{Basis.postType}$) and payload (with $\mt{Basis.postData}$).  This kind of handler should not be used with forms that exist solely within Ur/Web apps; for these, use Ur/Web's built-in support, as described below.  It may still be useful to use $\mt{Basis.postBody}$ with form requests submitted by code outside an Ur/Web app.  For such cases, the function $\mt{Top.postFields} : \mt{postBody} \to \mt{list} \; (\mt{string} \times \mt{string})$ may be useful, breaking a \texttt{POST} body of type \texttt{application/x-www-form-urlencoded} into its name-value pairs.
+Normal links are accessible via HTTP \texttt{GET}, which the relevant standard says should never cause side effects.  To export a page that may cause side effects, accessible only via HTTP \texttt{POST}, include one argument of the page handler of type $\mt{Basis.postBody}$.  When the handler is called, this argument will receive a value that can be deconstructed into a MIME type (with $\mt{Basis.postType}$) and payload (with $\mt{Basis.postData}$).  This kind of handler should not be used with forms that exist solely within Ur/Web apps; for these, use Ur/Web's built-in support, as described below.  It may still be useful to use $\mt{Basis.postBody}$ with form requests submitted by code outside an Ur/Web app.  For such cases, the function $\mt{Top.postFields} : \mt{postBody} \to \mt{list} \; (\mt{string} \times \mt{string})$ may be useful, breaking a \texttt{POST} body of type \texttt{application/x-www-form-urlencoded} into its name-value pairs.
 
 Any normal page handler may also include arguments of type $\mt{option \; Basis.queryString}$, which will be handled specially.  Rather than being deserialized from the current URI, such an argument is passed the whole query string that the handler received.  The string may be analyzed by calling $\mt{Basis.show}$ on it.  A handler of this kind may be passed as an argument to $\mt{Basis.effectfulUrl}$ to generate a URL to a page that may be used as a ``callback'' by an external service, such that the handler is allowed to cause side effects.
 
@@ -2419,9 +2419,7 @@ Ur/Web programs generally mix server- and client-side code in a fairly transpare
 
 \medskip
 
-The HTTP standard suggests that GET requests only be used in ways that generate no side effects.  Side effecting operations should use POST requests instead.  The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis.  Any page that may have a side effect must be accessed through a form, all of which use POST requests, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$.  A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions.  Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers.
-
-Ur/Web includes a kind of automatic protection against cross site request forgery attacks.  Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server.  Signing and signature checking are inserted automatically by the compiler.  This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect.
+The HTTP standard suggests that GET requests only be used in ways that generate no side effects.  Side-effecting operations should use POST requests instead.  The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis.  Any page that may have a side effect must be accessed through a form, all of which use POST requests, or via a direct call to a page handler with some argument of type $\mt{Basis.postBody}$.  A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions.  Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers.
 
 \subsection{Tasks}
 
@@ -2443,6 +2441,19 @@ The currently supported task kinds are:
 \item $\mt{periodic} \; n$: Code that is run when the application starts up and then every $n$ seconds thereafter.
 \end{itemize}
 
+\subsection{Security Model}
+
+Ur/Web follows a pragmatic security model that, nonetheless, isn't magic.  The warranty can be voided using the foreign function interface (FFI; see next section), but it is easy to check if that interface is being used, solely by inspecting \texttt{.urp} files.  If such inspection shows no use of the FFI, then a number of classic security problems are precluded (modulo bugs in the implementation of Ur/Web itself, of course):
+\begin{itemize}
+\item There can be no \textbf{code-injection attacks}.  That is, strings are never implicitly interpreted as programs and run, which can be particularly problematic for strings coming from unconstrained user input.  In the case of SQL code, the specialized name for such vulnerabilities is \emph{SQL injections}.  In the case of HTML or JavaScript code, the specialized name is \emph{cross-site scripting}.  Ur/Web programmers need not worry about the difference, because the Ur/Web implementation promises that you will know if a string is being interpreted as a program!
+\item Ur/Web includes a kind of automatic protection against \textbf{cross-site request forgery (CSRF) attacks}.  Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server.  Signing and signature checking are inserted automatically by the compiler.  This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect that the attacker couldn't cause directly due to lack of knowledge.
+\item Quite a lot of other insecure monkey business can go in web applications.  Ur/Web contains a pretty locked-down standard library, so that, for instance, it is not possible for Ur/Web code to access the file system directly... ergo it is not possible to leak secret file contents or overwrite files insecurely!  The FFI must be used to summon such rights explicitly.
+\end{itemize}
+
+However, Ur/Web doesn't guarantee ``any code that compiles is secure.''  The right model is that \emph{any HTTP endpoint exposed by the application can be called at any time with any argument values and any cookie values}.  Ur/Web does nothing to guarantee that all function calls experienced by the application are possible according to legit traversal of links and forms!  In particular, the cryptographic signing mentioned above is \emph{not} used to prevent users from making up whatever cookie values they like.  It is just used to make sure an application only takes action based on cookie values when the user has explicitly submitted a form (and presumably the application author takes care to make all forms sufficiently intuitive, so none have surprising side effects that defy security or privacy expectations).
+
+Another philosophical assumption is that \emph{there is no hope of protecting a user against an attacker with access to the legit user's browser}.  For instance, any attacker who can observe the HTML code of one page with CSRF protection is now able to trick the user into running arbitrary handler functions, since a cookie signature is not specific to the destination handler.  Sure, we would improve security slightly (at the expense of Ur/Web implementation complexity) by making signatures handler-specific or even handler-argument-specific, but the idea is that you have already lost if an attacker has that kind of access to your browser.  (And he needs browser access to see the page because of course your security-critical app is accessed only via TLS, right?)
+
 
 \section{\label{ffi}The Foreign Function Interface}
 
-- 
cgit v1.2.3


From b8b2375819b2ac9fefb3299dcbb1e04f51cb71a6 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 27 Jan 2019 10:00:38 -0500
Subject: Manual entry for '-endpoints'

---
 doc/manual.tex | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 8f7787fc..ba53f5d8 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -278,6 +278,8 @@ sqlite3 path/to/database/file <app.sql
 
 \item \texttt{-dumpSource}: When compilation fails, output to stderr the complete source code of the last intermediate program before the compilation phase that signaled the error.  (Warning: these outputs can be very long and aren't especially optimized for readability!)
 
+\item \texttt{-endpoints FILENAME}: Populate the specified file with a JSON description of all the HTTP endpoints that the compiled application supports, with information on MIME content type, for static resources.
+
 \item \texttt{-explainEmbed}: Trigger more verbose error messages about inability to embed server-side values in client-side code.
 
 \item \texttt{-js FILENAME}: Ur/Web applications with client-side code link in generated JavaScript files, which, by default, are assigned random-looking names.  Use this directive to override the filename chosen for the JavaScript code.  Be forewarned that the default method uses a name based on hashing the code itself, which is done for a good reason: browsers are very eager to cache JavaScript code, and application changes may fail to propagate quickly to browsers if this filename stays the same between versions.  In such cases, it isn't just that the user sees an old version of your application.  Instead, the application runs with a mix of old and new files, leading to arbitrary bugs that Ur/Web prevents, when used properly.
-- 
cgit v1.2.3


From e16efaf6603c4da33b74b499e0e1214c46ddf72d Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 17 Jul 2019 14:28:46 -0400
Subject: New JavaScript FFI function 'listen'

---
 doc/manual.tex  |  1 +
 lib/js/urweb.js | 10 ++++++++++
 2 files changed, 11 insertions(+)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index ba53f5d8..62b322ae 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2573,6 +2573,7 @@ It is possible to write JavaScript FFI code that interacts with the functional-r
   \item \cd{sr(v)} and \cd{sb(s, f)}, the ``return'' and ``bind'' monad operators, respectively
   \item \cd{ss(s)}, to produce the signal corresponding to source \cd{s}
   \item \cd{scur(s)}, to get the current value of signal \cd{s}
+  \item \cd{listen(s, f)}, to ask that function \cd{f} be called with the current value of \cd{s}, every time it changes, including immediately upon establishing this listener
   \end{itemize}
 
 \item The behavior of the \cd{<dyn>} pseudo-tag may be mimicked by following the right convention in a piece of HTML source code with a type like $\mt{xbody}$.  Such a piece of source code may be encoded with a JavaScript string.  To insert a dynamic section, include a \cd{<script>} tag whose content is just a call \cd{dyn(pnode, s)}.  The argument \cd{pnode} specifies what the relevant enclosing parent tag is.  Use value \cd{"tr"} when the immediate parent is \cd{<tr>}, use \cd{"table"} when the immediate parent is \cd{<table>}, and use \cd{"span"} otherwise.  The argument \cd{s} is a string-valued signal giving the HTML code to be inserted at this point.  As with the usual \cd{<dyn>} tag, that HTML subtree is automatically updated as the value of \cd{s} changes.
diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 66d427c8..332de6dc 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -2135,6 +2135,16 @@ function active(s) {
     }
 }
 
+function listen(s, onchange) {
+    var x = document.createElement("script");
+    x.dead = false;
+    x.signal = s;
+    x.sources = null;
+    x.closures = null;
+    x.recreate = onchange;
+    populate(x);
+}
+
 function input(x, s, recreate, type, name) {
     if (name) x.name = name;
     if (type) x.type = type;
-- 
cgit v1.2.3


From f54687e989372470c2848890e9499feb9fd70352 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Fri, 30 Aug 2019 17:15:48 -0400
Subject: urweb daemon restart

---
 doc/manual.tex     |  4 ++++
 src/main.mlton.sml | 15 ++++++++++-----
 2 files changed, 14 insertions(+), 5 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 62b322ae..64fe0f24 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -238,6 +238,10 @@ Further \cd{urweb} invocations in the same working directory will send requests
 \begin{verbatim}
 urweb daemon stop
 \end{verbatim}
+To restart a running (or crashed) daemon, run
+\begin{verbatim}
+urweb daemon restart
+\end{verbatim}
 Communication happens via a UNIX domain socket in file \cd{.urweb\_daemon} in the working directory.
 
 \medskip
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index e9317d46..a6eaa7ea 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -107,6 +107,8 @@ fun usage flag_info =
 
 (* Encapsulate main invocation handler in a function, possibly to be called multiple times within a daemon. *)
 
+exception DaemonExit
+
 fun oneRun args =
     let
         val timing = ref false
@@ -256,7 +258,7 @@ fun oneRun args =
 
         val () = case args of
                      ["daemon", "stop"] => (OS.FileSys.remove socket handle OS.SysErr _ => ();
-                                            OS.Process.exit OS.Process.success)
+                                            raise DaemonExit)
                    | _ => ()
 
         val sources = parse_flags (flag_info ()) args
@@ -360,7 +362,7 @@ fun startDaemon () =
                                                    OS.Process.exit OS.Process.success)
                                                 | _ =>
                                                   let
-                                                      val success = (oneRun (rev args))
+                                                      val success = (oneRun (rev args) handle DaemonExit => OS.Process.exit OS.Process.success)
                                                                     handle ex => (print "unhandled exception:\n";
                                                                                   print (General.exnMessage ex ^ "\n");
                                                                                   OS.Process.failure)
@@ -445,9 +447,12 @@ fun oneCommandLine args =
         else
             (OS.FileSys.remove socket;
              raise OS.SysErr ("", NONE))
-    end handle OS.SysErr _ => oneRun args
+    end handle OS.SysErr _ => oneRun args handle DaemonExit => OS.Process.success
             
 val () = (Globals.setResetTime ();
           case CommandLine.arguments () of
-             ["daemon", "start"] => startDaemon ()
-           | args => OS.Process.exit (oneCommandLine args))
+              ["daemon", "start"] => startDaemon ()
+            | ["daemon", "restart"] =>
+              (ignore (oneCommandLine ["daemon", "stop"]);
+               startDaemon ())
+            | args => OS.Process.exit (oneCommandLine args))
-- 
cgit v1.2.3


From 483115ee395c26ba7b52ac84757c8a1de4fe2d33 Mon Sep 17 00:00:00 2001
From: Simon Van Casteren <simon.van.casteren@gmail.com>
Date: Wed, 15 Jan 2020 00:18:07 +0100
Subject: Added some documentation for the LSP server to the manual

---
 doc/manual.tex | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 64fe0f24..779db408 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -244,6 +244,21 @@ urweb daemon restart
 \end{verbatim}
 Communication happens via a UNIX domain socket in file \cd{.urweb\_daemon} in the working directory.
 
+Bundled with the compiler is an LSP or Language Server Protocol server. This is a program that allows various editors to request information about Ur/Web code via a standardized messaging protocol. The Ur/Web LSP server currently provides basic implementations for autocompletion, hover and compiler errors. The server is started by running
+\begin{verbatim}
+urweb -startLspServer
+\end{verbatim}
+Currently there are no prebuilt editor plugins to register this server with your editor of choice but it should be fairly simple to do so. For example in Emacs using the lsp-mode, all you need to make this work is the following configuration (assuming you use the urweb-mode bundled with the compiler):
+\begin{verbatim}
+(require 'lsp)
+(setq lsp-language-id-configuration '((urweb-mode . "urweb")))
+(lsp-register-client
+  (make-lsp-client :new-connection (lsp-stdio-connection '("urweb" "-startLspServer"))
+                    :major-modes '(urweb-mode)
+                    :server-id 'urweb-lsp))
+\end{verbatim}
+Note that to keep the server responsive we don't compile Ur/Web code in the traditional way. Rather, we use only the .urs files (or if applicable .ur files that only contain valid .urs statements) for modules that are not currently being edited. That's why the LSP server requires .urs files for all of your modules.
+
 \medskip
 
 Some other command-line parameters are accepted:
-- 
cgit v1.2.3


From 6c07bbd4c486e8983ff3101411595bc1fc938834 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Sun, 19 Jan 2020 14:23:46 -0800
Subject: Fix documentation typo

Cooperative threads run *un*interrupted between context-switch points.
---
 doc/manual.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 779db408..44cd0007 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2124,7 +2124,7 @@ Configure the policy for meta names with the \texttt{allow} and \texttt{deny} \t
 
 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
 
-The concurrency model is \emph{cooperative multithreading}.  Like with, say, POSIX threads, which uses the \emph{preemptive multithreading} model, there may be multiple threads of control active at a time.  However, unlike with preemptive multithreading, the currently running thread gets to run interrupted until a well-defined \emph{context-switch} point.  Specifically, four functions defined below are the context-switch points.  They are $\mt{sleep}$, $\mt{rpc}$, $\mt{tryRpc}$, and $\mt{recv}$.  (We explain their purposes as we come to them below.)  Additional functions added via the foreign function interface might also have context-switching behavior.  In any case, it is guaranteed that a running thread ``owns the processor'' until it calls a context-switching function, at which time we may switch to running a different thread instead.
+The concurrency model is \emph{cooperative multithreading}.  Like with, say, POSIX threads, which uses the \emph{preemptive multithreading} model, there may be multiple threads of control active at a time.  However, unlike with preemptive multithreading, the currently running thread gets to run uninterrupted until a well-defined \emph{context-switch} point.  Specifically, four functions defined below are the context-switch points.  They are $\mt{sleep}$, $\mt{rpc}$, $\mt{tryRpc}$, and $\mt{recv}$.  (We explain their purposes as we come to them below.)  Additional functions added via the foreign function interface might also have context-switching behavior.  In any case, it is guaranteed that a running thread ``owns the processor'' until it calls a context-switching function, at which time we may switch to running a different thread instead.
 
 This concurrency paradigm has many nice properties.  For instance, there is almost never any need for locking or other synchronization between threads.
 
-- 
cgit v1.2.3


From a5115ec6628146cdc4b836b4e803c7bc781a4231 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Tue, 21 Jan 2020 09:51:42 -0800
Subject: monad has kind (Type->Type)->Type, not just Type->Type

---
 doc/manual.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 44cd0007..3d8e9381 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1473,7 +1473,7 @@ Some operations are only allowed in server-side code or only in client-side code
 The Ur Basis defines the monad constructor class from Haskell.
 
 $$\begin{array}{l}
-  \mt{class} \; \mt{monad} :: \mt{Type} \to \mt{Type} \\
+  \mt{class} \; \mt{monad} :: (\mt{Type} \to \mt{Type}) \to \mt{Type} \\
   \mt{val} \; \mt{return} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t} ::: \mt{Type} \\
   \hspace{.1in} \to \mt{monad} \; \mt{m} \\
   \hspace{.1in} \to \mt{t} \to \mt{m} \; \mt{t} \\
-- 
cgit v1.2.3


From 16b6fdce0bab0699fcf16f41991976b386181dd1 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Wed, 22 Jan 2020 14:43:26 -0800
Subject: Kind variables must be bracketed in expression-level binders

---
 doc/manual.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 44cd0007..fc59deec 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -644,7 +644,7 @@ A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may
 
 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references.  An expression $@x$ is a version of $x$ where all type class instance and disjointness arguments have been made explicit.  (For the purposes of this paragraph, the type family $\mt{Top.folder}$ is a type class, though it isn't marked as one by the usual means; and any record type is considered to be a type class instance type when every field's type is a type class instance type.)  An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments.  The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments.  For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations.  The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
 
-At the expression level, an analogue is available of the composite $\lambda$ form for constructors.  We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$.  A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind.  The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$.  It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.
+At the expression level, an analogue is available of the composite $\lambda$ form for constructors.  We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid [X] \mid [c \sim c]$.  A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind.  The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$.  It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.
 
 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable.  As for function arguments, only irrefutable patterns are legal.
 
-- 
cgit v1.2.3


From 15359c4e8e4546f789dfd316109aea6aa629e96e Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Wed, 22 Jan 2020 14:26:23 -0800
Subject: Consistently introduce application syntax before abstraction

Makes it slightly easier to recognize the symmetry between forms.
---
 doc/manual.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index fc59deec..2a3f21d6 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -486,8 +486,8 @@ $$\begin{array}{rrcll}
   &&& c \; c & \textrm{type-level function application} \\
   &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
   \\
-  &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
   &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\
+  &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
   \\
   &&& () & \textrm{type-level unit} \\
   &&& \#X & \textrm{field name} \\
@@ -574,8 +574,8 @@ $$\begin{array}{rrcll}
   \\
   &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
   \\
-  &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
   &&& e \; ! & \textrm{guarded expression application} \\
+  &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
   \\
   &&& \_ & \textrm{wildcard} \\
   &&& (e) & \textrm{explicit precedence} \\
-- 
cgit v1.2.3


From 3256b037dafdb0818589ca475df5e2aed64f1af2 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Wed, 22 Jan 2020 15:23:04 -0800
Subject: Elaborate e^* and e^+ syntax

Clarify that parentheses are used if and only if e consists of
multiple symbols; also, that both e and the separator (if any) will be
paranthesized. ("if any" is appropriate because the grammar extensions
for XML include "(x[=v])*", which has no separator.)

Fix the known-length type-level record syntax to indicate that commas
are used to separate field descriptors.

Change the pattern matching grammar to use "\mid" instead of "|" for
internal consistency. (No visible change, as far as I can tell.)
---
 doc/manual.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 2a3f21d6..b6febfaa 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -443,7 +443,7 @@ We give the Ur language definition in \LaTeX $\;$ math mode, since that is prett
   \end{tabular}
 \end{center}
 
-We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas.  Another separator may be used in place of a comma.  The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.
+We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas.  Another separator may be used in place of a comma.  When $e$ consists of multiple symbols, the $e$ term and separator (if any) are surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.
 
 We write $\ell$ for literals of the primitive types, for the most part following C conventions.  There are $\mt{int}$, $\mt{float}$, $\mt{char}$, and $\mt{string}$ literals.  Character literals follow the SML convention instead of the C convention, written like \texttt{\#"a"} instead of \texttt{'a'}.
 
@@ -492,7 +492,7 @@ $$\begin{array}{rrcll}
   &&& () & \textrm{type-level unit} \\
   &&& \#X & \textrm{field name} \\
   \\
-  &&& [(c = c)^*] & \textrm{known-length type-level record} \\
+  &&& [(c = c,)^*] & \textrm{known-length type-level record} \\
   &&& c \rc c & \textrm{type-level record concatenation} \\
   &&& \mt{map} & \textrm{type-level record map} \\
   \\
@@ -572,7 +572,7 @@ $$\begin{array}{rrcll}
   \\
   &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
   \\
-  &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
+  &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e\mid)^+ & \textrm{pattern matching} \\
   \\
   &&& e \; ! & \textrm{guarded expression application} \\
   &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
-- 
cgit v1.2.3


From 77d355444228fcde64572b86920e87df139fa4ed Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Tue, 4 Feb 2020 16:44:59 -0800
Subject: Fix record type shorthand

The syntax is {c : c}, not {c = c}.

Also, replace uses of shorthand (both correct and incorrect) in
semantics rules with elaborated $[c = c].
---
 doc/manual.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index bf844a0c..253cdc5d 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -622,7 +622,7 @@ There are a variety of derived syntactic forms that elaborate into the core synt
 
 In many contexts where record fields are expected, like in a projection $e.c$, a constant field may be written as simply $X$, rather than $\#X$.
 
-A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
+A record type may be written $\{(c : c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
 
 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
 
@@ -933,7 +933,7 @@ $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
   \Gamma, X \vdash e : \tau
 }$$
 
-$$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
+$$\infer{\Gamma \vdash \{\overline{c = e}\} : \$[\overline{c = \tau}]}{
   \forall i: \Gamma \vdash c_i :: \mt{Name}
   & \Gamma \vdash e_i : \tau_i
   & \forall i \neq j: \Gamma \vdash c_i \sim c_j
@@ -1000,7 +1000,7 @@ $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i
   & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
 }$$
 
-$$\infer{\Gamma \vdash \{\overline{X = p}\} \leadsto \Gamma_n; \{\overline{X = \tau}\}}{
+$$\infer{\Gamma \vdash \{\overline{X = p}\} \leadsto \Gamma_n; \$[\overline{X = \tau}]}{
   \Gamma_0 = \Gamma
   & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
 }
-- 
cgit v1.2.3


From 50dc9b9fe270e3d92955d71a1c027b076d719aca Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Tue, 4 Feb 2020 16:46:20 -0800
Subject: Fix typos in kinding judgments

Kind-polymorphism is written as "X --> k", not "X -> k".
---
 doc/manual.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 253cdc5d..8ea78e4f 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -767,10 +767,10 @@ $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
 }$$
 
 $$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{
-  \Gamma \vdash c :: X \to \kappa
+  \Gamma \vdash c :: X \longrightarrow \kappa
   & \Gamma \vdash \kappa'
 }
-\quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{
+\quad \infer{\Gamma \vdash X \Longrightarrow c :: X \longrightarrow \kappa}{
   \Gamma, X \vdash c :: \kappa
 }$$
 
-- 
cgit v1.2.3


From 5ed96ea023de0570061660363ee55c3f9cffda18 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Tue, 4 Feb 2020 16:48:57 -0800
Subject: Remove superfluous lambdas before guarded types

Guarded expression abstractions (fn [c ~ c] => e) begin with a lambda,
but guarded types ([c ~ c] => t) do not.
---
 doc/manual.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index 8ea78e4f..b1ac0041 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -797,7 +797,7 @@ $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)
   \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
 }$$
 
-$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
+$$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
   \Gamma \vdash c_1 :: \{\kappa\}
   & \Gamma \vdash c_2 :: \{\kappa'\}
   & \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type}
@@ -963,7 +963,7 @@ $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \
   & \Gamma_i \vdash e_i : \tau
 }$$
 
-$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
+$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
   \Gamma \vdash c_1 :: \{\kappa\}
   & \Gamma \vdash c_2 :: \{\kappa'\}
   & \Gamma, c_1 \sim c_2 \vdash e : \tau
-- 
cgit v1.2.3

