From f56a467bfd405b57335879982d41cd3c4ebaaaaf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Aug 2014 17:53:06 -0700 Subject: [PATCH] chore(doc/server): update server mode documentation Signed-off-by: Leonardo de Moura --- doc/server.org | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/doc/server.org b/doc/server.org index 47e9f89f0f..ec2a26d976 100644 --- a/doc/server.org +++ b/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