warnings for incomplete commads, rewording; for #10

LeanSearchClient/LoogleSyntax.lean

@@ -46,6 +46,7 @@ structure LoogleMatch where
   deriving Inhabited, Repr
 
 inductive LoogleResult where
+  | empty : LoogleResult
   | success : Array SearchResult →  LoogleResult
   | failure (error : String) (suggestions: Option <| List String) : LoogleResult
   deriving Inhabited, Repr
@@ -54,6 +55,8 @@ def getLoogleQueryJson (s : String) (num_results : Nat := 6) :
   CoreM <| LoogleResult:= do
   let apiUrl := "https://loogle.lean-lang.org/json"
   let s' := System.Uri.escapeUri s
+  if s.trim == "" then
+    return LoogleResult.empty
   let q := apiUrl ++ s!"?q={s'}"
   let s ← IO.Process.output {cmd := "curl", args := #["-X", "GET", "--user-agent", ← useragent,  q]}
   match Json.parse s.stdout with
@@ -200,6 +203,8 @@ syntax (name := loogle_cmd) "#loogle" loogle_filters  : command
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
     let result ← getLoogleQueryJson s
     match result with
+    | LoogleResult.empty =>
+      logInfo loogleUsage
     | LoogleResult.success xs =>
       let suggestions := xs.map SearchResult.toCommandSuggestion
       if suggestions.isEmpty then
@@ -220,13 +225,10 @@ syntax (name := loogle_cmd) "#loogle" loogle_filters  : command
       | none => pure ()
   | _ => throwUnsupportedSyntax
 
--- #loogle List ?a → ?b
-
--- #loogle nonsense
-
--- #loogle ?a → ?b
+@[inherit_doc loogle_cmd]
+syntax (name := just_loogle_cmd)(priority := low) "#loogle" loogle_filters  : command
+@[command_elab just_loogle_cmd] def justLoogleCmdImpl : CommandElab := fun _ => return
 
--- #loogle sin
 
 @[inherit_doc loogle_cmd]
 syntax (name := loogle_term) "#loogle" loogle_filters  : term
@@ -237,6 +239,8 @@ syntax (name := loogle_term) "#loogle" loogle_filters  : term
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
     let result ← getLoogleQueryJson s
     match result with
+    | LoogleResult.empty =>
+      logInfo loogleUsage
     | LoogleResult.success xs =>
       let suggestions := xs.map SearchResult.toTermSuggestion
       if suggestions.isEmpty then
@@ -269,6 +273,8 @@ syntax (name := loogle_tactic) "#loogle" loogle_filters  : tactic
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
     let result ← getLoogleQueryJson s
     match result with
+    | LoogleResult.empty =>
+      logInfo loogleUsage
     | LoogleResult.success xs => do
       let suggestionGroups := xs.map fun sr =>
          (sr.name, sr.toTacticSuggestions)

LeanSearchClient/Syntax.lean

@@ -207,7 +207,7 @@ def getTacticSuggestionGroups (ss : SearchServer) (s : String) (num_results : Na
     (fullName, sr.toTacticSuggestions)
 
 def incompleteSearchQuery (ss : SearchServer) : String :=
-  s!"{ss.cmd} query should end with a `.` or `?`.\n\
+  s!"{ss.cmd} query should be a string that ends with a `.` or `?`.\n\
    Note this command sends your query to an external service at {ss.url}."
 
 open Command
@@ -256,7 +256,7 @@ end SearchServer
 
 open Command
 /-- Search [LeanSearch](https://leansearch.net/) from within Lean.
-Queries should end with a `.` or `?`. This works as a command, as a term
+Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
 and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.
 
 ```lean
@@ -269,17 +269,19 @@ example : 3 ≤ 5 := by
   sorry
 ```
  -/
-syntax (name := leansearch_search_cmd) "#leansearch" str : command
+syntax (name := leansearch_search_cmd) "#leansearch" (str)? : command
 
 @[command_elab leansearch_search_cmd] def leanSearchCommandImpl : CommandElab :=
   fun stx =>
   match stx with
   | `(command| #leansearch $s) => do
     leanSearchServer.searchCommandSuggestions  stx s
+  | `(command| #leansearch) => do
+    logWarning leanSearchServer.incompleteSearchQuery
   | _ => throwUnsupportedSyntax
 
 /-- Search [Moogle](https://www.moogle.ai/api/search) from within Lean.
-Queries should end with a `.` or `?`. This works as a command, as a term
+Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
 and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.
 
 ```lean
@@ -292,53 +294,65 @@ example : 3 ≤ 5 := by
   sorry
 ```
  -/
-syntax (name := moogle_search_cmd) "#moogle" str : command
+syntax (name := moogle_search_cmd) "#moogle" (str)? : command
 
 @[command_elab moogle_search_cmd] def moogleCommandImpl : CommandElab :=
   fun stx =>
   match stx with
   | `(command| #moogle $s) => do
     moogleServer.searchCommandSuggestions  stx s
+  | `(command| #moogle) => do
+    logWarning moogleServer.incompleteSearchQuery
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc leansearch_search_cmd]
-syntax (name := leansearch_search_term) "#leansearch" str : term
+syntax (name := leansearch_search_term) "#leansearch" (str)? : term
 
 @[term_elab leansearch_search_term] def leanSearchTermImpl : TermElab :=
   fun stx expectedType? => do
   match stx with
   | `(#leansearch $s) =>
     leanSearchServer.searchTermSuggestions stx s
     defaultTerm expectedType?
+  | `(#leansearch) => do
+    logWarning leanSearchServer.incompleteSearchQuery
+    defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc moogle_search_cmd]
-syntax (name := moogle_search_term) "#moogle" str : term
+syntax (name := moogle_search_term) "#moogle" (str)? : term
 
 @[term_elab moogle_search_term] def moogleTermImpl : TermElab :=
   fun stx expectedType? => do
   match stx with
   | `(#moogle $s) =>
     moogleServer.searchTermSuggestions stx s
     defaultTerm expectedType?
+  | `(#moogle) => do
+    logWarning moogleServer.incompleteSearchQuery
+    defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc leansearch_search_cmd]
-syntax (name := leansearch_search_tactic) "#leansearch" str : tactic
+syntax (name := leansearch_search_tactic) "#leansearch" (str)? : tactic
 
 @[tactic leansearch_search_tactic] def leanSearchTacticImpl : Tactic :=
   fun stx => withMainContext do
   match stx with
   | `(tactic|#leansearch $s) =>
     leanSearchServer.searchTacticSuggestions stx s
+  | `(#leansearch) => do
+    logWarning leanSearchServer.incompleteSearchQuery
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc moogle_search_cmd]
-syntax (name := moogle_search_tactic) "#moogle" str : tactic
+syntax (name := moogle_search_tactic) "#moogle" (str)? : tactic
 
 @[tactic moogle_search_tactic] def moogleTacticImpl : Tactic :=
   fun stx => withMainContext do
   match stx with
   | `(tactic|#moogle $s) =>
     moogleServer.searchTacticSuggestions stx s
+  | `(#moogle) => do
+    logWarning moogleServer.incompleteSearchQuery
   | _ => throwUnsupportedSyntax

LeanSearchClientTest/Examples.lean

@@ -7,14 +7,14 @@ Examples of using the leansearch API. The search is triggered when the sentence
 -/
 
 /--
-warning: #leansearch query should end with a `.` or `?`.
+warning: #leansearch query should be a string that ends with a `.` or `?`.
 Note this command sends your query to an external service at https://leansearch.net/.
 -/
 #guard_msgs in
 #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m"
 
 /--
-warning: #leansearch query should end with a `.` or `?`.
+warning: #leansearch query should be a string that ends with a `.` or `?`.
 Note this command sends your query to an external service at https://leansearch.net/.
 -/
 #guard_msgs in

LeanSearchClientTest/MoogleExamples.lean

@@ -7,14 +7,14 @@ Examples of using the Moogle API. The search is triggered when the sentence ends
 -/
 
 /--
-warning: #moogle query should end with a `.` or `?`.
+warning: #moogle query should be a string that ends with a `.` or `?`.
 Note this command sends your query to an external service at https://www.moogle.ai/api/search.
 -/
 #guard_msgs in
 #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m"
 
 /--
-warning: #moogle query should end with a `.` or `?`.
+warning: #moogle query should be a string that ends with a `.` or `?`.
 Note this command sends your query to an external service at https://www.moogle.ai/api/search.
 -/
 #guard_msgs in