chore(doc/server): update server mode documentation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

doc/server.org

@@ -75,12 +75,26 @@ INFO [line-number]
 
 This command extracts typing information associated with line
 =[line-number]= (in the current file).
-Lean produces a possible empty sequence of entries terminated with
+Lean produces a possible empty sequence of entries delimited by the lines
+=-- BEGININFO= and =-- ENDINFO=.
 
 #+BEGIN_SRC
+-- BEGININFO
+[entries]*
 -- ENDINFO
 #+END_SRC
 
+If the server is still busy processing a previously requested update, then it
+produces the output
+
+#+BEGIN_SRC
+-- BEGININFO
+-- NAY
+-- ENDINFO
+#+END_SRC
+
+where =NAY= stands for "not available yet".
+
 A type information entry is of the form
 
 #+BEGIN_SRC
@@ -112,6 +126,7 @@ Information for synthesized placeholders is of the form
 Here is an example of output produced by Lean
 
 #+BEGIN_SRC
+-- BEGININFO
 -- TYPE|15|38
 num
 -- ACK
@@ -208,3 +223,12 @@ type of =Prop=.
 -- EVAL
 check Prop
 #+END_SRC
+
+If the server is still busy processing a previously requested update, then it
+produces the output
+
+#+BEGIN_SRC
+-- BEGINEVAL
+-- NAY
+-- ENDEVAL
+#+END_SRC