diff --git a/src/emacs/lean-cmd.el b/src/emacs/lean-cmd.el index c7ad08e54..bb2cb88f7 100644 --- a/src/emacs/lean-cmd.el +++ b/src/emacs/lean-cmd.el @@ -76,6 +76,10 @@ set using the command set_option in a ‘.lean’ file is supported." It has the effect of evaluating a command in the end of the current file" `(EVAL ,lean-cmd)) +(defun lean-cmd-options () + "Display all configuration options available in Lean." + `(OPTIONS)) + ;; Type ;; ==== (defun lean-cmd-type (cmd) @@ -192,6 +196,9 @@ It has the effect of evaluating a command in the end of the current file" (defun lean-cmd-eval-to-string (cmd) "Convert Eval command to string" (format "EVAL\n%s" (lean-cmd-eval-get-lean-cmd cmd))) +(defun lean-cmd-options-to-string (cmd) + "Convert Options command to string" + (format "OPTIONS")) (defun lean-cmd-to-string (cmd) "Convert command to string" @@ -204,7 +211,8 @@ It has the effect of evaluating a command in the end of the current file" ('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)))) + ('EVAL (lean-cmd-eval-to-string cmd)) + ('OPTIONS (lean-cmd-options-to-string cmd)))) ;; -- Test (cl-assert (string= (lean-cmd-to-string (lean-cmd-load "~/work/lean/basic.lean")) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index f85a5a8bf..8b1cc166a 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -23,6 +23,7 @@ (require 'lean-input) (require 'lean-type) (require 'lean-tags) +(require 'lean-option) (require 'lean-syntax) (defun lean-compile-string (exe-name args file-name) diff --git a/src/emacs/lean-option.el b/src/emacs/lean-option.el new file mode 100644 index 000000000..3c14cc3f5 --- /dev/null +++ b/src/emacs/lean-option.el @@ -0,0 +1,175 @@ +(require 'dash) +(require 'dash-functional) + +(defun lean-set-parse-string (str) + "Parse the output of eval command." + (let ((str-list (split-string str "\n"))) + ;; Drop the first line "-- BEGINSET" and + ;; the last line "-- ENDSET" + (setq str-list + (-take (- (length str-list) 2) + (-drop 1 str-list))) + (string-join str-list "\n"))) + +(defun lean-set-option () + "Set Lean option." + (interactive) + (lean-get-options) + (let* ((key-list (-map 'car lean-global-option-record-alist)) + (option-name + (completing-read "Option name: " + key-list + nil t "" nil (car key-list))) + (option (cdr (assoc option-name lean-global-option-record-alist))) + (option-value (lean-option-read option))) + (lean-server-send-cmd (lean-cmd-set option-name option-value)) + (while (not lean-global-server-message-to-process) + (accept-process-output (lean-server-get-process) 0 50 t)) + (pcase lean-global-server-message-to-process + (`(SET ,pre ,body) + (lean-server-log "The following pre-message will be thrown away:") + (lean-server-log "%s" pre) + (setq lean-global-server-message-to-process nil) + (lean-server-log "We have the following response from lean-server") + (message "%s" (lean-set-parse-string body))) + (`(,type ,pre , body) + (lean-server-log "The following pre-message will be thrown away:") + (lean-server-log "%s" pre) + (lean-server-log "Something other than SET detected: %S" type) + (setq lean-global-server-message-to-process nil))))) + +(defun lean-option-read-bool (prompt) + (interactive) + (completing-read prompt'(("true" 1) ("false" 2)) nil t "" nil "true")) + +(defun lean-option-read-int (prompt) + (interactive) + (let* ((str (read-string prompt)) + (val (string-to-int str)) + tmp-str) + (setq tmp-str (int-to-string val)) + (if (and (integerp val) + (stringp tmp-str) + (string= tmp-str str)) + val + (error "%s is not an int value" str)))) + +(defun lean-option-read-uint (prompt) + (interactive) + (let* ((str (read-string prompt)) + (val (string-to-int str)) + tmp-str) + (setq tmp-str (int-to-string val)) + (if (and (integerp val) + (>= val 0) + (stringp tmp-str) + (string= tmp-str str)) + val + (error "%s is not an unsigned int value" str)))) + +(defun lean-option-read-double (prompt) + (interactive) + (let* ((str (read-string prompt)) + (val (string-to-number str)) + tmp-str) + (setq tmp-str (number-to-string val)) + (if (and (numberp val) + (>= val 0) + (stringp tmp-str) + (string= tmp-str str)) + (string-to-number str) + (error "%s is not a double value" str)))) + +(defun lean-option-read-string (prompt) + (interactive) + (read-string prompt)) + +(defun lean-option-read-sexp (prompt) + (interactive) + (let* ((str (read-string prompt)) + (sexp (ignore-errors (read str)))) + (if (ignore-errors + (string= (prin1-to-string sexp) str)) + sexp + (error "%s is not a well-formed S-Expression")))) + +(defun lean-option-type (option) + (let ((type-str (lean-option-record-type option))) + (cond ((string= "Bool" type-str) 'Bool) + ((string= "Int" type-str) 'Int) + ((string= "Unsigned Int" type-str) 'UInt) + ((string= "Double" type-str) 'Double) + ((string= "String" type-str) 'String) + ((string= "S-Expressions" type-str) 'SEXP) + (t (error "lean-option-string-to-type: %s is not supported lean-option type." + type-str))))) + +(defun lean-option-read (option) + (let* ((option-type-str (lean-option-record-type option)) + (option-name (lean-option-record-name option)) + (option-desc (lean-option-record-desc option)) + (prompt (format "%s [%s] : %s = " + option-name + option-desc + option-type-str))) + (pcase (lean-option-type option) + (`Bool (lean-option-read-bool prompt)) + (`Int (lean-option-read-int prompt)) + (`UInt (lean-option-read-uint prompt)) + (`Double (lean-option-read-double prompt)) + (`String (lean-option-read-string prompt)) + (`SEXP (lean-option-read-sexp prompt))))) + +(cl-defstruct lean-option-record name type default-value desc) +(defun lean-option-parse-string (line) + "Parse a line to lean-option-record" + (let* ((str-list (split-string line "|")) + (option-name (substring-no-properties (cl-first str-list) 3)) + (option-type (cl-second str-list)) + (option-default-value (cl-third str-list)) + (option-desc (cl-fourth str-list))) + (make-lean-option-record :name option-name + :type option-type + :default-value option-default-value + :desc option-desc))) + +(defun lean-options-parse-string (str) + "Parse lines of option string into an entry of alist of lean-option-records + +(NAME . OPTION-RECORD)." + (let ((str-list (split-string str "\n")) + str-str-list + option-list) + ;; Drop the first line "-- BEGINOPTIONS" and + ;; the last line "-- ENDOPTIONS" + (setq str-list + (-take (- (length str-list) 2) + (-drop 1 str-list))) + (-map (lambda (line) + (let ((option-record (lean-option-parse-string line))) + `(,(lean-option-record-name option-record) . ,option-record))) + str-list))) + +(defun lean-get-options () + "Get Lean option." + (interactive) + (unless lean-global-option-record-alist + (lean-server-send-cmd (lean-cmd-options)) + (while (not lean-global-server-message-to-process) + (accept-process-output (lean-server-get-process) 0 50 t)) + (pcase lean-global-server-message-to-process + (`(OPTIONS ,pre ,body) + (lean-server-log "The following pre-message will be thrown away:") + (lean-server-log "%s" pre) + (setq lean-global-server-message-to-process nil) + (lean-server-log "We have the following response from lean-server") + (setq lean-global-option-record-alist + (lean-options-parse-string body))) + (`(,type ,pre , body) + (lean-server-log "The following pre-message will be thrown away:") + (lean-server-log "%s" pre) + (lean-server-log "Something other than SET detected: %S" type) + (setq lean-global-server-message-to-process nil)))) + lean-global-option-record-alist) + +(provide 'lean-option) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 046924c8c..6fc93bef9 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -46,7 +46,9 @@ (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)) + ,(rx line-start (group "-- ENDEVAL") line-end)) + (OPTIONS ,(rx line-start "-- BEGINOPTIONS" line-end) + ,(rx line-start (group "-- ENDOPTIONS") 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") @@ -93,6 +95,8 @@ "Handle signals for lean-server-process" (cond ((string-prefix-p "hangup" event) + (lean-server-initialize-global-vars)) + ((string-prefix-p "killed" event) (lean-server-initialize-global-vars)))) ;; How to create an async process @@ -104,6 +108,7 @@ (setq lean-global-server-current-file-name nil) (setq lean-global-server-message-to-process nil) (setq lean-global-server-last-time-sent nil) + (setq lean-global-option-record-alist nil) (when (timerp lean-global-nay-retry-timer) (cancel-timer lean-global-nay-retry-timer)) (setq lean-global-nay-retry-timer nil)) @@ -195,9 +200,10 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. ('INSERT (lean-server-check-current-file)) ('REMOVE (lean-server-check-current-file)) ('INFO (lean-flush-changed-lines)) - ('CHECK ) + ('CHECK ()) ('SET ()) - ('EVAL (lean-server-check-current-file)))) + ('EVAL (lean-server-check-current-file)) + ('OPTIONS ()))) (defun lean-server-after-send-cmd (cmd) "Operations to perform after sending a command." @@ -210,7 +216,8 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. ('INFO ()) ('CHECK ()) ('SET ()) - ('EVAL ()))) + ('EVAL ()) + ('OPTIONS ()))) (defun lean-server-send-cmd (cmd) "Send string to lean-server." diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index 0d2de0828..9683457b2 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -14,7 +14,6 @@ (require 'lean-debug) (require 'flymake) - (defun lean-fill-placeholder () "Fill the placeholder with a synthesized expression by Lean." (interactive) @@ -51,39 +50,6 @@ (when info-string (message "%s" info-string)))))) -;; ======================================================= -;; set option -;; ======================================================= - -(defun lean-set-parse-string (str) - "Parse the output of eval command." - (let ((str-list (split-string str "\n"))) - ;; Drop the first line "-- BEGINSET" and - ;; the last line "-- ENDSET" - (setq str-list - (-take (- (length str-list) 2) - (-drop 1 str-list))) - (string-join str-list "\n"))) - -(defun lean-set-option (option-name option-value) - "Set Lean option." - (interactive "sOption Name: \nsOption Value: ") - (lean-server-send-cmd (lean-cmd-set option-name option-value)) - (while (not lean-global-server-message-to-process) - (accept-process-output (lean-server-get-process) 0 50 t)) - (pcase lean-global-server-message-to-process - (`(SET ,pre ,body) - (lean-server-log "The following pre-message will be thrown away:") - (lean-server-log "%s" pre) - (setq lean-global-server-message-to-process nil) - (lean-server-log "We have the following response from lean-server") - (message "%s" (lean-set-parse-string body))) - (`(,type ,pre , body) - (lean-server-log "The following pre-message will be thrown away:") - (lean-server-log "%s" pre) - (lean-server-log "Something other than SET detected: %S" type) - (setq lean-global-server-message-to-process nil)))) - ;; ======================================================= ;; eval ;; ======================================================= diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index 85549504f..a4414e9da 100644 --- a/src/emacs/lean-variable.el +++ b/src/emacs/lean-variable.el @@ -11,10 +11,13 @@ "A shared variable contains a received message to process. A message is in the form of (TYPE PRE BODY) -where TYPE := INFO | SET | EVAL | ERROR, +where TYPE := INFO | SET | EVAL | OPTIONS | ERROR, PRE is a server message comes before the message BODY is a body of the received message.") +(defvar lean-global-option-record-alist nil + "lean option-record alist") + (defvar lean-global-server-process nil "lean server process")