Emacs/VSCode: Interactive mode (Deducteam#564)

- Electric mode for Emacs
- Buttons for Proof Navigation in Emacs
- Navigate by commands/tactics in Emacs and VScode
- Evaluated region shrinks on edit in Emacs and VScode
- Evaluated region changes colour after error in Emacs and VScode
- LSP server sends logs only from last command/tactic
- Few minor corrections in LSP server
- Improve VSCode indentation
- Fixes Deducteam#519
- Fixes Deducteam#515
- Fixes Deducteam#514
- Fixes Deducteam#513

Author: firewall2142

.dir-locals.el

@@ -1,2 +1,3 @@
 ((nil . ((sort-fold-case . t) ; Ignore case when sorting
-         )))
+	))
+ (emacs-lisp-mode . ((indent-tabs-mode . nil))))

.gitignore

@@ -20,3 +20,4 @@ libraries/zenon_modulo
 *.png
 .DS_Store
 *.map
+TODO.*

docs/ui/emacs.rst

@@ -7,14 +7,31 @@ Emacs
 Lambdapi source code can be edited with the `emacs`_ editor with the major
 mode ``lambdapi-mode``. It requires Emacs 26.1 or higher and provides:
 
-* Syntax highlighting for Lambdapi (``*.lp`` files) and Dedukti2 (``*.dk``
-  files)
+* Syntax highlighting for Lambdapi (``*.lp`` files) and Dedukti (``*.dk`` files)
 * Auto indentation for Lambdapi
 * Easier unicode input
 * Completion for Lambdapi
 * Typing of symbol at point (in minibuffer)
 * Type checking declarations
 
+List of short-cuts
+------------------
+
+* ``C-c C-c``: jump to cursor position
+* ``C-c C-n`` or button "Next": next tactic or command
+* ``C-c C-p`` or button "Prev": previous tactic or command
+* ``C-c C-f``: next proof
+* ``C-c C-b``: previous proof
+* ``C-c C-e``: toggle electric mode
+* ``M-;``    : (un)comment region
+* ``C-x RET C-\``: enter unicode characters in minibuffer using LaTeX
+* ``M-x customize-group lambdapi``: customize window layout
+* ``C-c C-r``: refresh window layout
+* Click on a symbol to discover its type in the bottom line
+
+As always with emacs, if you were to be dissatisfied with these
+keybindings, you can change them easily!
+
 Installation
 ------------
 
@@ -99,8 +116,9 @@ Usage
 Commenting regions
 ^^^^^^^^^^^^^^^^^^
 
-Lambdapi handles only single-line comments with ``//``. To comment a
-region in Emacs, select it and use ``M-;``.
+Lambdapi handles single-line and multi-line comments with ``//`` and 
+``/* ... */`` respectively. To comment a region in Emacs, select it and use
+``M-;``.
 
 Entering unicode
 ^^^^^^^^^^^^^^^^
@@ -156,45 +174,38 @@ LSP server
 Navigating goals
 ''''''''''''''''
 
-On lambdapi-mode startup, a window showing the goals at the current line
-is open.
-
-You can toggle the interactive mode with ``C-c C-i``. If you were to do
-so, you still can navigate the proofs with ``C-c C-p`` and ``C-c C-n``,
-jump between proofs with ``C-c C-b`` and ``C-c C-f``, and show the goals
-at the current line with ``C-c C-c``. As always with emacs, if you were
-to be dissatisfied with these keybindings, you can change them easily!
+On lambdapi-mode startup, the window is split into three buffers:
 
-Clicking on the ``i``-th goal of the ``*Goals*`` buffer puts the focus on it
-by inserting a ``focus i`` tactic in the proof script.
+* the top buffer contains the Lambdapi file,
+* the middle ``*Goals*`` buffer is where goals are displayed,
+* the bottom ``*lp-logs*`` buffer is where Lambdapi messages are displayed.
 
-CPU usage and deactivation
-''''''''''''''''''''''''''
-
-If for any reason the LSP server consumes too much power (e.g. if a
-non-terminating rewrite system is edited), it can be disabled with
-``M-x eglot-shutdown``.
+It is possible to print the goals to solve at some point in the file by
+using the following sort-cuts or the navigation buttons "Prev" and "Next":
 
-Pseudo interactive proof mode
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+* ``C-c C-c``: jump to cursor position
+* ``C-c C-n`` or button "Next": next tactic or command
+* ``C-c C-p`` or button "Prev": previous tactic or command
+* ``C-c C-f``: next proof
+* ``C-c C-b``: previous proof
 
-One can use `quickrun`_ to call lambdapi while editing a buffer. It can be
-configured for lambdapi with
+The part of the file up to the current goal is displayed with a green
+background. In case of error, the background gets red. If an edition
+occurs in the green zone, the green zone is automatically shrinked and
+the goals buffer updated.
 
-.. code:: emacs-lisp
+It is possible to make the green zone expand automatically each time a
+new command is typed by toggling the electric mode with ``C-c C-e``.
 
-   (quickrun-add-command "lambdapi"
-     '((:command . "lambdapi check")
-       (:exec    . ("%c %s")))
-     :mode 'lambdapi-mode)
-   (add-hook 'lambdapi-mode-hook
-     (lambda () (define-key lambdapi-mode-map (kbd "C-c r") #'quickrun)))
+Clicking on the ``i``-th goal of the ``*Goals*`` buffer puts the focus
+on it by inserting a ``focus i`` tactic in the proof script.
 
-to run lambdapi on the edited buffer with ``C-c r``. It can be used to
-display goals while doing a proof. To display the result of ``compute``,
-``type``, and simlar commmand as well, write ``"%c --verbose 1 %s"``
-instead of ``"%c %s"``.
+Electric Terminator mode
+''''''''''''''''''''''''
 
+You can toggle electric terminators either from the toolbar or
+using ``C-c C-e``. This will evaluate the region till the
+cursor whenever you type the ``;`` terminator or ``begin``.
 
 Customize window layout
 '''''''''''''''''''''''
@@ -203,7 +214,12 @@ 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``.
 
+CPU usage and deactivation
+''''''''''''''''''''''''''
 
+If for any reason the LSP server consumes too much power (e.g. if a
+non-terminating rewrite system is edited), it can be disabled with
+``M-x eglot-shutdown``.
 
 Other relevant packages
 -----------------------

editors/emacs/lambdapi-layout.el

@@ -0,0 +1,135 @@
+(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--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 ()
+  "Resets the window layout to default."
+  (interactive)
+  (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))))
+
+(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.75 "*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*"))))
+
+
+(provide 'lambdapi-layout)