new indentation setup;

completion-table: use isar-keywords-major;

1 files changed, 17 insertions, 77 deletions

diff --git a/isar/isar.el b/isar/isar.el
index c513f4ca..1fe73c16 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -64,13 +64,6 @@
   :type 'file
   :group 'isabelle-isar)
 
-(defcustom isabelle-isar-indent 2
-  "*Indentation degree in documents"
-  :type 'number
-  :group 'isabelle-isar)
-
-(defpgdefault script-indent t)		; indentation enabled
-
 
 ;;;
 ;;; ======== Configuration of generic modes ========
@@ -109,44 +102,6 @@
 
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Indentation                                                    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun isar-stack-to-indent (stack)
-  (cond
-   ((null stack) 0)
-   ((null (car (car stack)))
-    (nth 1 (car stack)))
-   (t (let* ((col (save-excursion
-		   (goto-char (nth 1 (car stack)))
-		   (current-indentation)))
-	    (ind-col (+ isabelle-isar-indent col)))
-	(if (eq (car (car stack)) ?p)
-	    (save-excursion
-	      (move-to-column (current-indentation))
-	      (cond
-	       ((proof-looking-at isar-indent-enclose-regexp) col)
-	       ((proof-looking-at isar-indent-reset-regexp) 0)
-	       (t ind-col)))
-	  ind-col)))))
-
-(defun isar-parse-indent (c stack)
-  (cond
-   ;; toplevel / other
-   ((proof-looking-at isar-indent-reset-regexp)
-    (cons (list proof-terminal-char (point)) (list (list nil 0))))
-   ((proof-looking-at isar-indent-regexp)
-    (cons (list proof-terminal-char (point)) stack))
-   ;; open / close
-   ((proof-looking-at isar-indent-open-regexp)
-    (cons (list ?p (point)) stack))
-   ((and (proof-looking-at isar-indent-close-regexp)
-	 (eq (car (car stack)) ?p))
-    (cdr stack))
-   (t stack)))
-
-
 ;;;
 ;;; theory header
 ;;;
@@ -207,17 +162,28 @@
    proof-script-command-start-regexp (proof-regexp-alt
 				      isar-any-command-regexp
 				      (regexp-quote ";"))
-   proof-comment-start		"(*"	; comment in a proof
-   proof-comment-end		"*)"
-   proof-string-start-regexp    "\"\\|{\\*"
-   proof-string-end-regexp      "\"\\|\\*}"
+   proof-comment-start		isar-comment-start
+   proof-comment-end		isar-comment-end
+   proof-comment-start-regexp	isar-comment-start-regexp
+   proof-comment-end-regexp	isar-comment-end-regexp
+   proof-string-start-regexp    isar-string-start-regexp
+   proof-string-end-regexp      isar-string-end-regexp
    ;; Next few used for func-menu and recognizing goal..save regions in
    ;; script buffer.
    proof-save-command-regexp    isar-save-command-regexp
    proof-goal-command-regexp    isar-goal-command-regexp
    proof-goal-with-hole-regexp  isar-goal-with-hole-regexp
    proof-save-with-hole-regexp  isar-save-with-hole-regexp
-   proof-indent-commands-regexp	proof-no-regexp
+
+   proof-indent-enclose-offset  (- proof-indent)
+   proof-indent-open-offset     0
+   proof-indent-close-offset    0
+   proof-indent-any-regexp      isar-indent-any-regexp
+;   proof-indent-inner-regexp    isar-indent-inner-regexp
+   proof-indent-enclose-regexp  isar-indent-enclose-regexp
+   proof-indent-open-regexp     isar-indent-open-regexp
+   proof-indent-close-regexp    isar-indent-close-regexp
+
    ;; proof engine commands
    proof-showproof-command	"pr"
    proof-goal-command		"lemma \"%s\";"
@@ -236,8 +202,6 @@
    ;; da: for pbp.  
    ;; proof-goal-hyp-fn		'isar-goal-hyp
    proof-state-preserving-p	'isar-state-preserving-p
-   proof-parse-indent		'isar-parse-indent
-   proof-stack-to-indent	'isar-stack-to-indent
    proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list))
 
 (defun isar-shell-mode-config-set-variables ()
@@ -621,30 +585,7 @@ proof-shell-retract-files-regexp."
 ;; Ideally this could be set and adjusted automatically from the
 ;; running process.
 
-(defconst isar-all-keywords
-  (append
-   isar-keywords-major
-   isar-keywords-minor
-   isar-keywords-control
-   isar-keywords-diag
-   isar-keywords-theory-begin
-   isar-keywords-theory-switch
-   isar-keywords-theory-end
-   isar-keywords-theory-heading
-   isar-keywords-theory-decl
-   isar-keywords-theory-goal
-   isar-keywords-qed
-   isar-keywords-qed-block
-   isar-keywords-qed-global
-   isar-keywords-proof-goal
-   isar-keywords-proof-block
-   isar-keywords-proof-chain
-   isar-keywords-proof-decl
-   isar-keywords-proof-asm
-   isar-keywords-proof-asm-goal
-   isar-keywords-proof-script))
-
-(defpgdefault completion-table isar-all-keywords)
+(defpgdefault completion-table isar-keywords-major)
 
 (eval-after-load "x-symbol-isar"
  ;; Add x-symbol tokens to isar-completion-table and rebuild
@@ -658,5 +599,4 @@ proof-shell-retract-files-regexp."
     (proof-add-completions))))
 
 
-
 (provide 'isar)