diff options
Diffstat (limited to 'isa')
-rw-r--r-- | isa/isa.el | 6 | ||||
-rw-r--r-- | isa/thy-mode.el | 11 |
2 files changed, 7 insertions, 10 deletions
@@ -335,12 +335,6 @@ Resulting output from Isabelle will be parsed by Proof General." ;; Next portion taken from isa-load.el ;; isa-load.el,v 3.8 1998/09/01 -(defcustom isabelle-use-sml-mode - (if (fboundp 'sml-mode) 'sml-mode) - "*If non-nil, attempt to use sml-mode in ML section of theory files." - :type 'boolean - :group 'isabelle) - (defgroup thy nil "Customization of Isamode's theory editing mode" ;; :link '(info-link "(Isamode)Theory Files") diff --git a/isa/thy-mode.el b/isa/thy-mode.el index dd0416a8..e7932068 100644 --- a/isa/thy-mode.el +++ b/isa/thy-mode.el @@ -73,9 +73,12 @@ any of the usual bracket characters in unusual ways." ("end") ("ML")) "Names of theory file sections and their templates. -Template is either a string to insert or a function. Useful functions are: +Each item in the list is a pair of a section name and a template. +A template is either a string to insert or a function. Useful functions are: thy-insert-header, thy-insert-class, thy-insert-default-sort, - thy-insert-const, thy-insert-rule" + thy-insert-const, thy-insert-rule. +The nil template does nothing. +You can add extra sections to theory files by extending this variable." :type '(repeat (cons string (choice function @@ -109,8 +112,8 @@ ML\n" "*Template for theory files. Contains a default selection of sections in a traditional order. You can use the following format characters: - %t -- replaced by theory name - %p -- replaced by names of parents, separated by +'s" + %t --- replaced by theory name + %p --- replaced by names of parents, separated by +'s" :group 'thy :type 'string) |