From 88410bf278207c0f0b708bbe2683ac7cdd325710 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 3 Sep 2014 00:45:16 -0700 Subject: [PATCH] feat(emacs/lean-server): support SHOW and VALID Implement lean-server-show and lean-server-valid functions. Close #116 --- src/emacs/lean-cmd.el | 40 ++++++++++++++++++++++++++------------ src/emacs/lean-server.el | 29 +++++++++++++++++++++++++-- src/emacs/lean-variable.el | 2 +- 3 files changed, 56 insertions(+), 15 deletions(-) diff --git a/src/emacs/lean-cmd.el b/src/emacs/lean-cmd.el index f6da8caa0..51a60d0e0 100644 --- a/src/emacs/lean-cmd.el +++ b/src/emacs/lean-cmd.el @@ -84,6 +84,14 @@ It has the effect of evaluating a command in the end of the current file" "Clear Cache" `(CLEAR-CACHE)) +(defun lean-cmd-show () + "Display the \"lines\" associated with the current buffer, or at least" + `(SHOW)) + +(defun lean-cmd-valid () + "Display valid/invalid lines. Invalid lines are the one we need to refresh type information" + `(VALID)) + ;; Type ;; ==== (defun lean-cmd-type (cmd) @@ -204,23 +212,31 @@ It has the effect of evaluating a command in the end of the current file" "Convert Options command to string" (format "OPTIONS")) (defun lean-cmd-clear-cache-to-string (cmd) - "Convert Options command to string" + "Convert clear-cache command to string" (format "CLEAR_CACHE")) +(defun lean-cmd-show-to-string (cmd) + "Convert show command to string" + (format "SHOW")) +(defun lean-cmd-valid-to-string (cmd) + "Convert valid command to string" + (format "VALID")) (defun lean-cmd-to-string (cmd) "Convert command to string" (cl-case (lean-cmd-type cmd) - ('LOAD (lean-cmd-load-to-string cmd)) - ('VISIT (lean-cmd-visit-to-string cmd)) - ('REPLACE (lean-cmd-replace-to-string cmd)) - ('INSERT (lean-cmd-insert-to-string cmd)) - ('REMOVE (lean-cmd-remove-to-string cmd)) - ('INFO (lean-cmd-info-to-string cmd)) - ('CHECK (lean-cmd-check-to-string cmd)) - ('SET (lean-cmd-set-to-string cmd)) - ('EVAL (lean-cmd-eval-to-string cmd)) - ('OPTIONS (lean-cmd-options-to-string cmd)) - ('CLEAR-CACHE (lean-cmd-clear-cache-to-string cmd)))) + ('LOAD (lean-cmd-load-to-string cmd)) + ('VISIT (lean-cmd-visit-to-string cmd)) + ('REPLACE (lean-cmd-replace-to-string cmd)) + ('INSERT (lean-cmd-insert-to-string cmd)) + ('REMOVE (lean-cmd-remove-to-string cmd)) + ('INFO (lean-cmd-info-to-string cmd)) + ('CHECK (lean-cmd-check-to-string cmd)) + ('SET (lean-cmd-set-to-string cmd)) + ('EVAL (lean-cmd-eval-to-string cmd)) + ('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)))) ;; -- Test (cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean")) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 939d2ac4f..36123f28e 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -49,6 +49,8 @@ ,(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))) "Regular expression pattern for lean-server message syntax") @@ -195,7 +197,9 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. ('CHECK ()) ('SET ()) ('EVAL (lean-server-check-current-file)) - ('OPTIONS ()))) + ('OPTIONS ()) + ('SHOW ()) + ('VALID ()))) (defun lean-server-after-send-cmd (cmd) "Operations to perform after sending a command." @@ -209,7 +213,9 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. ('CHECK ()) ('SET ()) ('EVAL ()) - ('OPTIONS ()))) + ('OPTIONS ()) + ('SHOW ()) + ('VALID ()))) (defun lean-server-send-cmd (cmd &optional cont) "Send string to lean-server." @@ -231,6 +237,24 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (when cont (lean-server-event-handler cont)))) +(defun lean-show-parse-string (str) + "Parse the output of eval command." + (let ((str-list (split-string str "\n"))) + ;; Drop the first line "-- BEGINSHOW" and + ;; the last line "-- ENDSHOW" + (setq str-list + (-take (- (length str-list) 2) + (-drop 1 str-list))) + (string-join str-list "\n"))) + +(defun lean-server-show () + (interactive) + (lean-server-send-cmd (lean-cmd-show) 'message)) + +(defun lean-server-valid () + (interactive) + (lean-server-send-cmd (lean-cmd-valid) 'message)) + (defun lean-server-set-timer-for-event-handler (cont) (setq lean-global-retry-timer (run-with-idle-timer @@ -285,4 +309,5 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (`() (lean-server-set-timer-for-event-handler cont) nil)))) + (provide 'lean-server) diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index e9f0d3f5c..5e008f0c9 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 | ERROR, +where TYPE := INFO | SET | EVAL | OPTIONS | SHOW | ERROR, PRE is a server message comes before the message BODY is a body of the received message.")