diff options
| -rw-r--r-- | isa/isa.el | 17 | ||||
| -rw-r--r-- | isar/isar.el | 8 |
2 files changed, 23 insertions, 2 deletions
@@ -1,12 +1,18 @@ ;; isa.el Major mode for Isabelle proof assistant -;; Copyright (C) 1994-1998 LFCS Edinburgh. +;; Copyright (C) 1994-2000 LFCS Edinburgh, David Aspinall. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> - ;; ;; $Id$ ;; +;; ----------------------------------------------------------------- +;; +;; This file and the rest of Isabelle Proof General contain code taken +;; from David Aspinall's Isamode system, a personal project undertaken +;; 1994-1999 as a contribution to the Isabelle community. +;; +;; ----------------------------------------------------------------- ;; Add Isabelle image onto splash screen @@ -17,6 +23,13 @@ nil (proof-splash-display-image "isabelle_transparent" t))) +;; In case Isa mode was invoked directly or by -*- isa -*- at +;; the start of the file, ensure that Isa mode is used from now +;; on for .thy and .ML files. +;; FIXME: be less messy with auto-mode-alist here (remove dups) +(setq auto-mode-alist + (cons '("\\.ML$\\|\\.thy$" . isa-mode) auto-mode-alist)) + (require 'proof) (require 'isa-syntax) diff --git a/isar/isar.el b/isar/isar.el index b0275a5b..4fd72083 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -15,6 +15,14 @@ nil (proof-splash-display-image "isabelle_transparent" t))) +;; In case Isar mode was invoked directly or by -*- isar -*- at +;; the start of the file, ensure that Isar mode is used from now +;; on for .thy files. +;; FIXME: be less messy with auto-mode-alist here (remove dups) +(setq auto-mode-alist + (cons '("\\.thy$" . isar-mode) auto-mode-alist)) + + (require 'proof) (require 'isar-syntax) |