aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar-keywords.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-06-24 09:02:33 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-06-24 09:02:33 +0000
commit7a8fe1da30d114d34479226640af4c1ea690771c (patch)
treeb18b5262ddeb474c7e87b56fb98aec7600d7466e /isar/isar-keywords.el
parent7e930e5e35f631e79881b4ec8ff0b855e75696e6 (diff)
Fix to prevent {* being considered a command, flag edits
Diffstat (limited to 'isar/isar-keywords.el')
-rw-r--r--isar/isar-keywords.el16
1 files changed, 11 insertions, 5 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index 55d3094b..8add31c2 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -2,15 +2,17 @@
;; Keyword classification tables for Isabelle/Isar.
;; This file generated by Isabelle99-2 -- DO NOT EDIT!
;;
+;; FIXME da: THIS VERSION HAS BEEN EDITED. See ***'s below.
+;;
;; $Id$
;;
(defconst isar-keywords-major
'("\\."
"\\.\\."
- "types_code"
- "consts_code"
- "generate_code"
+ "types_code" ;; ***
+ "consts_code" ;; ***
+ "generate_code" ;; ***
"ML"
"ML_command"
"ML_setup"
@@ -159,8 +161,12 @@
"use_thy_only"
"welcome"
"with"
- "{"
- "}"))
+ ;; Next one causes {* to be recognized as a command,
+ ;; unfortunately.
+ ;; "{"
+ "{[^\\*]" ;; ***
+ "}"
+ ))
(defconst isar-keywords-minor
'("actions"