Skip to content
Snippets Groups Projects
Commit 9f3c5ac9 authored by gabrielhdt's avatar gabrielhdt
Browse files

no dirs local, requirements

parent f85e3343
No related branches found
No related tags found
No related merge requests found
;;; Directory Local Variables
;;; For more information see (info "(emacs) Directory Variables")
((lambdapi-mode
(eval define-abbrev local-abbrev-table "subtype" "⊑" nil :system t)))
......@@ -13,8 +13,8 @@ library, also known as _Prelude_. The prelude is available
## Requirements
- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `heavy-let`
branch
[`lambdapi`](https://github.com/Deducteam/lambdapi.git) later than
fda8752584af52cdc8158a7a80bbe7fce5720616
## Structure
- `adlib` contains additional libraries not in the prelude
......@@ -23,46 +23,4 @@ library, also known as _Prelude_. The prelude is available
- `prelude` contains parts of the PVS prelude
- `sandbox` contains miscellaneous experiments
- `tools` contains some additional scripts and utilities
- `alternativs` contains files in other encodings
## Emacs abbreviations
The `.dir-locals.el` activates the `abbrev-mode` when opening a Dedukti file,
and calls a `set-local-abbrevs` function.
The
[`abbrev-mode`](https://www.gnu.org/software/emacs/manual/html_node/emacs/Abbrevs.html)
is used to expand some defined character sequences into longer words.
The typical example is to expand `btw` to `by the way`.
The function `set-local-abbrevs` is not built in emacs and
allows to define abbreviation locally to a loaded file,
otherwise, abbreviations would be saved and activated for all
Dedukti buffers. The function takes as argument a list of abbreviations.
The code of `set-local-abbrevs` comes from
<https://stackoverflow.com/questions/21836527/abbrev-local-to-document-in-emacs>
``` emacs-lisp
(defun set-local-abbrevs (abbrevs)
"Add ABBREVS to `local-abbrev-table' and make it buffer local.
ABBREVS should be a list of abbrevs as passed to `define-abbrev-table'.
The `local-abbrev-table' will be replaced by a copy with the new
abbrevs added, so that it is not the same as the abbrev table used
in other buffers with the same `major-mode'."
(let* ((bufname (buffer-name))
(prefix (substring (md5 bufname) 0 (length bufname)))
(tblsym (intern (concat prefix "-abbrev-table"))))
(set tblsym (copy-abbrev-table local-abbrev-table))
(dolist (abbrev abbrevs)
(define-abbrev (eval tblsym)
(car abbrev)
(cadr abbrev)
(caddr abbrev)))
(setq-local local-abbrev-table (eval tblsym))))
```
And we define the following abbreviations,
| Key sequence | Expansion |
|:-------------|----------:|
| subtype | ⊑ |
| upcast | ↑ |
| downcast | ↓ |
- `alternatives` contains files in other encodings
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment