Skip to content

Commit d7caecc

Browse files
handling comments and newlines; quick-fixes for #11 and #8
1 parent 86d0d05 commit d7caecc

File tree

2 files changed

+32
-9
lines changed

2 files changed

+32
-9
lines changed

LeanSearchClient/LoogleSyntax.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,8 @@ initialize loogleCache :
5656

5757
def getLoogleQueryJson (s : String) (num_results : Nat := 6) :
5858
CoreM <| LoogleResult:= do
59+
let s := s.splitOn "/-" |>.getD 0 s |>.trim
60+
let s := s.replace "\n" " "
5961
let cache ← loogleCache.get
6062
match cache.get? (s, num_results) with
6163
| some r => return r

LeanSearchClientTest/LoogleExamples.lean

Lines changed: 30 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,38 @@ import LeanSearchClient.LoogleSyntax
66
Examples of using the Loogle API. The search is triggered by the word at the end of the query.
77
-/
88

9-
#loogle List ?a → ?a
9+
-- #loogle List ?a → ?a
1010

11-
example := #loogle List ?a → ?a
11+
-- example := #loogle List ?a → ?a
1212

1313

14-
set_option loogle.queries 1
14+
-- set_option loogle.queries 1
1515

16-
example : 35 := by
17-
#loogle Nat.succ_le_succ
18-
sorry
16+
-- example : 3 ≤ 5 := by
17+
-- #loogle Nat.succ_le_succ
18+
-- sorry
1919

20-
example : 35 := by
21-
#loogle
22-
decide
20+
-- example : 3 ≤ 5 := by
21+
-- #loogle
22+
-- decide
23+
24+
/-!
25+
More examples to test comments do not interfere with the search or caching.
26+
-/
27+
28+
#loogle ?a * _ < ?a * _ ↔ _
29+
#loogle ?a * _ < ?a * _ ↔ _ /- foo -/
30+
#loogle ?a * _ < ?a * _ ↔ _
31+
32+
33+
-- comment
34+
#loogle ?a * _ < ?a * _ ↔ _
35+
36+
/--
37+
info: Loogle Search Results
38+
• #check Option.get!
39+
-/
40+
#guard_msgs in
41+
#loogle Option ?a → ?a, "get!"
42+
43+
/- hello -/

0 commit comments

Comments
 (0)