;; Copyright (C) 2019  Christian Barthel <bch@online.de>

 ;; 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)