(defun dot () (point))

(defun spec-mode ()
"Major mode for editing RSL specifications.  The mode contains templates for
modules, objects, and operations.  It also has font-lock definitions for
colored syntax highlighting."
  (interactive)
; (my-latex-mode)
  (setq mode-name "SpecL")
  (setq major-mode 'SpecL mode)
  (local-set-key "O" 'insert-long-object-template)
  (local-set-key "P" 'insert-long-operation-template)
  (local-set-key "M" 'insert-long-module-template)
  (local-set-key "o" 'insert-short-object-template)
  (local-set-key "p" 'insert-short-operation-template)
  (local-set-key "m" 'insert-short-module-template)

  (local-set-key "	" 'rsl-complete-symbol)

  (local-unset-key "
")
  (local-unset-key "
")

  (make-local-variable 'comment-start)
  (setq comment-start "(*")
  (make-local-variable 'comment-end)
  (setq comment-end "*)")
  (make-local-variable 'comment-start-skip)
  (setq comment-start-skip "*")
  (make-local-variable 'font-lock-defaults)
  (setq font-lock-defaults
	'((rsl-font-lock-keywords
	   rsl-font-lock-keywords-1 rsl-font-lock-keywords-2)
	  nil nil ((?_ . "w") (?. . "w") (?< . ". 1") (?> . ". 4")) nil
	  )
  )
  (font-lock-mode t)
)

;; Regexps stollen and adapted from modula-2 mode.
(defconst rsl-font-lock-keywords-1
  '(
    ;;
    ;; Module definitions.
    ("\\<\\(INTERFACE\\|MODULE\\|PROCEDURE\\)\\>[ \t]*\\(\\sw+\\)?"
     (1 font-lock-keyword-face) (2 font-lock-function-name-face nil t))
    ;;
    ;; Import directives.
    ("\\<\\(EXPORTS\\|FROM\\|IMPORT\\)\\>"
     (1 font-lock-keyword-face)
     (font-lock-match-c-style-declaration-item-and-skip-to-next
      nil (goto-char (match-end 0))
      (1 font-lock-constant-face)))
    ;;
    ;; Pragmas as warnings.
    ;; Spencer Allain <sallain@teknowledge.com> says do them as comments...
    ;; ("<\\*.*\\*>" . font-lock-warning-face)
    ;; ... but instead we fontify the first word.
    ("<\\*[ \t]*\\(\\sw+\\)" 1 font-lock-warning-face prepend)
    )
  "Subdued level highlighting for Modula-3 modes.")

(defconst rsl-font-lock-keywords-2
  (append rsl-font-lock-keywords-1
   (eval-when-compile
     (let ((rsl-types
	    (regexp-opt
	     '("integer" "boolean" "real" "integer")))
	   (rsl-keywords
	    (regexp-opt
	     '("and" "ax" "axiom" "begin" "define" "else" "end" "exists"
               "export" "extends" "forall" "foreach" "from" "mfunc" "function"
               "if" "iff" "implies" "import" "in" "inherits" "is" "isa"
               "lambda" "let" "mod" "module" "not" "obj" "object" "op"
               "operation" "or" "return""then" "theorem" "thm" "val" "value"
               "var" "variable" "where" "while" "xor")))
	   (rsl-builtins
	    (regexp-opt
	     '("components" "dataflow" "description" "equations" "in"
	       "inputs" "out" "outputs" "operations" "post" "postcondition"
	       "pre" "precondition")))
	   )
       (list
	;;
	;; Keywords except those fontified elsewhere.
	(concat "\\<\\(" rsl-keywords "\\)\\>")
	;;
	;; Builtins.
	(cons (concat "\\<\\(" rsl-builtins "\\)\\>") 'font-lock-builtin-face)
	;;
	;; Type names.
	(cons (concat "\\<\\(" rsl-types "\\)\\>") 'font-lock-type-face)
	;;
	;; Fontify tokens as function names.
	'("\\<\\(END\\|EXCEPTION\\|RAISES?\\)\\>[ \t{]*"
	  (1 font-lock-keyword-face)
	  (font-lock-match-c-style-declaration-item-and-skip-to-next
	   nil (goto-char (match-end 0))
	   (1 font-lock-function-name-face)))
	;;
	;; Fontify constants as references.
	'("\\<\\(FALSE\\|NIL\\|NULL\\|TRUE\\)\\>" . font-lock-constant-face)
	))))
  "Gaudy level highlighting for Modula-3 modes.")

(defvar rsl-font-lock-keywords rsl-font-lock-keywords-1
  "Default expressions to highlight in Modula-3 modes.")

(defun insert-long-object-template ()
"Insert a long-form object template."
  (interactive)
  (setq cc (current-column))
  (setq cp (point))
  (insert-string
    "object <NAME> is\n")
  (setq name (read-string "Object Name: "))
  (add-name-to-object-completion-list name)
  (backward-word 1)
  (backward-char 1)
  (backward-kill-word 1)
  (backward-delete-char 1)
  (insert-string name)
  (next-line 1)
  (beginning-of-line)
  (insert-string
    "    components: ;\n"
;   "    operations: ;\n"
    "    description: (*\n        \n    *);\n"
  )
  (if (and (>= (length name) 6)
       (string= (substring name 0 5) "class"))
       (setq name (substring name 6 (length name)))
  )
  (if (setq sm (string-match "instance of" name))
      (setq name (substring name 0 (- sm 1)))
  )
  (if (= cc 2)		; Per new 2-space when-in-module rsl conventions
    (setq cp (point))
  )
  (insert-string
    "end " name ";\n\n"
  )
  (indent-rigidly cp (point) cc)
; (previous-line 6)
  (previous-line 4)
  (end-of-line)
  (backward-delete-char 1)
  (beginning-of-line)
  (previous-line 2)
  (forward-word 1)
  (forward-char 2)
)

(defun insert-long-operation-template ()
"Insert a long-form operation template."
  (interactive)
  (setq cc (current-column))
  (setq cp (point))
  (insert-string
    "operation <NAME> is\n")
  (setq name (read-string "Operation Name: "))
  (backward-word 1)
  (backward-char 1)
  (backward-kill-word 1)
  (backward-delete-char 1)
  (insert-string name)
  (next-line 1)
  (beginning-of-line)

  ;QUITE BIZARRE: The "    precondition: ; " line below loses one char before
  ;		  the newline.  Hence the space after the semicolon, this space
  ;		  being lost in the inserted string.  Hmm, this is very weird.
  (insert-string
    "    inputs: ;\n"
    "    outputs: ;\n"
    "    description: (*\n        \n    *);\n"
    "    precondition: ; \n"
    "    postcondition: ;\n"
  )
  (if (and (>= (length name) 6)
       (string= (substring name 0 5) "class"))
       (setq name (substring name 6 (length name)))
  )
  (if (setq sm (string-match "instance of" name))
      (setq name (substring name 0 (- sm 1)))
  )
  (if (= cc 2)		; Per new 2-space when-in-module rsl conventions
    (setq cp (point))
  )
  (insert-string
    "end " name ";\n\n"
  )
  (indent-rigidly cp (point) cc)
; (previous-line 6)
  (previous-line 4)
  (end-of-line)
  (backward-delete-char 1)
  (beginning-of-line)
  (previous-line 5)
  (forward-word 1)
  (forward-char 2)
)

(defun insert-short-object-template ()
"Insert a short-form object template."
  (interactive)
  (setq cc (current-column))
  (setq cp (point))
  (insert-string
    "object <NAME> is ;\n")
  (setq name (read-string "Object Name: "))
  (backward-word 1)
  (backward-char 1)
  (backward-kill-word 1)
  (backward-delete-char 1)
  (insert-string name)
  (forward-word 1)
  (forward-char 1)
)

(defun insert-short-operation-template ()
"Insert a short-form object template."
  (interactive)
  (setq cc (current-column))
  (setq cp (point))
  (insert-string
    "operation <NAME>()->();\n")
  (setq name (read-string "Operation Name: "))
  (backward-char 8)
  (backward-kill-word 1)
  (backward-delete-char 1)
  (insert-string name)
  (forward-char 1)
)


(defvar rsl-object-completions '())
(defun add-name-to-object-completion-list (name)
"Add the given NAME to the completion list of objects."
  (interactive)
  (setq rsl-object-completions
	(append rsl-object-completions (list name)))
  
)


(defun rsl-complete-symbol ()
"Display a list of object or operation completions."

  ; Most likely, this function will use emacs' all-completions function, q.v.


  ; The initilal version of this function had a CONTEXT arg, which was
  ; to be be one of 'obj, 'op', or 'mod."  I'm not sure what the
  ; thinking was there, but we'll presumably rethink it when this
  ; puppy get's implemented.

  (interactive))


(defun rsl-to-java-comment ()
"Run from the beginning of an RSL description block that ends in a blank line."
    (interactive)

    ; Unident
    (setq d (dot))
    (search-forward "\n\n")
    (previous-line 1)
    (indent-rigidly d (dot) -8)

    ; Add "/****\n *" to the front of the comment block.
    (goto-char d)
    (insert "/****\n *\n")

    ; Add " * " to the beginning of each line.
    (while (not (string= (buffer-substring (- (dot) 1) (+ (dot) 1)) "\n\n"))
        (insert " * ")
	(next-line 1)
	(beginning-of-line)
    )

    ; Rejustify the paragraph.
    (previous-line 1)
    (forward-char 3)
    (set-fill-prefix)
    (fill-paragraph nil)
    
    ; Stick " *\n ****/" on the end.
    (next-line 1)
    (insert " *\n ****/\n")
)

(defun rsl-to-java-method-comment ()
"Run from the beginning of an RSL description block that ends in a blank line."
    (interactive)

    ; Unident
    (setq d (dot))
    (search-forward "\n\n")
    (previous-line 1)
    (indent-rigidly d (dot) -8)

    ; Add "    /**\n" to the front of the comment block.
    (goto-char d)
    (insert "    /**\n")

    ; Add "     * " to the beginning of each line.
    (while (not (string= (buffer-substring (- (dot) 1) (+ (dot) 1)) "\n\n"))
        (insert "     * ")
	(next-line 1)
	(beginning-of-line)
    )

    ; Rejustify the paragraph.
    (previous-line 1)
    (forward-char 7)
    (set-fill-prefix)
    (fill-paragraph nil)
    
    ; Stick "     */" on the end.
    (next-line 1)
    (insert "     */\n")

    ; Delete the blank line that the unconverted comment block was required to 
    ; end with
    (delete-char 1)
)
(autoload 'spec-mode "spec-mode" "autoloaded" t)