aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2009-11-24 11:05:36 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2009-11-24 11:05:36 +0000
commit5abc2ff937918826824352ff3e49e84f3535452d (patch)
treeefce5f9f65bf01ed7e0da9988c5b6e80cf510a92 /isar
parentaa9bd33b1850e8743d57e12e006297eda3d66100 (diff)
define isar-pr as load-time constant;
Diffstat (limited to 'isar')
-rw-r--r--isar/isar-syntax.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 408b910e..5b45eb89 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -447,7 +447,7 @@ matches contents of quotes for quoted identifiers.")
(defconst isar-undo "ProofGeneral.undo;")
-(defun isar-pr ()
+(defconst isar-pr
(if (member "ProofGeneral\\.pr"
isar-keywords-major)
"ProofGeneral.pr" ; does right thing
@@ -462,7 +462,7 @@ matches contents of quotes for quoted identifiers.")
(int-to-string i) ";"
(if linearp
(concat " "
- (isar-pr)
+ isar-pr
";"))
)
nil)) ; was proof-no-command