aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-07-17 12:23:14 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-07-17 12:23:14 +0000
commitffbb9e2856a3e8f2afa497f3ba102319d91671f8 (patch)
treebeb644f681580dafd5a35172e8165eab90fecf45 /isa
parent3dfd6b8f0e96deac9584f7e054344ad1128609d8 (diff)
Support subterm help facility (not quite working)
Diffstat (limited to 'isa')
-rw-r--r--isa/isa.el6
1 files changed, 5 insertions, 1 deletions
diff --git a/isa/isa.el b/isa/isa.el
index cb4c9481..1f6ef2e6 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -218,7 +218,11 @@ and script mode."
pg-subterm-anns-use-stack t
pg-subterm-start-char ?\372
pg-subterm-sep-char ?\373
- pg-subterm-end-char ?\374
+ pg-subterm-end-char ?\374
+ pg-before-subterm-markup-hook 'isabelle-convert-idmarkup-to-subterm
+ ;'pg-remove-specials
+ ;; FIXME: next one doesn't do quite the right thing, always returns 'a?
+ pg-subterm-help-cmd "printyp (type_of (read \"%s\"))"
;; === MULTIPLE FILE HANDLING ===
proof-shell-process-file