Logs UI

docs/ui/emacs.rst

@@ -196,16 +196,15 @@ display goals while doing a proof. To display the result of ``compute``,
 instead of ``"%c %s"``.
 
 
-Customize goals buffer
-''''''''''''''''''''''
-The position and amount of space taken by the ``*Goals*`` buffer can be changed
-in the LambdaPi customization group (Do ``M-x customize-group lambdapi``).
-If the space is too small, then the window will open
-either on the right side or at the bottom, whichever is more suitable.
+Customize window layout
+'''''''''''''''''''''''
 
+The window layout can be customized in the LambdaPi customization group
+(Do ``M-x customize-group lambdapi``).
 The layout can be refreshed with ``C-c C-r``.
 
 
+
 Other relevant packages
 -----------------------
 

docs/ui/vscode.rst

@@ -147,4 +147,11 @@ Hover
 Hovering symbols provides their type. This feature is still
 experimental.
 
+Logs
+----
+
+Logs are displayed in a terminal which opens automatically
+when needed.
+
+
 .. _VSCode: https://code.visualstudio.com/

editors/emacs/lambdapi-mode.el

@@ -92,95 +92,75 @@
 (defvar lambdapi-current-line-number (line-number-at-pos))
 (defvar lambdapi-changed-line-hook nil)
 
