isar-keywords-theory-enclose: removed isar-keywords-theory-switch, which usually appears locally as plain theory command;

isar-keywords-proper: simplified font-lock;
added isar-match-nesting -- distinguishes font-lock for local vs. global begin/end;

1 files changed, 92 insertions, 60 deletions

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 19d95716..63fe4db4 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -3,7 +3,7 @@
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; Authors:     David Aspinall <David.Aspinall@ed.ac.uk>
-;;		Markus Wenzel
+;;              Markus Wenzel
 ;; Maintainer:  Gerwin Klein <kleing@in.tum.de>
 ;;
 ;; $Id$
@@ -15,31 +15,31 @@
 
 ;; ----- character syntax
 
-(defconst isar-script-syntax-table-entries 
+(defconst isar-script-syntax-table-entries
   (append
        '(?\$ "."
-	 ?\/ "."
-	 ?\\ "\\"
-	 ?+  "."
-	 ?-  "."
-	 ?=  "."
-	 ?%  "."
-	 ?<  "w"
-	 ?>  "w"
-	 ?\& "."
-	 ?.  "w"
-	 ?_  "w"
-	 ?\' "w"
-	 ??  "w"
-	 ?`  "\""
-	 ?\( "()1"
-	 ?\) ")(4")
+         ?\/ "."
+         ?\\ "\\"
+         ?+  "."
+         ?-  "."
+         ?=  "."
+         ?%  "."
+         ?<  "w"
+         ?>  "w"
+         ?\& "."
+         ?.  "w"
+         ?_  "w"
+         ?\' "w"
+         ??  "w"
+         ?`  "\""
+         ?\( "()1"
+         ?\) ")(4")
    (cond
     (proof-running-on-XEmacs
      ;; We classify {* sequences *} as comments, although
      ;; they need to be passed as command args as text.
      ;; NB: adding a comment sequence b seems to break
-     ;; buffer-syntactic-context, best to use emulated 
+     ;; buffer-syntactic-context, best to use emulated
      ;; version.
     '(?\{ "(}5"
       ?\} "){8"
@@ -59,7 +59,7 @@ This list is in the right format for proof-easy-config.")
 (defconst isar-script-syntax-table-alist
   ;; NB: this is used for imenu.  Probably only need word syntax
   (let ((syn isar-script-syntax-table-entries)
-	al)
+        al)
     (while syn
       (setq al (cons (cons (char-to-string (car syn)) (cadr syn)) al))
       (setq syn (cddr syn)))
@@ -69,7 +69,7 @@ This list is in the right format for proof-easy-config.")
   "Set appropriate values for syntax table in current buffer."
   (let ((syn isar-script-syntax-table-entries))
     (while syn
-      (modify-syntax-entry 
+      (modify-syntax-entry
        (car syn) (cadr syn))
       (setq syn (cddr syn)))))
 
@@ -89,9 +89,11 @@ This list is in the right format for proof-easy-config.")
 
 ;; ----- keyword groups
 
+(defconst isar-keyword-begin "begin")
+(defconst isar-keyword-end "end")
+
 (defconst isar-keywords-theory-enclose
   (append isar-keywords-theory-begin
-          isar-keywords-theory-switch
           isar-keywords-theory-end))
 
 (defconst isar-keywords-theory
@@ -112,7 +114,7 @@ This list is in the right format for proof-easy-config.")
 
 (defconst isar-keywords-proof
   (append isar-keywords-proof-heading
-	  isar-keywords-proof-goal
+          isar-keywords-proof-goal
           isar-keywords-proof-chain
           isar-keywords-proof-decl
           isar-keywords-qed))
@@ -125,9 +127,15 @@ This list is in the right format for proof-easy-config.")
   (append isar-keywords-proof-goal
           isar-keywords-proof-asm-goal))
 
+(defconst isar-keywords-proper
+  (append isar-keywords-theory
+          isar-keywords-theory-switch
+          isar-keywords-proof-enclose
+          isar-keywords-proof))
+
 (defconst isar-keywords-improper
   (append isar-keywords-theory-script
-	  isar-keywords-proof-script
+          isar-keywords-proof-script
           isar-keywords-qed-global))
 
 (defconst isar-keywords-outline
@@ -154,7 +162,7 @@ This list is in the right format for proof-easy-config.")
   (append isar-keywords-proof-block
           isar-keywords-proof-close
           isar-keywords-qed-block
-	  '("begin")))
+          (list isar-keyword-begin)))
 
 
 ;; ----- regular expressions
@@ -175,17 +183,17 @@ This list is in the right format for proof-easy-config.")
 ;; maybe use separate functions?
 
 ;; DA: this goes wrong for { and } in fact, because plain { and } in
-;; `proof-script-command-start-regexp' also match with {* and *}, which 
+;; `proof-script-command-start-regexp' also match with {* and *}, which
 ;; should not be considered as commands (breaks new parser).
 ;; For now, we revert to old parser and old form of this function.
 
-(defun isar-ids-to-regexp (l) 
+(defun isar-ids-to-regexp (l)
   "Maps a non-empty list of tokens `l' to a regexp matching all elements"
   (let* ((special (remove-if-not (lambda (s) (string-match "{\\|}" s)) l))
          (normal (remove-if (lambda (s) (string-match "{\\|}" s)) l))
          (s-reg (isar-regexp-simple-alt special))
          (n-reg (concat "\\<\\(?:" (isar-regexp-simple-alt normal) "\\)\\>")))
-    (cond 
+    (cond
      ((null special) n-reg)
      ((null normal) s-reg)
      (t (concat n-reg "\\|" s-reg)))))
@@ -194,23 +202,23 @@ This list is in the right format for proof-easy-config.")
 ; (isar-ids-to-regexp '("bla" "blubber"))
 ; (isar-ids-to-regexp '("bla" "\\." "blubber"))
 ; (isar-ids-to-regexp '("bla" "\\." "blubber" "{"))
-              
+
 
 ;;
-;; Alternative version with attempt to work for new parser (unfinished) 
+;; Alternative version with attempt to work for new parser (unfinished)
 ;  (mapconcat
-;   (lambda (s) (if (proof-string-match "^\\W$" s) 
-;		   ;; was just s 
-;		   (cond 
-;		    ;; FIXME: what we really want here is to match { or }
-;		    ;; _except_ when followed/preceded by *, but not to
-;		    ;; consider * as part of match.  (Exclude punctuation??)
-;		    ;; That kind of construct is only allowed for whitespace,
-;		    ;; though.
-;		    ((string-equal s "{")  "{[^\*]")
-;		    ((string-equal s "}")  "[^\*]}") ;; FIXME wrong
-;		    (t			   s)) ; what else?
-;		   (concat "\\<" s "\\>")))
+;   (lambda (s) (if (proof-string-match "^\\W$" s)
+;                  ;; was just s
+;                  (cond
+;                   ;; FIXME: what we really want here is to match { or }
+;                   ;; _except_ when followed/preceded by *, but not to
+;                   ;; consider * as part of match.  (Exclude punctuation??)
+;                   ;; That kind of construct is only allowed for whitespace,
+;                   ;; though.
+;                   ((string-equal s "{")  "{[^\*]")
+;                   ((string-equal s "}")  "[^\*]}") ;; FIXME wrong
+;                   (t                     s)) ; what else?
+;                  (concat "\\<" s "\\>")))
 ;   l "\\|"))
 
 (defconst isar-ext-first "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z]\\)")
@@ -261,13 +269,40 @@ matches contents of quotes for quoted identifiers.")
 
 ;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
 ;; incomplete antiquotations like @{text bla"} (even though it is supposed to
-;; stop at eol anyway). 
+;; stop at eol anyway).
 
 (defconst isar-antiq-regexp
   (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
   "Regexp matching Isabelle/Isar antiquoations.")
 
 
+;; keyword nesting
+
+(defconst isar-nesting-regexp
+  (isar-ids-to-regexp (list isar-keyword-begin isar-keyword-end)))
+
+(defun isar-nesting ()
+  "Determine keyword nesting"
+  (let ((nesting 0) (limit (point)))
+    (save-excursion
+      (goto-char (point-min))
+      (while (proof-re-search-forward isar-nesting-regexp limit t)
+        (cond
+         ((proof-buffer-syntactic-context))
+         ((equal (match-string 0) isar-keyword-begin) (incf nesting))
+         ((equal (match-string 0) isar-keyword-end) (decf nesting)))))
+    nesting))
+
+(defun isar-match-nesting (limit)
+  (block nil
+    (while (proof-re-search-forward isar-nesting-regexp limit t)
+      (and (not (proof-buffer-syntactic-context))
+	   (if (equal (match-string 0) isar-keyword-begin)
+	       (> (isar-nesting) 1)
+	     (> (isar-nesting) 0))
+	   (return t)))))
+
+
 ;; ----- Isabelle inner syntax hilite
 
 (defface isabelle-class-name-face
@@ -337,6 +372,7 @@ matches contents of quotes for quoted identifiers.")
 (defconst isabelle-bound-name-face 'isabelle-bound-name-face)
 (defconst isabelle-var-name-face   'isabelle-var-name-face)
 
+
 (defconst isar-font-lock-local
   '("\\(\\\\<\\^loc>\\)\\(\\\\+<[A-Za-z]+>\\|.\\)"
     (1 x-symbol-invisible-face t)
@@ -344,13 +380,12 @@ matches contents of quotes for quoted identifiers.")
 
 (defvar isar-font-lock-keywords-1
   (list
+   (cons 'isar-match-nesting                               'font-lock-preprocessor-face)
    (cons (isar-ids-to-regexp isar-keywords-minor)          'font-lock-type-face)
    (cons (isar-ids-to-regexp isar-keywords-control)        'proof-error-face)
    (cons (isar-ids-to-regexp isar-keywords-diag)           'proof-tacticals-name-face)
    (cons (isar-ids-to-regexp isar-keywords-theory-enclose) 'font-lock-type-face)
-   (cons (isar-ids-to-regexp isar-keywords-theory)         'font-lock-keyword-face)
-   (cons (isar-ids-to-regexp isar-keywords-proof-enclose)  'font-lock-preprocessor-face)
-   (cons (isar-ids-to-regexp isar-keywords-proof)          'font-lock-keyword-face)
+   (cons (isar-ids-to-regexp isar-keywords-proper)         'font-lock-keyword-face)
    (cons (isar-ids-to-regexp isar-keywords-proof-context)  'proof-declaration-name-face)
    (cons (isar-ids-to-regexp isar-keywords-improper)       'font-lock-reference-face)
    (cons isar-improper-regexp 'font-lock-reference-face)
@@ -416,7 +451,7 @@ matches contents of quotes for quoted identifiers.")
 
 ;; ----- variations on undo
 
-(defconst isar-undo "ProofGeneral.undo;")  ;; no output undo 
+(defconst isar-undo "ProofGeneral.undo;")  ;; no output undo
 
 (defun isar-remove (name)
   (concat "init_toplevel; kill_thy " name ";"))
@@ -432,10 +467,7 @@ matches contents of quotes for quoted identifiers.")
   (proof-anchor-regexp
    (isar-ids-to-regexp
     (append isar-keywords-theory-begin
-	    isar-keywords-theory-switch))))
-
-(defconst isar-begin-regexp
-  (isar-ids-to-regexp '("begin")))  ;; no anchor!
+            isar-keywords-theory-switch))))
 
 (defconst isar-end-regexp
   (proof-anchor-regexp
@@ -475,19 +507,19 @@ matches contents of quotes for quoted identifiers.")
 (defconst isar-next-entity-regexps
   (list isar-any-entity-regexp
         (list isar-named-entity-regexp '(1 3))))
-;; da: I've removed unnamed entities, they clutter the menu 
+;; da: I've removed unnamed entities, they clutter the menu
 ;; NB: to add back, need ? at end of isar-any-entity-regexp
-;;	(list isar-unnamed-entity-regexp 1)))
+;;      (list isar-unnamed-entity-regexp 1)))
 ;; Might also remove heading
 
 (defconst isar-generic-expression
-  (mapcar (lambda (kw) 
-	    (list (capitalize kw)
-		  (concat "\\<" kw "\\>"
-			  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-			  isar-name-regexp "[[:=]")
-		  1))
-	  isar-keywords-fume))
+  (mapcar (lambda (kw)
+            (list (capitalize kw)
+                  (concat "\\<" kw "\\>"
+                          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+                          isar-name-regexp "[[:=]")
+                  1))
+          isar-keywords-fume))
 
 ;; ----- indentation