diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean index c811856..ae3f5b6 100644 --- a/LeanSearchClient/LoogleSyntax.lean +++ b/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 diff --git a/LeanSearchClient/Syntax.lean b/LeanSearchClient/Syntax.lean index b29ccc1..a4faa1c 100644 --- a/LeanSearchClient/Syntax.lean +++ b/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 diff --git a/LeanSearchClientTest/Examples.lean b/LeanSearchClientTest/Examples.lean index 8fcba8b..530e8ff 100644 --- a/LeanSearchClientTest/Examples.lean +++ b/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 diff --git a/LeanSearchClientTest/LoogleExamples.lean b/LeanSearchClientTest/LoogleExamples.lean index c281de4..df11430 100644 --- a/LeanSearchClientTest/LoogleExamples.lean +++ b/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