Names, docs corrected

LeanSearchClient/Basic.lean

@@ -4,3 +4,8 @@ register_option leansearch.queries : Nat :=
   { defValue := 6
     group := "leansearch"
     descr := "Number of results requested from leansearch (default 6)" }
+
+register_option moogle.queries : Nat :=
+  { defValue := 6
+    group := "moogle"
+    descr := "Number of results requested from leansearch (default 6)" }

LeanSearchClient/MoogleExamples.lean

@@ -3,7 +3,7 @@ import LeanSearchClient.Syntax
 /-!
 # Moogle Examples
 
-Examples of using the leansearch API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
+Examples of using the Moogle API. The search is triggered when the sentence ends with a full stop (period) or a question mark.
 -/
 
 /--
@@ -20,7 +20,7 @@ Note this command sends your query to an external service at https://www.moogle.
 #guard_msgs in
 example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m"
 
-set_option leansearch.queries 1
+set_option moogle.queries 1
 
 /--
 info: From: Nat.lt (type: Nat → Nat → Prop)

LeanSearchClient/Syntax.lean

@@ -11,17 +11,24 @@ import LeanSearchClient.Basic
 # LeanSearchClient
 
 In this file, we provide syntax for search using the [leansearch API](https://leansearch.net/)
+and the [Moogle API](https://www.moogle.ai/api/search).
 from within Lean. It allows you to search for Lean tactics and theorems using natural language.
 
 We provide syntax to make a query and generate `TryThis` options to click or
 use a code action to use the results.
 
-The queries are of three forms:
+The queries are of three forms. For leansearch these are:
 
 * `Command` syntax: `#leansearch "search query"` as a command.
 * `Term` syntax: `#leansearch "search query"` as a term.
 * `Tactic` syntax: `#leansearch "search query"` as a tactic.
 
+The corresponding syntax for Moogle is:
+
+* `Command` syntax: `#moogle "search query"` as a command.
+* `Term` syntax: `#moogle "search query"` as a term.
+* `Tactic` syntax: `#moogle "search query"` as a tactic.
+
 In all cases results are displayed in the Lean Infoview and clicking these replaces the query text.
 In the cases of a query for tactics only valid tactics are displayed.
 -/
@@ -67,6 +74,8 @@ structure SearchResult where
 def queryNum : CoreM Nat := do
   return leansearch.queries.get (← getOptions)
 
+def moogleQueryNum : CoreM Nat := do
+  return moogle.queries.get (← getOptions)
 namespace SearchResult
 
 def ofJson? (js : Json) : Option SearchResult :=
@@ -268,7 +277,7 @@ syntax (name := moogle_cmd) "#moogle" str : command
   | `(command| #moogle $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getMoogleQueryCommandSuggestions s (← queryNum)
+      let suggestions ← getMoogleQueryCommandSuggestions s (← moogleQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Moogle Results")
     else
       logWarning incompleteMoogleQuery
@@ -282,7 +291,7 @@ syntax (name := moogle_term) "#moogle" str : term
   | `(#moogle $s) =>
     let s := s.getString
     if s.endsWith "." || s.endsWith "?" then
-      let suggestions ← getMoogleQueryTermSuggestions s (← queryNum)
+      let suggestions ← getMoogleQueryTermSuggestions s (← moogleQueryNum)
       TryThis.addSuggestions stx suggestions (header := "Moogle Results")
     else
       logWarning incompleteMoogleQuery
@@ -299,7 +308,7 @@ syntax (name := moogle_tactic) "#moogle" str : tactic
     if s.endsWith "." || s.endsWith "?" then
       let target ← getMainTarget
       let suggestionGroups ←
-          getMoogleQueryTacticSuggestionGroups s (← queryNum)
+          getMoogleQueryTacticSuggestionGroups s (← moogleQueryNum)
       for (name, sg) in suggestionGroups do
         let sg ←  sg.filterM fun s =>
           let sugTxt := s.suggestion