;;; Major mode for editing formal source in Emacs
;;
;; This file is not part of XEmacs.
;;
;; (C) Copyright IBM Corp. 2002-2003
;;
;; Author: Irit Shitsevalov (aka irits)
;; Modifications: By Eli Bendersky (eliben), in June 2003 - supports Sugar/PSL (Sugar 2)
;; Keywords: languages

;; USAGE
;; =====

;; This file is supposed to work in Xemacs and Emacs version grater that 20.
;; I used it in Xemacs version 20.3.
;; Emacs should enter Formal mode when you find a Formal source file.
;; When you have entered Formal mode, you may get more info by pressing
;; C-h m. You may also get online help describing various functions by:
;; C-h f 

;; STEP-BY-STEP INSTALLATION:
                             
;; To use Formal mode, change your .emacs file as follows:
;;
;; 1) To load Formal library, add to your .emacs file the 3 following lines:
;;    1.a) one of 
;          (setq load-path (cons "~/.emacs-settings" load-path))
;;         where ~/.emacs-settings is a directory containing formal-mode.el file
;;         (this file)
;;    1.b)
;          (load-library "formal-mode")
;;    1.c)
;          (autoload 'formal-mode "formal-mode" nil t)
;; 2) If you do not have it yet in your .emacs file, add
;          (require 'font-lock)


;; Now you can call Formal mode either automatically (when you open formal files)
;; or non-automatically (by calling formal mode explicitly).
;; Note: You can see current mode (or modes) name in the (X)Emacs modeline
;;       in the bottom of (X)Emacs window. If you are viewing this file in (X)Emacs,
;;       you most probably see (Emacs-Lisp ....) in the modeline just now.

;; 3)To call Formal mode automatically, add to your .emacs the following code:
;  (setq auto-mode-alist
;      (append '(
;		("\\.edl\\'" . formal-mode)     ;; for files *.edl
;		("\\(\\`\\|/\\)checker" . formal-mode)        ;; for files checker*
;		("\\(\\`\\|/\\)envs[.]*" . formal-mode)       ;; for files envs*        
;		("\\(\\`\\|/\\)rule[s]?" formal-mode t))      ;; for files rules*
;	      auto-mode-alist))
;; assuming your formal files are called *.edl, envs*, rule*.

;; 3) To call Formal mode not automatically (to try it):
;;      3.a) Open a file with Formal code or swith to buffer with such file.
;;      3.2) Type M-x formal-mode .

