feat(emacs/lean-server): support SHOW and VALID

Implement lean-server-show and lean-server-valid functions.

Close #116

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,8 +212,14 @@ 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"
@@ -220,7 +234,9 @@ It has the effect of evaluating a command in the end of the current file"
     ('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))))
+    ('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"))

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)

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.")