renamed "go" to "do_search"

LeanSearchClient/LoogleSyntax.lean

@@ -136,11 +136,11 @@ syntax loogle_filter := (turnstyle term) <|> term
 syntax loogle_filters := loogle_filter,*
 
 open Command
-syntax (name := loogle_cmd) "#loogle" loogle_filters "go" : command
+syntax (name := loogle_cmd) "#loogle" loogle_filters "do_search" : command
 @[command_elab loogle_cmd] def loogleCmdImpl : CommandElab := fun stx =>
   Command.liftTermElabM do
   match stx with
-  | `(command| #loogle $args:loogle_filters go) =>
+  | `(command| #loogle $args:loogle_filters do_search) =>
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
     logInfo s
     let result ← getLoogleQueryJson s
@@ -159,26 +159,26 @@ syntax (name := loogle_cmd) "#loogle" loogle_filters "go" : command
       | some suggestions =>
         let suggestions : List TryThis.Suggestion :=
           suggestions.map fun s =>
-            {suggestion := .string s!"#loogle \"{s}\" go"}
+            {suggestion := .string s!"#loogle \"{s}\" do_search"}
         unless suggestions.isEmpty do
           TryThis.addSuggestions stx suggestions.toArray (header := s!"Did you maybe mean")
       | none => pure ()
   | _ => throwUnsupportedSyntax
 
--- #loogle List ?a → ?b go
+-- #loogle List ?a → ?b do_search
 
--- #loogle nonsense go
+-- #loogle nonsense do_search
 
--- #loogle ?a → ?b go
+-- #loogle ?a → ?b do_search
 
--- #loogle sin go
+-- #loogle sin do_search
 
 
-syntax (name := loogle_term) "#loogle" loogle_filters "go" : term
+syntax (name := loogle_term) "#loogle" loogle_filters "do_search" : term
 @[term_elab loogle_term] def loogleTermImpl : TermElab :=
     fun stx expectedType? => do
   match stx with
-  | `(#loogle $args go) =>
+  | `(#loogle $args do_search) =>
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
     let result ← getLoogleQueryJson s
     match result with
@@ -198,18 +198,18 @@ syntax (name := loogle_term) "#loogle" loogle_filters "go" : term
         let suggestions : List TryThis.Suggestion :=
           suggestions.map fun s =>
             let s := s.replace "\"" "\\\""
-            {suggestion := .string s!"#loogle \"{s}\" go"}
+            {suggestion := .string s!"#loogle \"{s}\" do_search"}
         unless suggestions.isEmpty do
           TryThis.addSuggestions stx suggestions.toArray (header := s!"Did you maybe mean")
       | none => pure ()
     defaultTerm expectedType?
   | _ => throwUnsupportedSyntax
 
-syntax (name := loogle_tactic) "#loogle" loogle_filters "go" : tactic
+syntax (name := loogle_tactic) "#loogle" loogle_filters "do_search" : tactic
 @[tactic loogle_tactic] def loogleTacticImpl : Tactic :=
     fun stx => do
   match stx with
-  | `(tactic|#loogle $args go) =>
+  | `(tactic|#loogle $args do_search) =>
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
     let result ← getLoogleQueryJson s
     match result with
@@ -239,19 +239,19 @@ syntax (name := loogle_tactic) "#loogle" loogle_filters "go" : tactic
       | some suggestions =>
         let suggestions : List TryThis.Suggestion :=
           suggestions.map fun s =>
-            {suggestion := .string s!"#loogle \"{s}\" go"}
+            {suggestion := .string s!"#loogle \"{s}\" do_search"}
         unless suggestions.isEmpty do
           TryThis.addSuggestions stx suggestions.toArray (header := s!"Did you maybe mean")
       | none => pure ()
   | _ => throwUnsupportedSyntax
 
 
 example : 3 ≤ 5 := by
-  -- #loogle Nat.succ_le_succ go
+  -- #loogle Nat.succ_le_succ do_search
   decide
 
--- example := #loogle List ?a → ?b go
+-- example := #loogle List ?a → ?b do_search
 
 end LeanSearchClient
 
--- #loogle "sin", Real → Real, |- Real go
+-- #loogle "sin", Real → Real, |- Real do_search

LeanSearchClientTest/LoogleExamples.lean

@@ -3,16 +3,16 @@ import LeanSearchClient.LoogleSyntax
 /-!
 # Loogle Examples
 
-Examples of using the Loogle API. The search is triggered by the word go at the end of the query.
+Examples of using the Loogle API. The search is triggered by the word do_search at the end of the query.
 -/
 
-#loogle List ?a → ?a go
+#loogle List ?a → ?a do_search
 
-example := #loogle List ?a → ?a go
+example := #loogle List ?a → ?a do_search
 
 
 set_option loogle.queries 1
 
 example : 3 ≤ 5 := by
-  #loogle Nat.succ_le_succ go
+  #loogle Nat.succ_le_succ do_search
   sorry

README.md

@@ -66,14 +66,14 @@ example : 3 ≤ 5 := by
 
 ## Loogle Search
 
-The `#loogle` command can also be used in all three modes. The syntax in this case is `#loogle <search query> go` as in the following examples.
+The `#loogle` command can also be used in all three modes. The syntax in this case is `#loogle <search query> do_search` as in the following examples.
 
 ```lean
-#loogle List ?a → ?a go
+#loogle List ?a → ?a do_search
 
-example := #loogle List ?a → ?a go
+example := #loogle List ?a → ?a do_search
 
 example : 3 ≤ 5 := by
-  #loogle Nat.succ_le_succ go
+  #loogle Nat.succ_le_succ do_search
   sorry
 ```