tactics with colGt; fixes #10

LeanSearchClient/LoogleSyntax.lean

@@ -265,7 +265,8 @@ syntax (name := loogle_term) "#loogle" loogle_filters  : term
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc loogle_cmd]
-syntax (name := loogle_tactic) "#loogle" loogle_filters  : tactic
+syntax (name := loogle_tactic)
+  withPosition("#loogle" (ppSpace colGt (loogle_filters)))  : tactic
 @[tactic loogle_tactic] def loogleTacticImpl : Tactic :=
     fun stx => do
   match stx with
@@ -293,7 +294,6 @@ syntax (name := loogle_tactic) "#loogle" loogle_filters  : tactic
           | _ => pure false
         unless sg.isEmpty do
           TryThis.addSuggestions stx sg (header := s!"From: {name}")
-
     | LoogleResult.failure error suggestions? =>
       logWarning s!"Loogle search failed with error: {error}"
       logInfo loogleUsage
@@ -307,6 +307,10 @@ syntax (name := loogle_tactic) "#loogle" loogle_filters  : tactic
       | none => pure ()
   | _ => throwUnsupportedSyntax
 
+syntax (name := just_loogle_tactic)(priority := low) "#loogle"  : tactic
+@[tactic just_loogle_tactic] def justLoogleTacticImpl : Tactic :=
+  fun _ => do
+    logWarning loogleUsage
 
 example : 3 ≤ 5 := by
   -- #loogle Nat.succ_le_succ

LeanSearchClient/Syntax.lean

@@ -334,25 +334,27 @@ syntax (name := moogle_search_term) "#moogle" (str)? : term
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc leansearch_search_cmd]
-syntax (name := leansearch_search_tactic) "#leansearch" (str)? : tactic
+syntax (name := leansearch_search_tactic)
+  withPosition("#leansearch" (colGt 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
+  | `(tactic|#leansearch) => do
     logWarning leanSearchServer.incompleteSearchQuery
   | _ => throwUnsupportedSyntax
 
 @[inherit_doc moogle_search_cmd]
-syntax (name := moogle_search_tactic) "#moogle" (str)? : tactic
+syntax (name := moogle_search_tactic)
+  withPosition("#moogle" (colGt 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
+  | `(tactic|#moogle) => do
     logWarning moogleServer.incompleteSearchQuery
   | _ => throwUnsupportedSyntax

LeanSearchClientTest/Examples.lean

@@ -33,3 +33,13 @@ warning: declaration uses 'sorry'
 example : 3 ≤ 5 := by
   #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
   sorry
+
+
+/--
+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
+example : 3 ≤ 5 := by
+  #leansearch
+  decide

LeanSearchClientTest/LoogleExamples.lean

@@ -16,3 +16,7 @@ set_option loogle.queries 1
 example : 3 ≤ 5 := by
   #loogle Nat.succ_le_succ
   sorry
+
+example : 3 ≤ 5 := by
+  #loogle
+  decide