+(defconst lambdapi--temp-buffer-name "lp-asdf2io3jnc"  ; any random name will work
+  "Buffer name for used by `lambdapi-refresh-window-layout'. Must
+not match any buffer used by user")
+
+
 (defun lambdapi-update-line-number ()
   (if interactive-goals
       (let ((new-line-number (line-number-at-pos)))
         (when (not (equal new-line-number lambdapi-current-line-number))
           (setq lambdapi-current-line-number new-line-number)
           (run-hooks 'changed-line-hook)))))
 
-
-(defgroup lambdapi nil
-  "LambdaPi is a proof assistant based on the λΠ-calculus modulo rewriting"
-  :group 'languages)
-
-(defcustom lambdapi-goals-window-side 'bottom
-  "Side at which to show goals window"
-  :type '(choice (const :tag "right"  right)
-                 (const :tag "left"   left)
-                 (const :tag "top"    top)
-                 (const :tag "bottom" bottom))
-  :group 'lambdapi)
-
-(defcustom lambdapi-goals-window-height-ratio 0.30
-  "Ratio of height taken by Goals window if split top or bottom"
-  :type '(float)
-  :group 'lambdapi)
-
-(defcustom lambdapi-goals-window-width-ratio 0.5
-  "Ratio of width taken by Goals window if split left or right"
-  :type '(float)
-  :group 'lambdapi)
-
-(defcustom lambdapi-goals-window-min-width 40
-  "Minimum width of Goals window"
-  :type '(integer)
-  :group 'lambdapi)
-
-(defcustom lambdapi-goals-window-min-height 4
-  "Minimum height of Goals window"
-  :type '(integer)
-  :group 'lambdapi)
-
+(defun lambdapi--apply-window-layout (tree)
+  "Applies the window configuration given by the argument tree,
+it is either a list (split-side ratio child1-tree child2-tree)
+or a leaf which is a buffer or a string with buffer's name.
+
+It is meant to be called by `lambdapi-refresh-window-layout'
+which also replaces buffers with name `lambdapi--temp-buffer-name'
+with the current buffer.
+
+Example:
+
+(lambdapi--apply-window-layout
+               '(h 0.6 \"proofs\" (v 0.3 \"goals\" \"logs\")))
+
+will produce
+
++------------+--------+
+|            | goals  |
+|   proofs   +--------+
+|            | logs   |
+|            |        |
++------------+--------+
+"
+  (if (not (listp tree))
+      (switch-to-buffer (eval tree) t t)
+    (let* ((way   (car tree))
+           (ratio  (eval (cadr tree)))
+           (child1 (caddr tree))
+           (child2 (cadddr tree))
+           curwin sibling)
+      (if (eq way 'h)
+          (progn
+            (split-window-horizontally
+             (truncate (* ratio (window-width))))
+            (setq curwin  (selected-window))
+            (setq sibling (next-window)))
+        (progn
+          (split-window-vertically
+           (truncate (* ratio (window-height))))
+          (setq curwin  (selected-window))
+          (setq sibling (next-window))))
+      (with-selected-window curwin
+        (lambdapi--apply-window-layout child1))
+      (with-selected-window sibling
+        (lambdapi--apply-window-layout child2)))))
 
 (defun lambdapi-refresh-window-layout ()
-  "Create *Goals* buffer if it is not present. Create a side window
-for the goals buffer using the lambdapi-goals-window-* variables."
+  "Resets the window layout to default."
   (interactive)
-  (let* ((goalsbuf (get-buffer-create "*Goals*"))
-	 (goalswindow (get-buffer-window goalsbuf))
-	 (gwin-height (truncate
-		       (* lambdapi-goals-window-height-ratio
-			  (frame-height))))
-	 (gwin-width (truncate
-		      (* lambdapi-goals-window-width-ratio
-			 (frame-width)))))
-    ;; Allocate window for *Goals* buffer
-    (if goalswindow
-	(delete-window goalswindow))
-    (setq goalswindow
-	  (display-buffer-in-side-window
-	   goalsbuf
-	   `((side . ,lambdapi-goals-window-side)
-	     (slot . nil)
-	     ,(pcase lambdapi-goals-window-side
-		((or 'right 'left)
-		 `(window-width . ,gwin-width))
-		((or 'top 'bottom)
-		 `(window-height . ,gwin-height))))))
-    ;; if goals window violated lambdapi-goals-window-min-*
-    ;; allocate a new window
-    (if (and goalswindow
-	     (< (window-width goalswindow)
-		lambdapi-goals-window-min-width))
-	(progn
-	  (delete-window goalswindow)
-	  (setq goalswindow
-		(display-buffer-in-side-window
-		 goalsbuf `((side . bottom)
-			    (slot . nil)
-			    (window-height . ,gwin-height))))))
-    (if (and goalswindow
-	     (< (window-height goalswindow)
-		lambdapi-goals-window-min-height))
-	(progn
-	  (delete-window goalswindow)
-	  (setq goalswindow
-		(display-buffer-in-side-window
-		 goalsbuf `((side . right)
-			    (slot . nil)
-			    (window-width . ,gwin-width))))))))
-
+  (let ((curbuf (current-buffer)))
+    (delete-other-windows)
+    (lambdapi--apply-window-layout lambdapi-window-layout)
+    (dolist (win (get-buffer-window-list lambdapi--temp-buffer-name))
+      (with-selected-window win
+        (switch-to-buffer curbuf t t)))
+    (kill-buffer lambdapi--temp-buffer-name)
+    (select-window (get-buffer-window curbuf))))
 
 (defvar lambdapi-mode-map nil "Keymap for `lambdapi-mode'")
 
@@ -195,6 +175,81 @@ for the goals buffer using the lambdapi-goals-window-* variables."
   (define-key lambdapi-mode-map (kbd "C-c C-b") #'lp-jump-proof-backward)
   (define-key lambdapi-mode-map (kbd "C-c C-r") #'lambdapi-refresh-window-layout))
 
+(defgroup lambdapi nil
+  "LambdaPi is a proof assistant based on the λΠ-calculus modulo rewriting"
+  :group 'languages)
+
+(defcustom lambdapi-window-X-ratio 0.5
+  "Ratio of height taken in horizontal split during window layout.
+(Not applicable to Layout 0)"
+  :type '(float)
+  :group 'lambdapi)
+
+(defcustom lambdapi-window-Y-ratio 0.8
+  "Ratio of width taken in vertical split during window layout
+(Not applicable to Layout 0)"
+  :type '(float)
+  :group 'lambdapi)
+
+(defcustom lambdapi-window-layout '(v 0.75
+                                      lambdapi--temp-buffer-name
+                                      (v 0.8 "*Goals*" "*lp-logs*"))
+  "Window layout of LambdaPi."
+  :group 'lambdapi
+  ;; :set might change window layout at an unexpected time
+  :set (lambda (option newval)
+         (setq lambdapi-window-layout newval)
+         (lambdapi-refresh-window-layout))
+  :type '(radio (sexp :tag "Layout 0"
+		      :format "%t\n"
+		      :value
+		      (v 0.75
+                         lambdapi--temp-buffer-name
+                         (v 0.8 "*Goals*" "*lp-logs*")))
+	        (sexp :tag "Layout 1"
+                      :format "%t\n"
+                      :value
+                      (v lambdapi-window-Y-ratio
+                         lambdapi--temp-buffer-name
+                         (h lambdapi-window-X-ratio
+			    "*Goals*" "*lp-logs*")))
+                (sexp :tag "Layout 2"
+                      :format "%t\n"
+                      :value
+                      (v lambdapi-window-Y-ratio
+                         (h lambdapi-window-X-ratio
+                            lambdapi--temp-buffer-name
+                            "*lp-logs*")
+                         "*Goals*"))
+                (sexp :tag "Layout 3"
+                      :format "%t\n"
+                      :value
+                      (h lambdapi-window-X-ratio
+                         lambdapi--temp-buffer-name
+                         (v lambdapi-window-Y-ratio
+                            "*lp-logs*"
+                            "*Goals*")))
+                (sexp :tag "Layout 4"
+                      :format "%t\n"
+                      :value
+                      (h lambdapi-window-X-ratio
+                         (v lambdapi-window-Y-ratio
+                            lambdapi--temp-buffer-name
+                            "*Goals*")
+                         "*lp-logs*"))
+                (sexp :tag "Goal bottom"
+                      :format "%t\n"
+                      :value
+                      (v lambdapi-window-Y-ratio
+                         lambdapi--temp-buffer-name
+                         "*Goals*"))
+                (sexp :tag "Goal right"
+                      :format "%t\n"
+                      :value
+                      (h lambdapi-window-X-ratio
+                         lambdapi--temp-buffer-name
+                         "*Goals*"))))
+
 
 ;; Main function creating the mode (lambdapi)
 ;;;###autoload

editors/emacs/lambdapi-proofs.el

@@ -117,6 +117,34 @@ make it clickable"
             (erase-buffer))
           (read-only-mode 1))))
 
+(defun lp-display-logs (logs)
+  "Display logs in *lp-logs* buffer"
+  (let ((logbuf (get-buffer-create "*lp-logs*")))
+    (with-current-buffer logbuf
+      (read-only-mode +1)
+      (with-silent-modifications
+        (set (make-local-variable 'window-point-insertion-type) t)
+	(erase-buffer)
+	(insert logs)
+        ;; TODO: fix performance issue
+        ;; See: https://emacs.stackexchange.com/a/38608/30239
+        (let ((ansi-color-apply-face-function
+               (lambda (beg end face)
+                 (when face
+                   (put-text-property beg end 'face face)))))
+          (ansi-color-apply-on-region (point-min) (point-max)))
+        ;;; remove whitespace at end of buffer
+        (goto-char (point-max))
+        (while (member (char-before) '(?  ?\C-j ?\C-i))
+          (delete-backward-char 1))))
+    (let ((logwin (get-buffer-window logbuf)))
+      (if logwin
+          (with-selected-window logwin
+            (goto-char (point-max))
+            (beginning-of-line)
+            (recenter -1))))))
+
+
 (defun eglot--signal-proof/goals (position)
   "Send proof/goals to server, requesting the list of goals at POSITION."
   (let ((server (eglot-current-server))
@@ -125,9 +153,16 @@ make it clickable"
     (if server
         (let ((response (jsonrpc-request server :proof/goals params)))
           (if response
-              (display-goals (plist-get response :goals))
-            (let ((goalsbuf (get-buffer-create "*Goals*")))
+              (progn
+		(display-goals (plist-get response :goals))
+		(lp-display-logs (plist-get response :logs)))
+            (let ((goalsbuf (get-buffer-create "*Goals*"))
+                  (logsbuf (get-buffer-create "*lp-logs*")))
               (with-current-buffer goalsbuf
+                (read-only-mode -1)
+                (erase-buffer)
+                (read-only-mode 1))
+              (with-current-buffer logsbuf
                 (read-only-mode -1)
                 (erase-buffer)
                 (read-only-mode 1))))))))
@@ -177,25 +212,21 @@ make it clickable"
 (defun lp-jump-proof-forward ()
   "Move the proof cursor to the next proof"
   (interactive)
-  (setq interactive-goals t)
   (move-proof-line #'lp-get-next-proof-line))
 
 (defun lp-jump-proof-backward ()
   "Move the proof cursor to the previous proof"
   (interactive)
-  (setq interactive-goals t)
   (move-proof-line #'lp-get-prev-proof-line))
 
 (defun lp-proof-forward ()
   "Move the proof cursor forward."
   (interactive)
-  (setq interactive-goals t)
   (move-proof-line #'1+))
 
 (defun lp-proof-backward ()
   "Move the proof cursor backward."
   (interactive)
-  (setq interactive-goals t)
   (move-proof-line #'1-))
 
 (defun toggle-interactive-goals ()
@@ -213,7 +244,9 @@ make it clickable"
               (hlt-highlight-region 0 (1+ (line-end-position)))
               (lp-display-goals))
         (goto-line line)
-        (hlt-unhighlight-region 0 (point-max))))))
+        (hlt-unhighlight-region 0 (point-max)))))
+  (message (format "Interactive mode is %s"
+                   (if interactive-goals "ON" "OFF"))))
 
 (provide 'lambdapi-proofs)
 ;;; lambdapi-proofs.el ends here