diff --git a/src/emacs/lean-cmd.el b/src/emacs/lean-cmd.el index 51a60d0e0..076623b0d 100644 --- a/src/emacs/lean-cmd.el +++ b/src/emacs/lean-cmd.el @@ -92,6 +92,11 @@ It has the effect of evaluating a command in the end of the current file" "Display valid/invalid lines. Invalid lines are the one we need to refresh type information" `(VALID)) +(defun lean-cmd-findp (line-number prefix) + "Find All auto-complete candidates matched with prefix at line-number" + `(FINDP ,line-number ,prefix)) + + ;; Type ;; ==== (defun lean-cmd-type (cmd) @@ -125,6 +130,10 @@ It has the effect of evaluating a command in the end of the current file" (cl-third set-cmd)) (defun lean-cmd-eval-get-lean-cmd (eval-cmd) (cl-second eval-cmd)) +(defun lean-cmd-findp-get-line-number (findp-cmd) + (cl-second findp-cmd)) +(defun lean-cmd-findp-get-prefix (findp-cmd) + (cl-third findp-cmd)) ;; -- Test (cl-assert (string= (lean-cmd-load-get-file-name (lean-cmd-load "nat.lean")) @@ -174,6 +183,12 @@ It has the effect of evaluating a command in the end of the current file" (cl-assert (string= (lean-cmd-eval-get-lean-cmd (lean-cmd-eval "print 3")) "print 3")) +(cl-assert (= (lean-cmd-findp-get-line-number + (lean-cmd-findp 10 "iff_")) + 10)) +(cl-assert (string= (lean-cmd-findp-get-prefix + (lean-cmd-findp 10 "iff_")) + "iff_")) ;; to-string functions ;; =================== @@ -220,6 +235,11 @@ It has the effect of evaluating a command in the end of the current file" (defun lean-cmd-valid-to-string (cmd) "Convert valid command to string" (format "VALID")) +(defun lean-cmd-findp-to-string (cmd) + "Convert valid command to string" + (format "FINDP %d\n%s" + (lean-cmd-findp-get-line-number cmd) + (lean-cmd-findp-get-prefix cmd))) (defun lean-cmd-to-string (cmd) "Convert command to string" @@ -236,7 +256,8 @@ It has the effect of evaluating a command in the end of the current file" ('OPTIONS (lean-cmd-options-to-string cmd)) ('CLEAR-CACHE (lean-cmd-clear-cache-to-string cmd)) ('SHOW (lean-cmd-show-to-string cmd)) - ('VALID (lean-cmd-valid-to-string cmd)))) + ('VALID (lean-cmd-valid-to-string cmd)) + ('FINDP (lean-cmd-findp-to-string cmd)))) ;; -- Test (cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean")) @@ -253,5 +274,7 @@ It has the effect of evaluating a command in the end of the current file" (concat "INFO 42"))) (cl-assert (string= (lean-cmd-to-string (lean-cmd-check 42 "∀ (n : nat), ne (succ n) zero")) (concat "CHECK 42" "\n" "∀ (n : nat), ne (succ n) zero"))) +(cl-assert (string= (lean-cmd-to-string (lean-cmd-findp 42 "iff_")) + (concat "FINDP 42" "\n" "iff_"))) ;; ---------------- (provide 'lean-cmd) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 70036e5b7..628fcc771 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -42,18 +42,20 @@ ;; How to read data from an async process ;; ====================================== (defconst lean-server-syntax-pattern - `((INFO ,(rx line-start "-- BEGININFO" (* not-newline) line-end) - ,(rx line-start (group "-- ENDINFO") line-end)) - (SET ,(rx line-start "-- BEGINSET" line-end) - ,(rx line-start (group "-- ENDSET") line-end)) - (EVAL ,(rx line-start "-- BEGINEVAL" line-end) - ,(rx line-start (group "-- ENDEVAL") line-end)) + `((INFO ,(rx line-start "-- BEGININFO" (* not-newline) line-end) + ,(rx line-start (group "-- ENDINFO") line-end)) + (SET ,(rx line-start "-- BEGINSET" line-end) + ,(rx line-start (group "-- ENDSET") line-end)) + (EVAL ,(rx line-start "-- BEGINEVAL" line-end) + ,(rx line-start (group "-- ENDEVAL") line-end)) (OPTIONS ,(rx line-start "-- BEGINOPTIONS" line-end) - ,(rx line-start (group "-- ENDOPTIONS") line-end)) - (SHOW ,(rx line-start "-- BEGINSHOW" line-end) - ,(rx line-start (group "-- ENDSHOW") line-end)) - (ERROR ,(rx line-start "-- " (0+ not-newline) line-end) - ,(rx line-start (group "-- ERROR" (0+ not-newline)) line-end))) + ,(rx line-start (group "-- ENDOPTIONS") line-end)) + (SHOW ,(rx line-start "-- BEGINSHOW" line-end) + ,(rx line-start (group "-- ENDSHOW") line-end)) + (FINDP ,(rx line-start "-- BEGINFINDP" (* not-newline) line-end) + ,(rx line-start (group "-- ENDFINDP") line-end)) + (ERROR ,(rx line-start "-- " (0+ not-newline) line-end) + ,(rx line-start (group "-- ERROR" (0+ not-newline)) line-end))) "Regular expression pattern for lean-server message syntax") (defun lean-server-split-buffer (buf-str beg-regex end-regex) @@ -198,8 +200,9 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. ('SET ()) ('EVAL (lean-server-check-current-file)) ('OPTIONS ()) - ('SHOW ()) - ('VALID ()))) + ('SHOW (lean-server-check-current-file)) + ('VALID (lean-server-check-current-file)) + ('FINDP (lean-server-check-current-file)))) (defun lean-server-after-send-cmd (cmd) "Operations to perform after sending a command." @@ -215,7 +218,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. ('EVAL ()) ('OPTIONS ()) ('SHOW ()) - ('VALID ()))) + ('VALID ()) + ('FINDP ()))) (defun lean-server-send-cmd (cmd &optional cont) "Send string to lean-server." @@ -247,6 +251,18 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (-drop 1 str-list))) (string-join str-list "\n"))) +(defun lean-findp-parse-string (str) + "Parse the output of findp command." + (let ((str-list (split-string str "\n"))) + ;; Drop the first line "-- BEGINFINDP" and + ;; the last line "-- ENDFINDP" + (setq str-list + (-take (- (length str-list) 2) + (-drop 1 str-list))) + (--map + (let ((items (split-string it "|"))) + `(,(cl-first items) . ,(cl-second items))) str-list))) + (defun lean-server-show () (interactive) (lean-server-send-cmd (lean-cmd-show) 'message)) diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index 1d62f39e6..0f83f78b2 100644 --- a/src/emacs/lean-variable.el +++ b/src/emacs/lean-variable.el @@ -11,7 +11,7 @@ "A shared variable contains a received message to process. A message is in the form of (TYPE PRE BODY) -where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | ERROR, +where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | FINDP | ERROR, PRE is a server message comes before the message BODY is a body of the received message.")