Improvements to support: needs work in segment-up-to, though.

1 files changed, 128 insertions, 6 deletions

diff --git a/twelf/twelf.el b/twelf/twelf.el
index 1ce03049..77730b00 100644
--- a/twelf/twelf.el
+++ b/twelf/twelf.el
@@ -8,13 +8,18 @@
 ;;
 ;;
 
+;; FIXME: PG needs a bit of tuning to get this to work 
+;; properly, because of mixed syntax for comments.
+
+;; We should introduce a proof-parse-to-next-command 
+;; configurable setting, perhaps, which should skip
+;; comments automatically.  
+
 (require 'proof-easy-config)            ; easy configure mechanism
 
-;; (require 'twelf-font)		; font lock configuration
+(require 'twelf-font)			; font lock configuration
 ;; (require 'twelf-old)			; port of parts of old code
-
-;; FIXME: almost working, must modify syntax table so that comments
-;; are recognized properly.
+;; FIXME: put parts of old code into twelf-syntax or similar
 
 (proof-easy-config 
  'twelf "Twelf" 
@@ -24,8 +29,8 @@
  proof-shell-auto-terminate-commands nil ; server commands don't end with .
 
  ;; FIXME: must also cope with single line comments beginning with %
- proof-comment-start             "%{"
- proof-comment-end               "}%"
+ proof-comment-start             "%{\\|^%"
+ proof-comment-end               "}%\\|^%.*\n"
  proof-comment-start-regexp	 "%[%{\t\n\f]"
  proof-comment-end		 ""
 
@@ -62,4 +67,121 @@
  ;;"^\\[opening \\|^###\\|^Reading")
  )
 
+
+;;
+;; Syntax table
+;;
+
+;; Taken from old Emacs mode, renamed fns to be convention compliant
+(defun twelf-set-syntax (char entry)
+  (modify-syntax-entry char entry twelf-mode-syntax-table))
+(defun twelf-set-word  (char) (twelf-set-syntax char "w   "))
+(defun twelf-set-symbol (char) (twelf-set-syntax char "_   "))
+
+(defun twelf-map-string (func string)
+  (if (string= "" string)
+      ()
+    (funcall func (string-to-char string))
+    (twelf-map-string func (substring string 1))))
+
+;; A-Z and a-z are already word constituents
+;; For fontification, it would be better if _ and ' were word constituents
+(twelf-map-string 
+ 'twelf-set-word "!&$^+/<=>?@~|#*`;,-0123456789\\") ; word constituents
+(twelf-map-string 'twelf-set-symbol "_'")         ; symbol constituents
+;; Delimited comments are %{ }%, see 1234 below.
+(twelf-set-syntax ?\ "    ")            ; whitespace
+(twelf-set-syntax ?\t "    ")           ; whitespace
+(twelf-set-syntax ?% "< 14")            ; comment begin
+(twelf-set-syntax ?\n ">   ")           ; comment end
+(twelf-set-syntax ?: ".   ")            ; punctuation
+(twelf-set-syntax ?. ".   ")            ; punctuation
+(twelf-set-syntax ?\( "()  ")           ; open delimiter
+(twelf-set-syntax ?\) ")(  ")           ; close delimiter
+(twelf-set-syntax ?\[ "(]  ")           ; open delimiter
+(twelf-set-syntax ?\] ")[  ")           ; close delimiter
+(twelf-set-syntax ?\{ "(}2 ")           ; open delimiter
+(twelf-set-syntax ?\} "){ 3")           ; close delimiter
+;; Actually, strings are illegal but we include:
+(twelf-set-syntax ?\" "\"   ")          ; string quote
+;; \ is not an escape, but a word constituent (see above)
+;;(twelf-set-syntax ?\\ "/   ")         ; escape
+
+
+
+;;
+;; Syntax highlighting (from twelf-old.el, needs work)
+;;
+
+;; Automatically highlight Twelf sources using font-lock
+;; (FIXME: this is not so good, should work with font-lock properly!)
+(require 'twelf-font)
+(add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer)
+
+(defun twelf-current-decl ()
+  "Returns list (START END COMPLETE) for current Twelf declaration.
+This should be the declaration or query under or just before
+point within the nearest enclosing blank lines.
+If declaration ends in `.' then COMPLETE is t, otherwise nil."
+  (let (par-start par-end complete)
+    (save-excursion
+      ;; Skip backwards if between declarations
+      (if (or (eobp) (looking-at (concat "[" *whitespace* "]")))
+          (skip-chars-backward (concat *whitespace* ".")))
+      (setq par-end (point))
+      ;; Move forward from beginning of decl until last
+      ;; declaration before par-end is found.
+      (if (not (bobp)) (backward-paragraph 1))
+      (setq par-start (point))
+      (while (and (twelf-end-of-par par-end)
+                  (< (point) par-end))
+        (setq par-start (point)))
+      ;; Now par-start is at end of preceding declaration or query.
+      (goto-char par-start)
+      (skip-twelf-comments-and-whitespace)
+      (setq par-start (point))
+      ;; Skip to period or consective blank lines
+      (setq complete (twelf-end-of-par))
+      (setq par-end (point)))
+    (list par-start par-end complete)))
+
+(defun twelf-next-decl (filename error-buffer)
+  "Set point after the identifier of the next declaration.
+Return the declared identifier or `nil' if none was found.
+FILENAME and ERROR-BUFFER are used if something appears wrong."
+  (let ((id nil)
+        end-of-id
+	beg-of-id)
+    (skip-twelf-comments-and-whitespace)
+    (while (and (not id) (not (eobp)))
+      (setq beg-of-id (point))
+      (if (zerop (skip-chars-forward *twelf-id-chars*))
+          ;; Not looking at id: skip ahead
+          (skip-ahead filename (current-line-absolute) "No identifier"
+                      error-buffer)
+        (setq end-of-id (point))
+        (skip-twelf-comments-and-whitespace)
+        (if (not (looking-at ":"))
+            ;; Not looking at valid decl: skip ahead
+            (skip-ahead filename (current-line-absolute end-of-id) "No colon"
+                        error-buffer)
+          (goto-char end-of-id)
+          (setq id (buffer-substring beg-of-id end-of-id))))
+      (skip-twelf-comments-and-whitespace))
+    id))
+
+(defconst twelf-syntax-menu
+  '("Syntax Highlighting"
+    ["Highlight Declaration" twelf-font-fontify-decl t]
+    ["Highlight Buffer" twelf-font-fontify-buffer t]
+    ;;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate
+    ;;'font-lock-mode))
+      )
+  "Menu for syntax highlighting in Twelf mode.")
+
+(defpgdefault menu-entries
+  (cdr twelf-syntax-menu))
+
+  
+
 (provide 'twelf)
\ No newline at end of file