From 2e6a2c6a097588279322021aedcf1fd6f74ce92f Mon Sep 17 00:00:00 2001 From: Christian Barthel Date: Thu, 19 Dec 2019 23:39:50 +0100 Subject: [PATCH] first defintions for a new TLA+ mode goal is to implement a convenient mode to read and write TLA+ specifications. This commit adds the first few functions to - create a new module - run SANY on a TLA+ module - run TLaTeX export and create DVI file format - some bascic font-highlighting - comments can be created --- tla+-mode.el | 173 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 173 insertions(+) create mode 100644 tla+-mode.el diff --git a/tla+-mode.el b/tla+-mode.el new file mode 100644 index 0000000..faa1caf --- /dev/null +++ b/tla+-mode.el @@ -0,0 +1,173 @@ + ;; Copyright (C) 2019 Christian Barthel + + ;; Author: Christian Barthel + ;; Keywords: TLA+ + + ;; This file is free software; you can redistribute it and/or modify + ;; it under the terms of the GNU General Public License as published by + ;; the Free Software Foundation; either version 2, or (at your option) + ;; any later version. + + ;; This file is distributed in the hope that it will be useful, + ;; but WITHOUT ANY WARRANTY; without even the implied warranty of + ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + ;; GNU General Public License for more details. + + ;; You should have received a copy of the GNU General Public License + ;; along with GNU Emacs; see the file COPYING. If not, write to + ;; the Free Software Foundation, Inc., 59 Temple Place - Suite 330, + ;; Boston, MA 02111-1307, USA. + + ;;; Commentary: + + ;; + + ;;; Code: + +(defcustom tla+-mode-hook '() + "Normal hook run when entering TLA+ mode." + :type 'hook + :options '() + :group 'tla+) + +(defcustom tla+-java-path "/usr/local/bin/java" + "Path to the `java' program" + :type 'file + :group 'tla+) + +(defcustom tla+-tlatools-path + "/usr/home/bch/tmp/tlaplus/tlatools/dist/tla2tools.jar" + "Path to the TLA+ `tlatools.jar' file" + :type 'file + :group 'tla+) + + + +(defvar tla+-mode-map + (let + ((map (make-sparse-keymap)) + (menu-map (make-sparse-keymap "TLA+")) + (export-map (make-sparse-keymap))) + (set-keymap-parent map lisp-mode-shared-map) + (define-key map "\e\t" 'ispell-complete-word) + + ;; Main TLA+ Menu: + (bindings--define-key map [menu-bar tla+] + (cons "TLA+" menu-map)) + + ;; Export Menu: + (bindings--define-key menu-map [export] (cons "Export.." export-map)) + + (bindings--define-key export-map [export-pdf] + '(menu-item "Run TLatex and create PDF" tla+-run-tlatex-pdf + :help "Typeset TLaTex and create PDF Document")) + + (bindings--define-key export-map [export-dvi] + '(menu-item "Run TLatex and create DVI" tla+-run-tlatex-dvi + :help "Typeset TLaTex and create DVI Document")) + + (bindings--define-key export-map [export-ps] + '(menu-item "Run TLatex and create PS" tla+-run-tlatex-ps + :help "Typeset TLaTex and create PS Document")) + + (bindings--define-key export-map [export-open] + '(menu-item "Open DVI Viewer" tla+-run-tlatex-ps + :help "Open DVI Viewer")) + + ;; Main Menu + (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator) + + (bindings--define-key map [menu-bar tla+ tla+-run-sany] + '(menu-item "Run Syntax Checker" tla+-run-sany + :help + "Run SANY2 " + "(parser and syntax checker for TLA+ specifications.) ")) + + (bindings--define-key map [menu-bar tla+ tla+-create-module] + '(menu-item "Create new Module" tla+-create-module + :help "Create a new TLA+ Module")) + (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator) + map) + "Keymap for `tla+-mode'.") + + +(defconst tla+-font-lock-keywords + (list + '("\\<\\(MODULE\\|VARIABLE\\|EXTENDS\\)\\>" . font-lock-builtin-face) + '("\\\\\\*.*$" . font-lock-comment-face) + '("(\\*.*\\*)" . font-lock-comment-face) + '("\\('\\w*'\\)" . font-lock-variable-name-face) + "Highlighting for TLA+ Keywords.")) + + +;;;###autoload (add-to-list 'auto-mode-alist '("\\.tla\\'" . tla+-mode)) +;;;###autoload +(define-derived-mode tla+-mode nil "TLA+" + "Major mode for editing text written for humans to read. +In this mode, paragraphs are delimited only by blank or white lines. +You can thus get the full benefit of adaptive filling + (see the variable `adaptive-fill-mode'). +\\{text-mode-map} +Turning on Text mode runs the normal hook `text-mode-hook'." + (setq-local font-lock-defaults + '(tla+-font-lock-keywords)) + (setq-local text-mode-variant t) + (setq-local comment-start "\\* ") + (setq-local require-final-newline mode-require-final-newline)) + +(defun tla+-create-module () + (interactive) + (insert + (concat + "------------------- MODULE ......... -----------------------\n" + "EXTENDS Naturals, ...\n" + "VARIABLE ..\n" + "------------------------------------------------------------\n" + "============================================================\n" + "\\* Modification History\n" + "\\* Created " (current-time-string) " by " user-full-name "\n"))) + + +(defun tla+-run-sany () + "TODO: jump to line.." + (interactive) + (let* ((filename (buffer-file-name)) + (sanybuffer (get-buffer-create "*tla2sany.SANY*")) + (output (shell-command-to-string (concat + tla+-java-path + " -cp " + tla+-tlatools-path + " tla2sany.SANY " + filename)))) + (save-excursion + (split-window-below) + (other-window 1) + (switch-to-buffer sanybuffer) + (insert output)))) + +(defun tla+-run-tlatex (type) + "TODO: jump to line.." + (interactive + (list + (completing-read + "Format: " + '(("pdf" 1) ("dvi" 2) ("ps" 3)) nil t ""))) + (let* ((filename (buffer-file-name)) + (output (shell-command (concat + tla+-java-path + " -cp " + tla+-tlatools-path + " tla2tex.TLA " + filename)))) + (message (concat type)))) +;; (save-excursion +;; (split-window-below) +;; (other-window 1) +;; (switch-to-buffer sanybuffer) +;; (insert output)))) + +(defun tla+-run-tlatex-pdf () (tla+-run-tlatex "pdf")) +(defun tla+-run-tlatex-dvi () (tla+-run-tlatex "dvi")) +(defun tla+-run-tlatex-ps () (tla+-run-tlatex "ps")) + +(provide 'tla+-mode)