From 5aa0ef56ebf8fa0568d9dd82b7f90b6940a2ddb6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 6 Sep 2014 09:15:47 -0700
Subject: [PATCH] doc(server): add FINDG and FINDP documentation, closes #144

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/server.org | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/doc/server.org b/doc/server.org
index a9dacfad8..21547bb13 100644
--- a/doc/server.org
+++ b/doc/server.org
@@ -307,3 +307,67 @@ where each entry is of the form
 
 The available =kinds= are: =Bool=, =Int=, =Unsigned Int=, =Double=,
 =String=, and =S-Expressions=.
+
+** Find pattern
+
+Given a sequence of characters, the command =FINDP= uses string fuzzy matching to
+find declarations in the environment. The procedure uses [Bitap algorithm](http://en.wikipedia.org/wiki/Bitap_algorithm).
+The approximate match is defined in terms of [Levenshtein distance](http://en.wikipedia.org/wiki/Levenshtein_distance).
+The matches are sorted based on this distance.
+
+#+BEGIN_SRC
+FINDP [line-number]
+[pattern]
+#+END_SRC
+
+The line number =[line-number]= is used to select the environment object that will be used to perform the search.
+Only declarations in the environment are considered by =FINDP=.
+The output has the following form
+
+#+BEGIN_SRC
+-- BEGINFINDP [NAY]? [STALE]?
+[entries]*
+-- ENDFINDP
+#+END_SRC
+
+The modifier =NAY= is included when the environment object for the given line is not available yet.
+The modifier =STALE= is included to indicate that an environment object is being used, but it
+does not contain the latest changes.
+
+The entries are of the form
+
+#+BEGIN_SRC
+[name]|[type]
+#+END_SRC
+
+The types are printed without using line breaks.
+The command =FINDP= is mainly used to implement auto-completion.
+
+** Find declarations for "placeholder/goal"
+
+A declaration may contain placeholders/goals =_=. Some of these placeholders are instantiated automatically by Lean.
+Others, must be manually filled by the user. The command =FINDG= generates a sequence of declarations that may be used to
+"fill" a particular placeholder. This command is only available if the declaration containing =_= is type correct, and
+lean "knows" what is the expected type for =_=.
+
+#+BEGIN_SRC
+FINDG [line-number] [column-number]
+[filters]*
+#+END_SRC
+
+The character at the given =[line-number]= and =[column-number]= must be a =_=.
+The command also accepts a sequence of filters of the form =+[id_1]= and =-[id_2]=.
+Lean will only consider declarations whose name contains =id_1= and does not contain =id_2=.
+Here is an example:
+
+#+BEGIN_SRC
+FINDG 48 10
++intro -and -elim
+#+END_SRC
+
+For the command above, lean will print any declaration whose resultant type matches the type expected by =_=, and
+whose name contains =intro= but does not contain =and= and =elim=.
+Lean does not display "trivial" matches. We say a match is trivial if the resultant type of a declaration
+matches anything.
+
+The output produced by =FINDG= uses the same format used by =FINDP=.