;; HIGHLIGHTING EXPLANATION
;; Formal mode use Font-Lock minor mode for highlighting.
;; If you use Font-Lock mode already skip to  HIGHLIGHTING CUSTOMIZATION.
;; Check modeline:
;;    if you can see the word 'Font' there then you are currently using Font-Lock mode.
;; 
;; If you enter Formal mode AND you did not like the colors,
;; you can set colors used by Font-Lock in your .emacs file.
;; Each version of (X)emacs has its own set of faces Font-Lock use.
;; For example, these are my "pastel" settings (work for Xemacs 20.3): 
;(set-face-foreground 'font-lock-comment-face       "red")      
;(set-face-background 'font-lock-comment-face       "ivory")
;(set-face-foreground 'font-lock-doc-string-face    "deeppink") 
;(set-face-foreground 'font-lock-function-name-face "darkviolet")  
;(set-face-foreground 'font-lock-keyword-face       "DarkGoldenrod")     
;(set-face-foreground 'font-lock-preprocessor-face  "blue3")  
;(set-face-background 'font-lock-preprocessor-face  "honeydew")
;(set-face-foreground 'font-lock-reference-face     "sienna")  
;(set-face-foreground 'font-lock-string-face        "darkgreen")      
;(set-face-foreground 'font-lock-type-face          "mediumblue")     
;(set-face-foreground 'font-lock-variable-name-face "violetred")


;; HIGHLIGHTING customization
;; There are 2 levels of decoration (more or less of text is highlighted).
;; In Xemacs you can change them in Options ->Syntax Hightlighting -> Least/Most.
;;           Don't forget Options -> Save Options after this!

;; CUSTOMIZATION of Formal mode
;; If you want to customize Formal mode to fit you better,
;; you may add to your .emacs file those lines:
;; (the values of the variables presented here are the defaults):
;;
;; ;; User customization for Formal mode
;; (setq  formal-tab-indent            (default t)
;;        formal-tab-indent-in-comment (default nil)
;;        formal-tabulated-colon       (default nil)
;;        formal-indent-level          (default 2)
;;        formal-indent-level-big      (default 6)
;;        formal-indent-colon-in-declaration-level (default 24)
;;        formal-indent-colon-in-case-level        (default 15)
;;        formal-indent-tabulated-colon-level      (default 72)
;;        formal-indent--comment-small (default 48)
;;        formal-indent--comment-big   (default 64)
;;        formal-indent-sugar          (default 2)
;;        formal-auto-newline          (default nil))

;; KNOWN BUGS / BUGREPORTS
;; =======================
;; As far as I know, there is at least one bug in any non trivial program
;; I believe this program is not trivial.
;; Please send bug reports with detailed information on bug and your Emacs version.
;; Bug reports and suggestions about Formal mode features
;; will be cindly apreciated.
;; Send bug reports to irits@il.ibm.com or eliben@il.ibm.com

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun current-point ()
  "Return current point. Do nothing. Written for easy debugging."
  (interactive)
  (message "Current point %d" (point)))

(defun second (list)
  "Try for emacs, without cl.elc library"
  (car (cdr list)))
  
(defconst formal-mode-version "0.2"
  "Version of `formal.el'.")

(defvar formal-mode-abbrev-table nil
  "Abbrev table in use in Formal-mode buffers.")
(define-abbrev-table 'formal-mode-abbrev-table ())

(defun dont-panic ()
  "Advice to Formal user"
  (interactive)
  (message "Don't panic!"))

(defvar formal-mode-popup-menu nil)
(defvar formal-mode-popup-menu-1
  (purecopy '("Formal"
	      ["Mark Function"               formal-mark-defun t]
	      ["Go to beginning of function" formal-beg-of-defun t]
	      ["Go to end of function"       formal-end-of-defun t]
	      "---"
	      ["Comment Region"   comment-region (region-exists-p)]
	      ["Uncomment Region" uncomment-region (region-exists-p)]
	      ["Indent Region"    formal-indent-region (region-exists-p)]
	      ;;["Indent Line"      formal-indent-line t] - not interactive
	      "---"
	      ["Advice"            dont-panic t]
	      ["If you desperate!" doctor t]
	      )))	    
;(defvar formal-mode-menubar-menu nil)
;(defvar formal-mode-menubar-menu-1
;  (purecopy (cons "Frml" (cdr formal-mode-popup-menu-1))))

(defvar formal-mode-map ()
  "Keymap used in Formal mode.")
(if formal-mode-map
    ()
  (setq formal-mode-map (make-sparse-keymap))
  (define-key formal-mode-map ";"        'electric-formal-semi)
 ; (define-key formal-mode-map ":"        'electric-formal-colon)
  (define-key formal-mode-map "}"        'electric-formal-close-brace)
  (define-key formal-mode-map ")"        'electric-formal-close-brace)
  (define-key formal-mode-map "-"        'electric-formal--comment)
  (define-key formal-mode-map "#"        'electric-formal-hash)
  (define-key formal-mode-map "\r"       'electric-formal-terminate-line)
  (define-key formal-mode-map "\t"       'electric-formal-tab)
;  (define-key formal-mode-map "\M-\t"    'formal-complete-word)
;  (define-key formal-mode-map "\M-?"     'formal-show-completions)
  (define-key formal-mode-map "\M-\C-h"  'formal-mark-defun)
  ;comment-region and kill comment are working
;  (define-key formal-mode-map "\C-c\C-c" 'formal-comment-area)    
;  (define-key formal-mode-map "\C-c\C-u" 'formal-uncomment-area)
  
  (define-key formal-mode-map "\M-\C-a"  'formal-beg-of-defun)
  (define-key formal-mode-map "\M-\C-e"  'formal-end-of-defun)
;  (define-key formal-mode-map "\C-c\C-d" 'formal-goto-defun)
;  (define-key formal-mode-map "\C-c\C-o" 'formal-outline)
;; A command to change the whole buffer won't be used terribly
;; often, so no need for a key binding.
;  (define-key formal-mode-map "\C-cd"    'formal-downcase-keywords)
;  (define-key formal-mode-map "\C-cu"    'formal-upcase-keywords)
;  (define-key formal-mode-map "\C-cc"    'formal-capitalize-keywords)
  )

;(defvar formal-imenu-generic-expression
;  '("^[ \t]*\\(function\\|procedure\\)[ \t\n]+\\([a-zA-Z0-9_.:]+\\)" . (2))
;  "Imenu expression for Formal-mode.  See `imenu-generic-expression'.")

(defvar formal-keywords
  '( "always" "ASSIGN" "DEFINE" "FAIRNESS" "VAR"
     "assign" "boolean" "bvtoi" "define" "envs" "eventually" "fairness" "fell" "formula" "formulas"
     "init" "instance" "itobv" "mode" "module" "never" "next" "nondets" "ones" "process"
     "rep" "rose" "rule" "test_pins" "union" "var" "zeroes" "case" "else" "endif" "esac" "if" "then"
     "AG" "AX" "AF" "A" "E" "U" "W" "G" "F" "X" "EG" "EX" "EF" "ABG" "ABF"
     "assert" "vunit" "vprop" "vmode"
     "until" "until!" "until_" "until!_"
     "before" "before!" "before_" "before!_"
     "next_event" "next_event!" "within" "within!" "whilenot" "whilenot"))

;;;
;;; Regular expressions used to calculate indent, etc.
;;;
(defconst formal-defun-re       "\\<\\(module\\|instance\\|process\\|vunit\\|vmode\\|vprop\\)\\>"
  "Formal keywords that start defuns")
(defconst formal-beg-block-ind-re   "\\<\\(case\\|if\\)\\>"
  "Formal keywords")
(defconst formal-beg-block-re   "\\<\\(case\\|if\\)\\>\\|{\\|%\\(for\\|if\\)\\>"
  "Formal keywords")
				;\<\(case\|if\)\>\|{
(defconst formal-end-block-ind-re   "\\\\|%end\\>" 
  "Formal keywords")
(defconst formal-end-block-re   "\\\\|}\\|%end\\>" 
  "Formal keywords")
				;\<\(esac\|endcase\|endif\)\>\|}
(defconst formal-rule-keywords-all  "\\<\\(envs\\|f\\(airness\\|or\\(all\\|mulas?\\)\\)\\|strong\\|test_pins\\|assert\\|re\\(duce_instance\\|strict\\)\\|inherit\\)\\>"
  "Formal keywords in rules")
(defconst formal-rule-keywords  "\\<\\(envs\\|f\\(airness\\|ormulas?\\)\\|assume\\|assume_guarantee\\|restrict\\|restrict_guarantee\\|cover\\|re\\(duce_instance\\|strict\\)\\|inherit\\)\\>"
  "Formal keywords in rules, exept for 'forall")
(defconst formal-indent-1-re    (concat "\\<\\(var\\|assign\\|define\\|in\\(itially\\|var\\)\\|trans\\|fg\\|gf\\)\\>\\|"
					formal-rule-keywords-all)
  "Formal keywords of indentation level 1, include formal-rule-keywords-all")
(defconst formal-indent-2-re    "\\<\\(init\\|next\\|m\\(ax\\|in\\\)\\)\\>" 
  "Formal keywords of indentation level 2")

;(defconst formal-symbol-re      "\\<[a-zA-Z_][a-zA-Z_0-9.]*\\>")
;(defconst formal-declaration-re "\\<\\(var\\)\\>")
;(defconst formal-sub-block-re   "\\<\\(if\\|else\\|then\\)\\>")
;(defconst formal-noindent-re    "\\<\\(begin\\|end\\|until\\|else\\)\\>")
;(defconst formal-nosemi-re      "\\<\\(begin\\|repeat\\|then\\|do\\|else\\)\\>") ;? 

;;(defconst formal-autoindent-lines-re  "\\<\\(module\\|instance\\|process\\|rule\\|mode\\|var\\|endif\\|begin\\|else\\)\\>")  ;?
(defconst formal-autoindent-lines-re
  (concat formal-defun-re "\\|" formal-indent-1-re "\\|\\<\\(init\\|next\\)\\>\\|" 
	  formal-beg-block-re "\\|\\<\\(then\\|else\\)\\>\\|" formal-end-block-re )
  "Formal keywords")
  
;;; Strings used to mark beginning and end of excluded text
(defconst formal-exclude-str-start "/*-----\\/----- EXCLUDED -----\\/-----")
(defconst formal-exclude-str-end " -----/\\----- EXCLUDED -----/\\-----*/")

(defvar formal-mode-syntax-table nil
  "Syntax table in use in Formal-mode buffers.")

(if formal-mode-syntax-table
    ()
  (setq formal-mode-syntax-table (make-syntax-table))
  (modify-syntax-entry ?\\ "."   formal-mode-syntax-table)
  (modify-syntax-entry ?+ "."    formal-mode-syntax-table)
  (modify-syntax-entry ?- ". 12a" formal-mode-syntax-table)
  (modify-syntax-entry ?= "."    formal-mode-syntax-table)
  (modify-syntax-entry ?% "."    formal-mode-syntax-table)
  (modify-syntax-entry ?< "."    formal-mode-syntax-table)
  (modify-syntax-entry ?> "."    formal-mode-syntax-table)
  (modify-syntax-entry ?& "."    formal-mode-syntax-table)
  (modify-syntax-entry ?| "."    formal-mode-syntax-table)
  (modify-syntax-entry ?_ "w"    formal-mode-syntax-table)
  (modify-syntax-entry ?/ ". 58b" formal-mode-syntax-table)
  (modify-syntax-entry ?* ". 67b" formal-mode-syntax-table)
  (modify-syntax-entry ?\n "> a" formal-mode-syntax-table)
  (modify-syntax-entry ?\' "\""  formal-mode-syntax-table))

  
(defconst formal-font-lock-keywords-1 
(list 
 '("^#[ 	]*include[      ]+\\(<[^>\"\n]+>\\)" 1 font-lock-string-face)
 '("^[ \t]*#[ \t]*define[ 	]+\\(\\(\\[sw+\\)(\\)" 2 font-lock-function-name-face)
 '("^#[ 	]*if\\>" ("\\<\\(defined\\)\\>[ 	]*(?\\(\\sw+\\)?" nil nil
			  (1 font-lock-preprocessor-face) (2 font-lock-variable-name-face nil t)))
 '("^#[ 	]*elif\\>" ("\\<\\(defined\\)\\>[ 	]*(?\\(\\sw+\\)?" nil nil
			    (1 font-lock-preprocessor-face) (2 font-lock-variable-name-face nil t)))
 '("^[ \t]*\\(#[ 	]*[a-z]+\\)\\>[ 	]*\\(\\sw+\\)?"
   (1 font-lock-preprocessor-face) (2 font-lock-variable-name-face nil t))
 '("\\<\\(boolean\\|o\\(riginal\\|verride\\)\\|prev\\)\\>"
   1 font-lock-type-face)   
 '("\\(%\\<\\(for\\|e\\(nd\\|lse\\)\\|i\\(f\\|n\\)\\|then\\)\\>\\)"     
   ;;\(      %for \|%end   \|%else  \|%if   \|%in  \|%then   \> \)"     
   1 font-lock-reference-face)
 '("\\(%?\\<\\(step\\|do\\)\\>\\)"
   1 font-lock-reference-face)
 '("\\<\\(assign\\|define\\|in\\(stance\\|it\\(\\|ially\\)\\|var\\)\\|module\\|vmode\\|vunit\\|vprop\\|process\\|next\\|trans\\|var\\)\\>"
   ;;\< \(assign \|define \|instance    \|init  \|initially\|invar  \|module    \|mode \|rule \|process \|next \|trans \|var\)
   1 font-lock-keyword-face)  
 '("\\<\\(strong\\|forall\\|fairness\\|hints\\|assert\\|inherit\\|re\\(duce_instance\\|strict\\)\\|assume\\|assume_guarantee\\|property\\|sequence\\|abort\\|struct\\|clock\\|const\\|default\\|endpoint\\|eventually\\|restrict\\|restrict_guarantee\\|cover\\)\\>"
   ;;\< \(envs \|fairness    \|forall   \|formula \|formulas   \|inherit \|reduce_instance   \\|restrict  \|test_pins \|as_in
   1 font-lock-keyword-face) 
  '("^[ \t]*\\<\\(GF\\>\\([ \t]*->[ \t]*GF\\>\\)?\\|FG\\>\\([ \t]*->[ \t]*\\(FG\\|GF\\)\\>\\)?\\)"
   1 font-lock-keyword-face)
 ) "Low-level to highlight in Formal mode.")

(defconst formal-font-lock-keywords-2
  (append formal-font-lock-keywords-1
	  (list
	   '("^[ \t]*\\(mod\\(ule\\|e\\)\\|instance\\|property\\|sequence\\|abort\\|struct\\|clock\\|const\\|default\\|endpoint\\|eventually\\|rule\\|vunit\\|vmode\\|vprop\\)\\>[ \t]*\\([a-z_][a-z0-9_]*\\)"
	     3 font-lock-function-name-face)
;	   '("^[ \t]*\\(var\\)\\>\\( override\\)?[ \t\n]*\\([a-z0-9_/]+\\)"
;	     3 font-lock-variable-name-face)           ;; first variable in var statement
;	   '("^[ \t]*\\(var\\)\\>\\( override\\)?[ \t\n]*\\(\\([a-z0-9_/]+\\)\\(([^)])\\)?,[ \n]*\\)*\\([a-z][a-z0-9_]*\\)"
;	     (3 font-lock-variable-name-face nil t))           ;; second  variable in var statement
	   '("^[ \t]*\\(\\(var\\)\\>\\( override\\)?\\)[ \t\n]*\\([a-z0-9_/]+\\)"
	     (font-lock-match-c++-style-declaration-item-and-skip-to-next
	      (goto-char (or (match-beginning 4) (match-end 1)))
	      (goto-char (match-end 1))
	      (1 font-lock-variable-name-face)))
	   ;; I do not know what this means, I just stalled it from C highlight!
	   '("^[ \t]*\\(assign[ \t]*\\)?\\(init\\|next\\)([ \t]*\\([a-z0-9_/]+\\)"
	     3 font-lock-variable-name-face)
;; '("[ \t]*\\([a-z0-9_\\]+\\)\\>[ \t]*:=" 1 font-lock-variable-name-face t) 
;; '("[ \t]*\\([a-z0-9_]+\\)([0-9]+)[ \t]*:=" 1 font-lock-variable-name-face t) 
;; '("[ \t]*\\([a-z0-9_]+\\)([0-9]+..[0-9]+)[ \t]*:=" 1 font-lock-variable-name-face t)
	   '("^[ \t]*\\(forall\\)[ \t\n]*\\([a-z0-9_/]+\\)"
	     2 font-lock-variable-name-face)
	   '("[^#]?\\<\\(if\\|case\\|e\\(lse\\|nd\\(if\\|case\\)\\|sac\\)\\|then\\)\\>"
	     ;;     \< \(if \|case \|else    \|endif   \|endcase \|esac    |then \) \>
	     1 font-lock-doc-string-face) ;font-lock-defun-face
	   '("[^\\]?\\<\\(a\\(\\|lways\\|B\\(F\\|G\\)\\|F\\|G\\|X\\)\\|E\\(\\|B\\(F\\|G\\)\\|F\\|G\\|X\\)\\|never\\|goto\\|holds_until\\|m\\(ax\\|in\\)\\|X\\|F\\|G\\)\\>"
	     1 font-lock-reference-face)
	   '("[^\\]?\\<\\(before_?\\>\\(!_?\\)?\\|next_event\\(\\|_f\\|_e\\|_a\\)\\>[!]?\\|U\\(\\>\\|ntil_?\\>\\(!_?\\)?\\)\\|W\\(\\>\\|hilenot\\>!?\\|ithin\\>!?\\)\\)"
	     1 font-lock-reference-face)
 )))


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

;(put 'formal-mode 'font-lock-defaults
;     '((formal- font-lock-keywords	formal-font-lock-keywords-1 formal-font-lock-keywords-2)
;       nil t ((?\_ . "w")) nil ))
;(put 'formal-mode 'font-lock-defaults '(formal-font-lock-keywords nil t ((?\_ . "w")) nil ))
;(setq font-lock-defaults 'formal-mode)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Custom variables definition

(defconst formal-emacs-ver-20.2-or-more-p (and ;(string-match "Xemacs " emacs-version)
						      (>= emacs-major-version 20)
						      (>= emacs-minor-version 2)))

(if formal-emacs-ver-20.2-or-more-p	;(symbolp custom-define-hook)	
    (progn
      
(defgroup formal nil
      "Major mode for editing Formal source (EDL code and Sugar) in Emacs"
      :group 'languages)

(defcustom formal-debug nil
  "*Print messages for debugging if not nil"
  :type 'boolean
  :group 'formal)

(defcustom formal-tab-indent t
  "*Non-nil means TAB in Formal mode should reindent the current line,
regardless of where in the line point is when the TAB command is used.
The only exeption is when formal-tab-indent-in-comment set false
and point is in comment."
  :type 'boolean
  :group 'formal)

(defcustom formal-tab-indent-in-comment nil
  "*Concerns indentation in comment.
Non-nil means TAB in Formal mode should reindent the current comment line,
Meaningful if formal-tab-indent is true"
  :type 'boolean
  :group 'formal)

(defcustom formal-tabulated-colon nil
  "* If true, colons in cases and assignements (:=) aligned to the same level"
  :type 'boolean
  :group 'formal)  

(defgroup formal-indent nil
  "*Formal indentation levels definitions"
  :group 'formal)

(defcustom formal-indent-level 2
  "*Indentation of Formal statements with respect to containing block."
  :type 'integer
  :group 'formal-indent)

(defcustom formal-indent-level-big 6
  "*Indentation of long Formal statements (like assign of a long statement)
with respect to its beginning."
  :type 'integer
  :group 'formal-indent)

(defcustom formal-indent-colon-in-declaration-level nil
  "*Indentation of Formal statements including colon with respect to its beginning."
  :type 'integer
  :group 'formal-indent)  
(defcustom formal-indent-colon-in-case-level nil
  "*Indentation of Formal case assignements starting with colon with respect to its beginning."
  :type 'integer
  :group 'formal-indent)

(defcustom formal-indent-tabulated-colon-level nil
  "*Position of tabulated colon in cases and assignements (:=)."
  :type 'integer
  :group 'formal-indent)  

(defcustom formal-indent--comment-small 48
  "*Indentation for -- comments after statement."
  :type 'integer
  :group 'formal-indent)
(defcustom formal-indent--comment-big 64
  "*Indentation for -- comments after long statement."
  :type 'integer
  :group 'formal-indent)

(defcustom formal-indent-sugar 2
  "*Indentation inside Sugar formulas."
  :type 'integer
  :group 'formal-indent)

(defcustom formal-auto-newline nil
  "*Non-nil means automatically newline after semicolons."
  :type 'boolean
  :group 'formal)

)
(progn
(defvar formal-tab-indent t
  "*Non-nil means TAB in Formal mode should reindent the current line,
regardless of where in the line point is when the TAB command is used.
The only exeption is when formal-tab-indent-in-comment set false
and point is in comment.")
(defvar formal-tab-indent-in-comment nil
  "*Concerns indentation in comment.
Non-nil means TAB in Formal mode should reindent the current comment line,
Meaningful if formal-tab-indent is true")

(defvar formal-tabulated-colon nil
  "* If true, colons in cases and assignements (:=) aligned to the same level")

(defvar formal-indent-level 2
  "*Indentation of Formal statements with respect to containing block.")
(defvar formal-indent-level-big 6
  "*Indentation of long Formal statements (like assign of a long statement)
with respect to its beginning.")
(defvar formal-indent-colon-in-declaration-level nil
  "*Indentation of Formal statements including colon with respect to its beginning.")
(defvar formal-indent-colon-in-case-level nil
  "*Indentation of Formal case assignements starting with colon with respect to its beginning.")
(defvar formal-indent-tabulated-colon-level nil
  "*Position of tabulated colon in cases and assignements (:=).")
(defvar formal-indent--comment-small 48
  "*Indentation for -- comments after statement.")
(defvar formal-indent--comment-big 64
  "*Indentation for -- comments after long statement.")
(defvar formal-indent-sugar 2
  "*Indentation inside Sugar formulas.")

(defvar formal-auto-newline nil
  "*Non-nil means automatically newline after semicolons.")
(defvar formal-debug nil
  "*Print messages for debugging if not nil")
))



;(defcustom formal-auto-endcomments t
;  "*Non-nil means a comment \* ... } is set after the ends which ends cases and
;functions. The name of the function or case will be set between the braces.
;Currently not working"
;  ;; function formal-set-autocomments
;  :type 'boolean
;  :group 'formal)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;;  Macros
;;;

(defun try ()
  (interactive)
  (formal-debug-message "try1")
  (formal-debug-message "try2,%s " 2))

(defsubst formal-debug-message (FMT &rest ARGS)
  (if formal-debug
;      (if ARGS	  
	  (message FMT ARGS)))
 ;   (message FMT)))

(defsubst formal-get-beg-of-line (&optional arg)
  (save-excursion
    (beginning-of-line arg)
    (point)))

(defsubst formal-get-end-of-line (&optional arg)
  (save-excursion
    (end-of-line arg)
    (point)))

(defsubst formal-inside-comment-or-string-p () ; Written by Irit
  "Return true if inside comment or string"
  (let ((parse-sexp-ignore-comments nil)
	(state (save-excursion
		 (parse-partial-sexp (point-min) (point)))))
    (or (nth 3 state) (nth 4 state))))

(defsubst formal-search-forward (regexp &optional bound noerror)
  "Search forward for regexp, skiping comments and strings.
Move point and Return search result (point). Returns nil if regexp not found"
  (let ((search-result))
    (while (and (setq search-result (re-search-forward regexp bound noerror))
		(formal-inside-comment-or-string-p))
      ())
    search-result))

(defsubst formal-search-backward (regexp &optional bound noerror)
  "Search backward for regexp, skiping comments and strings.
Move point and Return search result (point). Returns nil if regexp not found"
  (let ((search-result))
    (while (and (setq search-result (re-search-backward regexp bound noerror))
		(formal-inside-comment-or-string-p))
      ())
    search-result))

(defsubst formal-search-indent-clues-backward (clues)
  "Goes back until something in  is found.
Skips strings and comments"
  (while (and (re-search-backward clues nil 'move)
	      (not (equal (point) (point-min)))
	      (formal-inside-comment-or-string-p)) 
    ()))

(defsubst parse-state (from)
  "Used in indentation functions"
  (let ((parse-sexp-ignore-comments t))
    (save-excursion (parse-partial-sexp from (point)))))

(defun skip-comments-backward ()
  "Skip comments and  blank characters backward.
Change point"
  (while (/= (point)
	     (progn (forward-comment -1)
		    (point)))
    nil)
  (skip-syntax-backward " "))

(defun skip-comments-forward ()
  "Skip comments and  blank characters forward.
Change point. Return nil."
  (while (/= (point)
	     (progn (forward-comment 1) (point))) nil)
  (skip-syntax-forward " ")
  ())
  
(defsubst formal-within-string ()
  (save-excursion
    (nth 3 (parse-partial-sexp (formal-get-beg-of-line) (point)))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;###autoload

(defun formal-mode ()
  "Major mode for editing Formal (EDL and Sugar) code. \\
TAB indents for Formal code.  Delete converts tabs to spaces as it moves back.

Useful functions are: 
\\[formal-mark-defun]\t Mark function
\\[formal-beg-of-defun]\t Move to beginning of current function
\\[formal-end-of-defun]\t Move to end of current function
\\[comment-region]\t Inserts -- in the beginning of the line 
\\[uncomment-region]\t Removes -- in the beginning of the line
\\[formal-indent-region]\t Indent every line in region

Variables controlling indentation/edit style:

 formal-tab-indent		 (default t)
  Non-nil means TAB in Formal mode should reindent the current line,
regardless of where in the line point is when the TAB command is used.
The only exeption is when formal-tab-indent-in-comment set false
and point is in comment.

 formal-tab-indent-in-comment	 (default nil)
  Concerns indentation in comment or string. Meaningful if formal-tab-indent is true.
Non-nil means TAB in Formal mode should reindent the current comment line.

 formal-tabulated-colon t
  If true, colons in cases and assignements (:=) aligned to the same level

 formal-indent  - Levels of indentation
	formal-indent-level		(default 2)
	   Indentation of Formal statements with respect to containing block.
	formal-indent-level-big	        (default 6)
	   Indentation of long Formal statements (like assign of a long statement)
           with respect to its beginning.
	formal-indent-colon-in-declaration-level (default 24)
	   Indentation of Formal statements including colon with respect to its beginning.
	formal-indent-colon-in-case-level        (default 15)
	   Indentation of Formal case assignements starting with colon with respect to its beginning.
 	formal-indent-tabulated-colon-level      (default 72)
  	   Position of tabulated colon in cases and assignements (:=).
	formal-indent--comment-small    (default 48)
	   Indentation for -- comments after statement.
	formal-indent--comment-big	(default 64)
	   Indentation for -- comments after long statement.
	formal-indent-sugar		(default 2)
	   Indentation inside Sugar formulas.

 formal-auto-newline		 (default nil)
  Non-nil means automatically newline after semicolons."

;Turning on Formal mode calls the value of the variable formal-mode-hook with
;no args, if that value is non-nil."
  (interactive)
  (if (>= emacs-major-version 20)
      (progn
	(kill-all-local-variables)
	(use-local-map formal-mode-map)
	(setq major-mode 'formal-mode)
	(setq mode-name "Formal")
	(setq local-abbrev-table formal-mode-abbrev-table)
	(set-syntax-table formal-mode-syntax-table)
	(make-local-variable 'indent-line-function)
	(setq indent-line-function 'formal-indent-line)
	;;(setq comment-indent-function 'formal-indent-comment)
	(make-local-variable 'parse-sexp-ignore-comments)
	;;Non-nil means `forward-sexp', etc., should treat comments as whitespace.
	(setq parse-sexp-ignore-comments nil)
	(make-local-variable 'case-fold-search) ;Non-nil if searches should ignore case.
	(setq case-fold-search t)
	(make-local-variable 'comment-start)
	(setq comment-start "--")		; String to insert to start a new comment
	(make-local-variable 'comment-end)
	(setq comment-end "")			; String to insert to end a new comment.
	(make-local-variable 'comment-start-skip)
	;; Regexp to match the start of a comment plus everything up to its body.
	(setq comment-start-skip "/\\*+ *\\|-- *")
	;;  (make-local-variable 'comment-multi-line)`
					;  (setq comment-multi-line t)
	;; Font lock support
	(make-local-variable 'font-lock-defaults)
	(setq font-lock-defaults
	      '((formal-font-lock-keywords formal-font-lock-keywords-1 formal-font-lock-keywords-2)
		nil t ((?\_ . "w")) nil ))
	(if (not font-lock-mode)
	    (font-lock-mode))
	;;(?/ . "w") can not add to syntax-table because its unhighlights comments
					;	'(formal-font-lock-keywords nil t))
	;; Imenu support don't know what is this!
	;;  (make-local-variable 'imenu-generic-expression)
	;;  (setq imenu-generic-expression formal-imenu-generic-expression)
	;;  (run-hooks 'formal-mode-hook))
	(if (not formal-mode-popup-menu)
	    (easy-menu-define formal-mode-popup-menu formal-mode-map ""
			      formal-mode-popup-menu-1))
	(easy-menu-add formal-mode-popup-menu)
	(if (and (string-match "walzer" abbreviated-home-dir)
		 (not formal-tabulated-colon))
	    (or (beep)
		(y-or-n-p "Gil, did you forget to set Tabulated Colon option on? "))))
    (message "This formal-mode.el file runs only for Emacs or Xemacs version grater than 20"))
  )



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;;  Electric functions
;;;


(defun electric-formal-terminate-line ()
  "Terminate line and indent next line."
  (interactive)
  ;; First, check if current line should be indented
  (save-excursion
    (beginning-of-line)
    (skip-chars-forward " \t")
    (if (looking-at formal-autoindent-lines-re)
	(formal-indent-line)) )
  (delete-horizontal-space)		; Removes trailing whitespaces
  (newline)
  ;; Indent next line
  (formal-indent-line)
  (skip-chars-forward " \t")
  ;;(end-of-line)
  ;; Maybe we should set some endcomments
;  (if formal-auto-endcomments
;      (formal-set-auto-comments))
  ;; Check if we shall indent inside comment
;  (let ((setstar nil))
;    (save-excursion
;      (forward-line -1)
;      (skip-chars-forward " \t")
;      (cond ((looking-at "\\*[ \t]+\\")
;	     ;; Delete region between `*' and `)' if there is only whitespaces.
;	     (forward-char 1)
;	     (delete-horizontal-space))
;	    ((and (looking-at "(\\*\\|\\*[^\\]")
;		  (not (save-excursion
;			 (search-forward "*\\" (formal-get-end-of-line) t))))
;	     (setq setstar t))))
;    ;; If last line was a star comment line then this one shall be too.
;    (if (null setstar)	
;	(formal-indent-line)
;      (insert "*  "))))
  )

(defun electric-formal--comment ()
  "Insert '-'character, reindent line and indent comments"
  (interactive)
  (if (let ((signal-error-on-buffer-boundary nil)) ; forward-char will not signal error at start of buffer
	(save-excursion (forward-char -1)
			(char-equal (char-after (point)) ?-)))		; if -- comment
      (progn (save-excursion
	       (beginning-of-line)
	       (formal-indent-line))
	     (if (save-excursion
		   (beginning-of-line)
		   (not (looking-at "[ \t]*-")))
		 (let ((current-col (current-column)))
		   (save-excursion
		     (skip-chars-backward "-" (point-min))
		     (cond
		      ((< current-col formal-indent--comment-small)
		       (indent-to formal-indent--comment-small))
		      ((< current-col formal-indent--comment-big)
		       (indent-to formal-indent--comment-big))
		      (1
			 (insert "\t"))
		      )))
	       ()))
    ())
  (insert "-"))

(defun electric-formal-semi ()
  "Insert `;' character and reindent the line."
  (interactive)
  (insert last-command-char)
  (if formal-auto-newline
      (electric-formal-terminate-line)
    (save-excursion
      (beginning-of-line)
      (formal-indent-line))))

(defun electric-formal-close-brace ()
  "Insert `}' or ')' character and indent line, if it is end of block. Maybe not needed?"
  (interactive)
  (insert last-command-char)
  ;; Do nothing if within string.
  (if (formal-inside-comment-or-string-p)
      ()
    (save-excursion
      (beginning-of-line)
      (if (looking-at "[ \t]*\\()\\|}\\)")
	  (formal-indent-line))
      )))

(defun electric-formal-colon-in-case (start-block)
  "Insert white space before : in case statement. Used in electric-formal-colon only"
  (let ((first-colon-ind (formal-search-first-colon-incase-indent start-block (1-(point))))
	(start-block-column (save-excursion
			      (goto-char start-block)
			      (current-column))))
    (cond (first-colon-ind		; : was in this case already
	   (if (< (current-column) first-colon-ind)
	       (indent-to first-colon-ind)
	     (insert "\t")))
	  ((save-excursion		; line starting with: ?
	     (beginning-of-line)
	     (looking-at "[ \t]*."))
	   (fixup-whitespace)		; Removes trailing whitespaces
	   (insert " ")
	   (if (< (current-column)  (+ start-block-column formal-indent-colon-in-case-level))
	       (indent-to (+ start-block-column formal-indent-colon-in-case-level))
	     (insert "\t")))
	  (1
	   (indent-to (+ (current-indentation) formal-indent-colon-in-case-level)))
	  )))

(defun formal-fixed-indent-to (indentation-col)
  "Indent from point with tabs and spaces until indentation-col is reached.
If current column greater then indentation-col insert new line."
  (fixup-whitespace)
  (if (> (current-column) indentation-col)
      (insert "\n"))
  (indent-to indentation-col))

(defun electric-formal-colon ()
  "Insert `:' and do all indentions except line indent on this line."
  (interactive)
  (if (formal-inside-comment-or-string-p)
       ()				; Do nothing if within string.
    (let* ((here (point))
	   (indent-str (save-excursion
			 (beginning-of-line)
			 (formal-indent-line)))
	   (type (car indent-str))
	   (start-block (if (car (cdr indent-str))
			    (car (cdr indent-str))
			  0))
	   (start-block-column))
      (cond ((equal type 'case)
	     (if formal-tabulated-colon
		 (formal-fixed-indent-to formal-indent-tabulated-colon-level)
	       (electric-formal-colon-in-case start-block)))
	    ((equal type 'declaration)
	     (save-excursion (goto-char start-block)
			     (setq start-block-column (current-column)))
	     (fixup-whitespace)
	     (indent-to formal-indent-colon-in-declaration-level)
	     (insert "\t"))	
	    ((and (equal type 'level-1)
		  (save-excursion
		    (if (second indent-str)
			(goto-char start-block)
		      (beginning-of-line))
		    (and (looking-at "[ \t]*forall\\>")
			 (formal-search-forward ":" here 'noerror)) ))
	     1)				; Second : in [forall varname : vartype :]
	    ((save-excursion
	       (beginning-of-line)
	       (looking-at "[ \t]*\\(var\\|forall\\)"))
	     (if (< (current-column) formal-indent-colon-in-declaration-level)
		 (indent-to  formal-indent-colon-in-declaration-level)
	       (insert "\t")))
	    ((or (equal type 'defun)
		 (not formal-tabulated-colon)) ; :=
	     (insert "\t")) 
	    (1				; formal-tabulated-colon in :=
	     (formal-fixed-indent-to formal-indent-tabulated-colon-level)
	     ))))
    ;(let ((formal-tab-always-indent nil))
     ; (formal-indent-command))))
  (insert last-command-char))
    
(defun electric-formal-hash ()
  "Insert `#', and indent to column 0 if this is a CPP directive."
  (interactive)
  (insert last-command-char) 
  (if (save-excursion (beginning-of-line) (looking-at "^[ \t]*#"))
      (save-excursion (beginning-of-line)
		      (delete-horizontal-space))))

(defun electric-formal-tab ()
  "Function called when TAB is pressed in Formal mode."
  (interactive)
;  (if (or (formal-inside-comment-or-string-p)
;	  (and (not (bolp))
;	       (save-excursion (beginning-of-line) (char-equal (following-char) ?#))))
;      (insert "\t")
  ;; If tab not indent, or tab not indent in comment and we are in comment, only insert tab.
    (if (or (not formal-tab-indent)	
	    (and (not formal-tab-indent-in-comment) 
		 (formal-inside-comment-or-string-p)))
	    (insert "\t")
      ;; If formal-tab-indent, indent the beginning of the line.
;      (progn			  	
	(save-excursion
	  (beginning-of-line)
	  (formal-indent-line))
;	(if (save-excursion
;	      (skip-chars-backward " \t")
;	      (bolp))
;	    (formal-indent-line)
;	  (insert "\t")))
    ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; Interactive functions
;;;

(defun formal-indent-region (beg end)
  "Indent every line in region"
  (interactive "r")  
  (save-excursion
    (let ((lines-num (count-lines beg end))
	  (lines-num-done 0))
      (goto-char beg)
    (while (< lines-num-done lines-num)
      (formal-indent-line)
      (forward-line 1)
      (setq lines-num-done (1+ lines-num-done)) )    )))

(defun uncomment-region (beg end)
  "Simple call to comment-region with negative argument.
Equivalent C-u -1 M-x comment-region"
  (interactive "r")  
  (comment-region beg end -1)) 

(defun skip-parentheses ()
  "From openning parentheses jump to closing"
  (interactive)
  (let ((parse-sexp-ignore-comments t))
    (if (or (equal (char-after (point)) ?\{)
	    (equal (char-after (point)) ?\())
	(goto-char (scan-lists (point) 1 0))
      (goto-char (scan-lists (point) -1 0)) )))

;;; search and mark of beginning and end of function 

(defun formal-search-end-of-defun-from-beg () ; Written by Irit 
  "Search and Return position of the end of defun, assuming standing at the beginning of defun.
Called from (formal-search-beg-of-defun)"
  (save-excursion
    (if (not (looking-at formal-defun-re))
	()				;\\<\\(module\\|instance\\|process\\|rule\\|mode\\)\\>")
      (let* ((parse-sexp-ignore-comments t)
	     (end-of-defun-from-beg (cond ((looking-at "instance\\>")
					   (formal-search-forward ";" nil 'move))
					  ((looking-at "module\\>")
					   (scan-lists (point) 3 0 (current-buffer) 'noerror))
					  (1
					   (scan-lists (point) 1 0 (current-buffer) 'noerror))) ))
	(if end-of-defun-from-beg
	    (progn  (goto-char end-of-defun-from-beg)
		    (end-of-line)
		    (point)) 
	  (point-max))			;last function not finished
	))))

(defun formal-search-beg-of-defun ()
  "Search for beginning of current defun. If found, returns list (beg-of-defun enf-of-defun).
If not found returns nil"
  (save-excursion
    (let ((here (point))
	  (end-of-defun))
      (formal-search-indent-clues-backward formal-defun-re)
      (catch 'beginning
	(while t
	  (cond
	   ((not (looking-at formal-defun-re))	    
	  (throw 'beginning nil))	; reached beg-of-buffer -> Not inside a function
	   ((and (setq end-of-defun (formal-search-end-of-defun-from-beg))
		 (> end-of-defun here))
	    (throw 'beginning (list (point) end-of-defun)))
	   ;; \\<\\(module\\|instance\\|process\\|rule\\|mode\\)\\>"
	   ;; - only instance\\|process inside something else
	   ((looking-at "\\<\\(module\\|rule\\|mode\\)\\>")
	    (throw 'beginning nil)))
	  ;; Left case of function inside function
	(formal-search-indent-clues-backward "\\<\\(module\\|rule\\|mode\\)\\>")) 
	))))
    	   

(defun formal-beg-of-defun ()		; Written by Irit
  "Move backward to the beginning of the current function or procedure."  
  (interactive)
  (let ((beg-of-defun (formal-search-beg-of-defun )))
    (if beg-of-defun
	(goto-char (car beg-of-defun))
      (message "Not inside function"))))

(defun formal-end-of-defun ()		; Written by Irit
  "Move forward to the end of the current function or procedure."
  (interactive)
  (let ((beg-end-of-defun (formal-search-beg-of-defun)))
    (if beg-end-of-defun
	(goto-char (second beg-end-of-defun))
      (message "Not inside function"))))

(defun formal-mark-defun ()		; Stallen and changed by Irit
  "Mark the current formal function (or procedure).
This puts the mark at the end, and point at the beginning."
  (interactive)
;  (push-mark)
  (let ((beg-end-of-defun (formal-search-beg-of-defun )))
    (if beg-end-of-defun
	(progn
	  (push-mark)
;	  (goto-char (second beg-end-of-defun))	;(formal-end-of-defun)
	  (push-mark (second beg-end-of-defun))
	  (goto-char (car beg-end-of-defun)) ;(formal-beg-of-defun)
	  (if (fboundp 'zmacs-activate-region)
	      (zmacs-activate-region)))
      (message "Not inside function"))))      
  
     	       
;;; -- change case of keywords functions

;(defun formal-downcase-keywords ()
;  "Downcase all Formal keywords in the buffer."
;  (interactive)
;  (formal-change-keywords 'downcase-word))

;(defun formal-upcase-keywords ()
;  "Upcase all Formal keywords in the buffer."
;  (interactive)
;  (formal-change-keywords 'upcase-word))

;(defun formal-capitalize-keywords ()
;  "Capitalize all Formal keywords in the buffer."
;  (interactive)
;  (formal-change-keywords 'capitalize-word))

;;; Change the keywords according to argument.
;(defun formal-change-keywords (change-word)
;  (save-excursion
;    (let ((keyword-re (concat "\\<\\("
;			      (mapconcat 'identity formal-keywords "\\|")
;			      "\\)\\>")))
;      (goto-char (point-min))
;      (while (re-search-forward keyword-re nil t)
;	(funcall change-word -1)))))

;.

;;;
;;; Other functions
;;;
;(defun formal-set-auto-comments ()
;  "Insert `\* case *\' or `\* NAME }' on this line if appropriate.
;Insert `\* case *\' if there is an `end' on the line which
;ends a case block.  Insert `\* NAME }' if there is an `end'
;on the line which ends a function or procedure named NAME."
;  (save-excursion
;    (forward-line -1)
;    (skip-chars-forward " \t")
;    (if (and (looking-at formal-end-block-re) ; changed, was //"))
	  (thenelse (looking-at "[ \t]*%\\(then\\|else\\)\\>")))
      (formal-search-indent-clues-backward "%\\(if\\|for\\|then\\|end\\)\\>")
      (while (not (eq (point) (point-min)) )	
	(cond
	 ((looking-at "%end\\>")
	  (setq nest (1+ nest)))	
	 ((eq nest 0)
	  (cond ((looking-at "%\\(if\\|for\\)\\>") ; % beginning found!
		 (cond
		  (thenelse
		   (throw 'nesting (list 'ifthenelse (point))))
		  (end
		   (throw 'nesting (list 'endblock (point))))
		   ))
		((looking-at "%then\\>")
		 (if (and (not end)
			  thenelse)	; found %then for %else
		     (throw  'nesting (list 'endblock))))
		))
	 ((looking-at "%\\(if\\|for\\)\\>")
	  (setq nest (1- nest))))
	(formal-search-indent-clues-backward "%\\(if\\|for\\|then\\|end\\)\\>")))      
  ))

(defun formal-calculate-indent-local ()
  " Calculate indentation using only this line information. If indentation type found, returns
list (indent-type  character-address-of-start-of-innermost-containing-list; nil if non)
Called only from formal-calculate-indent function"
  (save-excursion
    (let* ((state (parse-state (point-min)))
	   (clue-start))
      (cond ((nth 3 state) (throw 'nesting (list 'string nil)))
	    ((or (nth 4 state) nil)
	     ;;looking-at "--\\|/\\*"))
	     (throw 'nesting (list 'comment nil)))
	    ((and (eq (char-after (point)) ?\} )
		  (second state))
	     (throw 'nesting (list 'end-curly-block (second state)))) 
	    ((and (eq (char-after (point)) ?\) )
		  (second state))
	     (throw 'nesting (list 'endblock (second state))))
	    ((eq (following-char) ?#)
	     (throw 'nesting (list 'cpp nil)))
	    ((looking-at "%\\(end\\|then\\|else\\)\\>")
	     (formal-search-preproc-backward))		     
	    ((looking-at formal-defun-re)
	     (throw 'nesting (list 'defun nil)))
	    ((looking-at formal-indent-1-re)		    
	     (throw 'nesting (list 'level-1 nil))) ; in first line
	    ((and (looking-at "next\\>")
		  (save-excursion (skip-comments-backward)
				  (beginning-of-line)
				  (setq clue-start (point))
				  (looking-at "[ \t]*assign init\\>") ))
	     (throw 'nesting (list 'assign-next clue-start)))
	    ((looking-at formal-indent-2-re)
	     (throw 'nesting (list 'level-2 nil))) ; in first line	    
;	    ((setq clue-start (save-excursion (skip-comments-backward)
;					      (if (and (not (eq (point) (point-min)))
;						       (not (forward-char -2))
;						       (looking-at ":="))
;						  (point)
;						())))
;	     (throw 'nesting (list 'assignement clue-start)))
	    ))))

(defun formal-indent-from-end-statement (end-keyword oldpos)
  "Search point - start of current statement. Moves point. If located in start already, returns nil.
Called only from found-indent in case plain assignment found."
  (let ((end-of-prev-statement (progn	;search for end of prev assignement,  
				 (goto-char oldpos)
				 (if (formal-search-backward ";" end-keyword 'move)
				     (formal-end-statement oldpos)
				   (point))) )) 
    (if (progn (skip-comments-forward)
	       (< (point) oldpos))
	(throw 'nesting (list 'plain (point)))
      (throw 'nesting (list 'plain nil)))))

(defun found-indent-defun (oldpos)
;" Calculates type of indentation in case formal-defun-re descovered. Called from found-indent."
  (cond ((and (looking-at "\\")
              (let ((paramlist-end (save-excursion
                                     (search-forward ":")
                                     (scan-lists (point) 2 0 (current-buffer) 'noerror))))
                (or (not paramlist-end)
                    (> paramlist-end oldpos))))
         (throw 'nesting (list 'paramlist (formal-search-forward "("  nil 'move))))
        ((and (looking-at "\\")
              (let ((paramlist-end (save-excursion
                                     (scan-lists (point) 2 0 (current-buffer) 'noerror))))
                (or (not paramlist-end)
                    (> paramlist-end oldpos))))
         (throw 'nesting (list 'paramlist (formal-search-forward "("  nil 'move))))
	((save-excursion (goto-char oldpos)
			 (looking-at "{"))
	 (throw 'nesting (list 'defun (point))))
	((and (looking-at "\\")
	      (let ((process-end (save-excursion (scan-lists (point) 1 0 (current-buffer) 'noerror))))
		(or (not process-end)
		    (> process-end oldpos))))
	 (throw 'nesting (list 'process (point))))
	((save-excursion (goto-char oldpos)
			 (looking-at "}"))
	 (throw 'nesting (list 'defun (point))))
	(1
	 (throw 'nesting (list 'plain nil))) ))

(defun found-indent-formula (oldpos)
" Calculates type of indentation in case 'formula' word descovered.
Called from found-indent."
  (let ((formula-word (point))
	(formula-end (save-excursion (scan-lists (point) 1 0 (current-buffer) 'noerror)))
	(fab-opening-{))
    (cond ((and formula-end (< formula-end oldpos)) ; between formulas? 
	   (throw 'nesting (list 'level-1 nil ))) ; second in list nil - in-first-line
	  ((progn (formal-search-forward "{"  nil 'move)
		  (or (<= oldpos (point)) ; between formala-word and {
		      (= (point) (point-max))  )) ; can not proceed to next progn
	   (throw 'nesting (list 'formula formula-word)))
	  ((progn (forward-char 1)
		  (save-excursion
		    (setq fab-opening-{ (formal-search-forward "{"  nil 'move))
		    (setq fab-close-} (formal-search-forward "}"  nil 'move)))
		  (and fab-opening-{
		       (< fab-opening-{ oldpos)
		       (or (not fab-close-})
			   (> fab-close-} oldpos))))
	   (throw 'nesting (list 'fab (formal-search-forward "{"  nil 'move) )))
	  (1
	   (throw 'nesting (list 'formula (point)))   ))))

(defun found-indent (oldpos)
  "Checks if the point in place wich can give any clue about type of indentation.
If in such place, returns indentetion type and position of place which will used to indentation calculation.
Returns nil otherwise
Called only from formal-calc-indent-loop function"
  (save-excursion    
    ;;  (skip-chars-forward " \t" )
    ;;(message "got to found-indent, point is %d" (point))
    (let ((parse-sexp-ignore-comments t))
      (cond       
       ((looking-at formal-defun-re)
	(found-indent-defun oldpos))
       ((looking-at "\\")
	(found-indent-formula oldpos))
       ((and (looking-at "\\")
	     (let ((var-statement-end (save-excursion (formal-search-forward ";"  nil 'move))))
	       (or (not var-statement-end)
		   (> var-statement-end oldpos))))
	(throw 'nesting (list 'declaration (point))))
       ((looking-at "\\")	
	(let ((var-statement-end (save-excursion (formal-search-forward ":"  nil 'move)
						 (forward-char 1)
						 (formal-search-forward "\\(:\\|;\\)"  nil 'move))))
	  (if (or (not var-statement-end)
		  (> var-statement-end oldpos))
	      (throw 'nesting (list 'declaration (point)))
	    (throw 'nesting (list 'level-1 nil))  )))
       ((looking-at formal-rule-keywords)
;;"\\<\\(envs\\|forall\\|test_pins\\|reduce_instance\\|restrict\\|inherit\\|fairness\\|formula\\|formulas\\)\\>"
	(let ((statement-end (save-excursion (formal-search-forward ";" nil 'move)) ))
	  (if (and statement-end
		   (< statement-end oldpos))
	      (throw 'nesting (list 'level-1 nil)) ; second in list nil - in-first-line
	    (throw 'nesting (list 'level-1 (point))))	  ))
       ((save-excursion (eq (char-after (1- (point))) ?#))
	(throw 'nesting (list 'plain nil)))	
       ((looking-at formal-indent-1-re)
	(let* ((end-keyword (progn (skip-syntax-forward "^( " oldpos)
				   (if (looking-at "[ ]*override")
				       (and (skip-syntax-forward " " oldpos)
					    (skip-syntax-forward "^ " oldpos)))
				   (point))))
	  (formal-indent-from-end-statement end-keyword oldpos)))
       ((save-excursion (beginning-of-line)
			(looking-at "\\( \\t\\)*\\(assign \\)?\\<\\(init\\|next\\)\\>"))
	(let* ((start-keyword (point)))
	  (formal-indent-from-end-statement start-keyword oldpos)))
       ))))

(defun formal-calc-indent-end-of-search-{ ()
  " Checks whether we are in formula or fab or { block
Called only from formal-calc-indent-loop in case nest=0"
  (let ((pos (point)))    
    (skip-comments-backward)
    (forward-char -1)
    (cond ((char-equal (char-after (point)) ?\,)	; fab in fab?
	   (throw 'nesting (list 'fab pos )))
	  ((and (char-equal (char-after (point)) ?{)	; fab in formula?
		(save-excursion
		  (forward-char -1)
		  (not (formal-search-indent-clues-backward formal-autoindent-lines-re))
		  (point)
		  (looking-at "\\")))
	   (throw 'nesting (list 'fab pos )))
	  ((and
	    (not (forward-char 1))
	    (not (formal-search-indent-clues-backward formal-autoindent-lines-re))
	    (point)
	    (looking-at "\\"))
	   (throw 'nesting (list 'formula (point))))
	  (1
	   (throw 'nesting (list 'inblock pos ))))
    ))

(defsubst formal-calc-indent-end-of-search-if (end thenelse elsed)
  " Calculate indent type for if-statement.
(Was) Called only from formal-calc-indent-loop-nest-0 " 
  (throw 'nesting  
	 (cond (end			; same indent as if 
		(list 'endblock  (point)))  
	       ((or thenelse elsed)	; then/else line of If  
		(list 'ifthenelse (point)))
	       (1			; long if condition
		(list 'if (point))))	 ))

(defun formal-calc-indent-loop-nest-0 (oldpos end thenelse elsed)
  " Calculate indent type. If no nesting found search backwards for clues.
Called only from formal-calc-indent-loop in case nest=0"
  (cond ((char-equal (char-after (point)) ?{)		; inside {block}	?		 
	 (formal-calc-indent-end-of-search-{ ))
	((looking-at "%for\\>")				     
	 (throw 'nesting (list (if (not end)
				   'infor 
				 'endblock)
			       (point))))
	((looking-at "\\")
	 (throw 'nesting 
		(cond (end		; same indent as if
		       (list 'endblock  (point)))
		      ((or thenelse elsed) ; then/else line of If
		       (list 'ifthenelse (point)))
		      (1		; long if condition
		       (list 'if (point))))	 ))
;;	 (formal-calc-indent-end-of-search-if end thenelse elsed))
	((and (looking-at "\\")
	      (not end))		; in else - if or case?
	 (setq elsed (point)))		; For endif - not important
	((and (looking-at "\\")
	      (not end))		; For endif - looking for if	
	 (throw 'nesting (if thenelse	; was looking at else - should be same indentation as then
			     (list 'endblock  (point))
			   (list 'ifthen (point))) ))	; was in long then		      
	((looking-at "\\")
	 (throw 'nesting (if end	; same indent as case
			     (list 'endblock (point))		       
			   (list 'case (point))) )))
  (formal-search-indent-clues-backward formal-autoindent-lines-re))

(defun formal-calc-indent-loop (oldpos end thenelse)
  " Loop until correct indent type is found, then throws 'nesting. 
Called only from formal-calculate-indent" 
  (let* ((parse-sexp-ignore-comments t)
	 (nest 0) 
	 (elsed ))
    (formal-search-indent-clues-backward formal-autoindent-lines-re)
    (while (not (or (found-indent oldpos)
		    (eq (point) (point-min)) ))
      (cond ((char-equal (char-after (point)) ?})
	     (forward-char)
	     (backward-list 1)
	     (formal-search-indent-clues-backward formal-autoindent-lines-re))		       
	    ((looking-at formal-end-block-re)
	     (setq nest (1+ nest))
	     ;; instead of (formal-search-indent-clues-backward formal-autoindent-lines-re)
	     (cond ((looking-at "\\<\\(endcase\\|esac\\)\\>\\|{\\|}")
		    (formal-search-indent-clues-backward "\\<\\(case\\|endcase\\|esac\\)\\>\\|{\\|}"))
		   ((looking-at "\\")
		    (formal-search-indent-clues-backward "\\<\\(if\\|endif\\)\\>\\|{\\|}"))
		   ((looking-at "%end\\>")
		    (formal-search-indent-clues-backward "%\\(for\\|if\\|end\\)\\>\\|{\\|}")) ))
	    ((equal nest 0)
	     (formal-calc-indent-loop-nest-0 oldpos end thenelse elsed))
	    ((looking-at formal-beg-block-re)
	     (setq nest (1- nest))
	     (formal-search-indent-clues-backward formal-autoindent-lines-re))
	    (1
	     (formal-search-indent-clues-backward formal-autoindent-lines-re))	     
	    )    )))


(defun formal-calculate-indent ()
  "Calculate the indentation data of the current Formal line.
Return a list of three elements: (INDENT-TYPE INDENT-LEVEL Parsing-from-beginning-of-block)."
  (save-excursion    
    (beginning-of-line)
    (skip-chars-forward " \t")
    (let* ((oldpos (point))
	   (end (looking-at formal-end-block-ind-re))
	   (thenelse (looking-at "\\(then\\|else\\)\\>"))
	   (type
	    (catch 'nesting
	      ;; Check if looking at something simple
	      (formal-calculate-indent-local)
	      ;; Loop until correct indent is found
	      (formal-calc-indent-loop oldpos end thenelse)
	      ;; If indent did not found until here
	      (throw 'nesting (list 'plain nil))))
	   (state (if (second type)
		      (parse-state (second type))
		    0))) 
      (list (car type) (second type) state)
      )))

;; Functions calculation indentation (in number) when indentation type is known.
(defun formal-paramlist-indent (start-block)
  " Calculates indentation for list of parameters
 (,..)(,..)       or    instance  :  (,..)(,..) "
  (if (<= (point) start-block)		; Opening ( of in params.
      (save-excursion
	(search-backward-regexp ":\\|\\<\\(module\\|instance\\)\\>" (point-min) 'no-error)
	(current-column))
    (save-excursion			; continue params.
      (beginning-of-line)
      (+ (* formal-indent-level
	    (car (parse-state start-block)) )
	 (save-excursion (goto-char start-block)
			 (1+ (current-column)))))
    ))

(defun formal-declaration-indent (start-block)
  " Calculates indentation for VAR declaration               Var/forall ,  : type ;/:"
  (save-excursion
    (beginning-of-line)
    (if (looking-at "[ \t]*:")
	formal-indent-colon-in-declaration-level
      (let ((here (point))
	    (parse-sexp-ignore-comments t))
	(save-excursion
	  (goto-char start-block)
	  (if (search-forward-regexp ":" here 'noerrror)	 
	      (1+ (current-column))	; the long type of a "Var varname : type;"
	    ;; long Var list
	    ( + 4 formal-indent-level)))) ; after Var  = formal-indent-level + length(VAR) + 1	
      )))

(defun formal-fab-indent (start-block)
  " Calculates indentation for fab statement                 { [*], ...} "
  (let ((prev-line-indent))
    (save-excursion
      (beginning-of-line)
      (skip-chars-forward " \t")
      (cond
       ((or (eq (char-after (point)) ?\} )
	    (eq (char-after (point)) ?\) ))	; end of block
	(backward-list 1)
	(current-indentation)) 
       ((progn
	  (skip-comments-backward)
	  (forward-char -1)
	  (char-equal (char-after (point)) ?,))		; start of not first cycle description 
	;;(re-search-backward "{" start-block 'no-error)
	;;(+ sugar-indent (current-indentation)))
	(+ formal-indent-sugar prev-ind))
       ((eq (char-after (point)) ?\{ )		; start of  first cycle description
	(+ formal-indent-sugar (current-indentation)))
                      ;; continue previous cycle description left
      (1
       (forward-char)
       (let ((state (parse-state start-block)) )
	 (+ (* formal-indent-sugar (car state)) (* 3 formal-indent-sugar) prev-ind)))
      ;; ((re-search-backward "{" start-block 'no-error)
      ;;(+ (* 3 sugar-indent) (current-indentation)))
       ))))

(defun formal-formula-indent (formula)
  " Calculates indentation for formula statement              formula { .()..} "
  (save-excursion
    (beginning-of-line)
    (skip-chars-forward " \t")
    (if (or (eq (char-after (point)) ?\} )
	    (eq (char-after (point)) ?\) ))
	(progn
	  (save-excursion
	    (backward-list 1)
	    (current-indentation)))
      (let ((state (parse-state start-block)) )
	(if (second state)
	    (save-excursion		; there is { after 'formula' word
	      (goto-char (second state))
	      (cond ((char-equal (char-after (point)) ?\( )
		     (+ formal-indent-sugar (current-column)))
		    ((char-equal (char-after (point)) ?\{ )
		     (+ formal-indent-sugar (current-indentation)))
		    (1
		     (* (1+ (car state)) formal-indent-sugar))))
	  (save-excursion		; between 'formula' word and {
	    (goto-char formula)
	    (+ formal-indent-sugar (current-column))))
	)  )))

;; Case indent functions
(defsubst formal-search-first-colon-incase-indent (start-block here)
  " Calculates indentation of : in first case statement. Returns nil if not found until here"
  (save-excursion
    (goto-char start-block)
    (if (formal-search-forward ":" here 'noerror)
	(1-(current-column))
      nil)))

(defun formal-look-for-end-statement ()
  " Search for end previous statement in case-statement, after ; found. Moves point"
  (if (looking-at "}\\|;\\|d" )
      (progn
	(forward-char)   
	(skip-comments-forward)				  
	(cond ((eq (char-after (point)) ?})	; Found ; /* possible comment */ }
	       (point))
	      ((looking-at "%end\\>")	; Found ; /* possible comment */ %end
	       (forward-char 3) 
	       (point)) 
	      ;; no condition holds -> Found regular ; at end of statement. Then returns nil.
	      ))))	

(defun formal-end-statement (here)
  (let ((prev-statement-end (point))) ; else - we found ; and it is not first statement in case
    (if (and (formal-look-for-end-statement)
	     (> here (point)))	; checking it is really end of statement -is there } or %end?
	(progn
	  (setq prev-statement-end (point))
	  (if (formal-look-for-end-statement)
	      (point)
	    prev-statement-end))
      prev-statement-end)) )	; regular end of previous statement

(defun formal-previous-statement-in-case-end (start-block first-colon-ind prev-line-end-pos here)
  " Search for end previous statement in case-statement.
Return end of <> word if we are in the first statement in case"
  (if (not first-colon-ind)		; sure in first statement in case
      (+ 3 start-block)			; 3= length of "case" word -1
    (save-excursion			
      (goto-char prev-line-end-pos)
      (if (and (not (char-equal (char-after (point)) ?\;)) ; in first statement in case
	       (not (formal-search-backward ";" start-block 'noerror)))
	  (+ 3 start-block)		; 3= length of "case" word -1
	(formal-end-statement here)) )))

(defun formal-case-indent (start-block)
  " Calculates indentation for case statement
case    condition : assignement;    ... else : assignement;    esac; "  
  (save-excursion
    (beginning-of-line)
    (skip-chars-forward " \t")
    (let* ((here (point))
	   (first-colon-ind (formal-search-first-colon-incase-indent start-block here))
	   (prev-line-end-pos (save-excursion			     
				(skip-comments-backward)
				(forward-char -1)
				(point)))
	   (prev-stat-end (formal-previous-statement-in-case-end ; end of "case" word if first statement
			   start-block first-colon-ind prev-line-end-pos here))
	   (assignement-part-start (save-excursion
				     (goto-char prev-stat-end)
				     (formal-search-forward ":" here 'noerror))))
      (cond
       ((eq (char-after (point)) ?:)	; start of assignement
	(formal-debug-message "Case: looking at :, first was at %s" first-colon-ind)
	(cond (formal-tabulated-colon
	       formal-indent-tabulated-colon-level)
	      (first-colon-ind
	       first-colon-ind)
	      (1
	       (+ prev-ind formal-indent-colon-in-case-level)) ))
       ((equal prev-stat-end prev-line-end-pos) ; next or first case-statement in case
					;  (equal start-block prev-line-end-pos))
	(formal-debug-message "Case: next or first case-statement")
					;      (+ prev-ind formal-indent-level))
	(+ prev-column formal-indent-level))
       (assignement-part-start		; continue of assignement case
	(formal-debug-message "Case: Assignement part")
	
	(cond ((and			;(or (= first-colon-ind formal-indent-tabulated-colon-level)
		formal-tabulated-colon	; )
		(looking-at "\\(case\\|if\\)\\>"))
	       (+ prev-column (* 2 formal-indent-level)))
	      (1
	       (+ first-colon-ind formal-indent-level)) ))	       
       (1				; long condition
	(formal-debug-message "Case: long condition")
	(+ prev-ind formal-indent-level-big))))
    )) 
  
		  

(defun formal-curly-block-indent (start-block prev-ind)
  " Calculates indentation for block                  {} "
  (save-excursion
    (goto-char start-block)
    (skip-comments-backward)
    (forward-char -1)
    (if (char-equal (char-after (point)) ?:)	; block in case assignement part?
	(if formal-tabulated-colon
	    formal-indent-tabulated-colon-level
	  (+ (current-column) formal-indent-level) )
      (+ prev-ind formal-indent-level))))

(defun formal-end-curly-block-indent (start-block prev-ind)
  " Calculates indentation for block                  {} "
  (save-excursion
    (goto-char start-block)
    (forward-char -1)
    (skip-syntax-backward " ")
    (forward-char -1)
    (if (and (char-equal (char-after (point)) ?\")
	     (let ((parse-sexp-ignore-comments t))
	       (re-search-backward "formula" (point-min) 'noerror)))
	(current-indentation)     
      prev-ind)))

(defun formal-if-cond-indent (start-block)
  " Calculates indentation for if-statement             if () then..."
  (save-excursion
    (beginning-of-line)
    (let ((state (parse-state start-block)) ) 
      (+ prev-column 3 (* (car state) formal-indent-level))
       ;; long if condition - aligned as ( in "if ("
      )))

(defun formal-plain-indent (start-block in-first-statement-line)
  " Calculates indentation for plain statement "
  (if in-first-statement-line			; long statement
      (* 2 formal-indent-level)
    (let* ((keyword-end-indent (save-excursion
				 (goto-char start-block)
				 (current-column)))
	   (state (save-excursion
		    (beginning-of-line)
		    (parse-state start-block)) ) )
	(+ keyword-end-indent formal-indent-level (* (car state) formal-indent-level ))) ))

(defun formal-assign-next-indent (start-block)
  " Calculates indentation for asssign-next statement after assign-init          Assign next ()      "
  (save-excursion
    (beginning-of-line)
    (search-backward-regexp "\\" start-block ) ;; if error returns error
    (current-column)))

(defun formal-level-indent (start-block in-first-statement-line level)
  " Calculates indentation for level-1 and level-2 indentation statement, first and futher line of statement.
test_pins pin1, pin2, ... ; -- for example"
  (if in-first-statement-line
	(* level formal-indent-level)      
    (save-excursion
      (goto-char start-block)
      (skip-chars-forward " \t")	; looking at formal keyword now    
      (skip-chars-forward "[a-z][A-Z]_")
      (1+ (current-column)))))
      

(defconst formal-indent-alist
  '((string . formal-indent-level-big)
    (comment . (current-indentation) )
    (defun . 0)
    (cpp . 0)
    (level-1 . (formal-level-indent start-block in-first-statement-line 1))    
    (level-2 . (* 2 formal-indent-level))
    (assign-next . (formal-assign-next-indent start-block))
    (plain . (formal-plain-indent start-block in-first-statement-line))
    (endblock . prev-column)
    (end-curly-block . (formal-end-curly-block-indent start-block prev-ind))
    (round-bracket . (+ prev-column formal-indent-level))
    (if . (formal-if-cond-indent start-block))
    (ifthenelse . (+ prev-column formal-indent-level)) ; then/else of if
    (ifthen . (+ prev-column formal-indent-level))
    (inblock . (formal-curly-block-indent start-block prev-ind))
    (case . (formal-case-indent start-block))
    (infor . (+ prev-ind formal-indent-level))
    (paramlist . (formal-paramlist-indent start-block))
    (declaration . (formal-declaration-indent start-block))
    (assignement . (+ prev-ind formal-indent-level))
    (formula . (formal-formula-indent start-block))
    (fab .(formal-fab-indent start-block) )
  ))

(defun formal-indent-line ()
  "Indent current line as a Formal statement."
  (save-excursion
    (let* ((indent-str (formal-calculate-indent))
	   (type(car indent-str))
	   (cdr-indent-str (cdr indent-str))
	   (in-first-statement-line (not (car cdr-indent-str)))
	   (start-block (if in-first-statement-line
			    (point-min)
			  (car cdr-indent-str)))
	   (end-of-prev-stat (save-excursion
			       (let ((parse-sexp-ignore-comments t))
				 (if (> (point) start-block)
				     (re-search-backward ";" start-block 'no-error))
				 (point))))
	   (prev-column)
	   (prev-ind (save-excursion
			       (goto-char start-block)
			       (setq prev-column (current-column))
			       (current-indentation)) ))
      (formal-debug-message "Type: %s " type)	; In some things indentation should not be changed 
      ;;      (if (eq type 'comment)		
      ;;	  ()				
	;; But most lines are treated this way:
	(let ((right-indent))
	  ;;	  (beginning-of-line)
	  (setq right-indent		;(+ (* (nth 2 indent-str) formal-indent-level)
				(eval (cdr (assoc type formal-indent-alist))))
	  (if (not (equal (current-indentation) right-indent))
	      (progn
		(beginning-of-line)
		(delete-horizontal-space)          
		(indent-to right-indent)))) ; )if no special treatment  for comment?
	indent-str)))
  



(defun formal-indent-comment (&optional arg)
  "Indent current line as comment.
If optional arg is non-nil, just return the
column number the line should be indented to."
  (let* ((stcol (save-excursion
		  (re-search-backward "(/*\\|--" nil t)
		  (1+ (current-column)))))
    (if arg stcol
      (delete-horizontal-space)
      (indent-to stcol))))

;  "Return the indent level that will line up several lines within the region
;from b to e nicely. The lineup string is str."
;(defun formal-get-lineup-indent (b e str)
;  (save-excursion
;    (let ((ind 0)
;	  (reg (concat str "\\|\\(\\\\)")))
;      (goto-char b)
;      ;; Get rightmost position
;      (while (< (point) e)
;	(if (re-search-forward reg (min e (formal-get-end-of-line 2)) 'move)
;	    (progn
;	      ;; Skip record blocks
;	      (if (match-beginning 1)
;		  (formal-declaration-end)
;		(progn
;		  (goto-char (match-beginning 0))
;		  (skip-chars-backward " \t")
;		  (if (> (current-column) ind)
;		      (setq ind (current-column)))
;		  (goto-char (match-end 0))
;		  (end-of-line)
;		  )))))
;      ;; In case no lineup was found
;      (if (> ind 0)
;	  (1+ ind)
;	;; No lineup-string found
;	(goto-char b)
;	(end-of-line)
;	(skip-chars-backward " \t")
;	(1+ (current-column))))))
    

;;; formal.el ends here