From e802883b031415f13f79c912c0005b3ebbc20932 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 3 Sep 2014 08:08:28 -0700 Subject: [PATCH] feat(emacs/lean-option): show the current value of an option close #125 --- src/emacs/lean-option.el | 50 +++++++++++++++++++++++--------------- src/emacs/lean-server.el | 3 ++- src/emacs/lean-type.el | 3 +-- src/emacs/lean-variable.el | 3 --- 4 files changed, 33 insertions(+), 26 deletions(-) diff --git a/src/emacs/lean-option.el b/src/emacs/lean-option.el index 7f9c044f5..a6e585b6d 100644 --- a/src/emacs/lean-option.el +++ b/src/emacs/lean-option.el @@ -1,6 +1,15 @@ +;; -*- lexical-binding: t; -*- +;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. +;; Released under Apache 2.0 license as described in the file LICENSE. +;; +;; Author: Soonho Kong +;; + (require 'dash) (require 'dash-functional) +(cl-defstruct lean-option-record name type value desc) + (defun lean-set-parse-string (str) "Parse the output of eval command." (let ((str-list (split-string str "\n"))) @@ -11,19 +20,21 @@ (-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)) +(defun lean-set-option-cont (option-record-alist) + (let* ((key-list (-map 'car 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 (cdr (assoc option-name option-record-alist))) (option-value (lean-option-read option))) (lean-server-send-cmd (lean-cmd-set option-name option-value) 'message))) +(defun lean-set-option () + "Set Lean option." + (interactive) + (lean-get-options 'lean-set-option-cont)) + (defun lean-option-read-bool (prompt) (interactive) (completing-read prompt'(("true" 1) ("false" 2)) nil t "" nil "true")) @@ -92,12 +103,14 @@ (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 (lean-option-record-name option)) + (option-desc (lean-option-record-desc option)) + (option-value (lean-option-record-value option)) + (prompt (format "%s [%s] : %s (%s) = " option-name option-desc - option-type-str))) + option-type-str + option-value))) (pcase (lean-option-type option) (`Bool (lean-option-read-bool prompt)) (`Int (lean-option-read-int prompt)) @@ -106,17 +119,16 @@ (`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-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 + :value option-value :desc option-desc))) (defun lean-options-parse-string (str) @@ -136,13 +148,11 @@ `(,(lean-option-record-name option-record) . ,option-record))) str-list))) -(defun lean-get-options () +(defun lean-get-options (cont) "Get Lean option." (interactive) - (unless lean-global-option-record-alist - (lean-server-send-cmd (lean-cmd-options) - '(lambda (option-record-alist) - (setq lean-global-option-record-alist - option-record-alist))))) - + (lean-server-send-cmd (lean-cmd-options) + (lambda (option-record-alist) + (when cont + (funcall cont option-record-alist))))) (provide 'lean-option) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index bf6b7c020..b630a5490 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -103,7 +103,6 @@ (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-retry-timer) (cancel-timer lean-global-retry-timer)) (setq lean-global-retry-timer nil)) @@ -288,6 +287,7 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (lean-server-log "The following pre-message will be thrown away:") (lean-server-log "%s" pre) (setq lean-global-server-buffer post) + (message "lean-server-event-handler: %S" type) (cl-case type (INFO (let ((info-record (lean-server-get-info-record-at-pos body))) @@ -302,6 +302,7 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd. (EVAL (funcall cont (lean-eval-parse-string body))) (OPTIONS + (message "handle options") (funcall cont (lean-options-parse-string body))) (SHOW (funcall cont (lean-show-parse-string body))) diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el index a590c4362..424f4063e 100644 --- a/src/emacs/lean-type.el +++ b/src/emacs/lean-type.el @@ -1,3 +1,4 @@ +;; -*- lexical-binding: t; -*- ;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. ;; Released under Apache 2.0 license as described in the file LICENSE. ;; @@ -14,8 +15,6 @@ (require 'lean-debug) (require 'flymake) -(setq-local lexical-binding t) - (defun lean-fill-placeholder-cont (info-record) "Continuation for lean-fill-placeholder" (let ((synth (and info-record (cl-first (lean-info-record-synth info-record))))) diff --git a/src/emacs/lean-variable.el b/src/emacs/lean-variable.el index 5e008f0c9..1d62f39e6 100644 --- a/src/emacs/lean-variable.el +++ b/src/emacs/lean-variable.el @@ -15,9 +15,6 @@ 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.") -(defvar lean-global-option-record-alist nil - "lean option-record alist") - (defvar lean-global-server-process nil "lean server process")