diff options
| author | David Aspinall | 2004-06-13 21:10:41 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-06-13 21:10:41 +0000 |
| commit | 557f642864feb7f1859e81365256ed192b7047ce (patch) | |
| tree | 42868584b98ea72d0e3b40349147c5b4b603b6ea | |
| parent | 7eb2222e64e25f1bd224fa5a04aba3982da0f5d4 (diff) | |
Add functions for displaying/printing draft.
| -rw-r--r-- | isar/isar.el | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el index 79a9b315..1bfc4ca3 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -371,6 +371,18 @@ proof-shell-retract-files-regexp." (proof-definvisible isar-help-theorems "print_theorems" [h t]) (proof-definvisible isar-help-trans-rules "print_trans_rules" [h T]) +;; NB: would be nice to query save first for these next two +(proof-definvisible isar-display-draft + '(format "display_drafts \"%s\"" buffer-file-name) + [(control d)]) + +(proof-definvisible isar-print-draft + '(if (y-or-n-p + (format "Print draft of file %s ?" buffer-file-name)) + (format "display_drafts \"%s\"" buffer-file-name) + (error "Aborted.")) + [(control p)]) + (defpgdefault menu-entries (append (list isabelle-logics-menu) @@ -392,7 +404,14 @@ proof-shell-retract-files-regexp." ["attributes" isar-help-attributes t] ["commands" isar-help-commands t] ["inner syntax" isar-help-syntax t] - ["methods" isar-help-methods t]))))) + ["methods" isar-help-methods t]))) + (list + ;; FIXME: these are not defined until post Isabelle2004, + ;; for now we grey them out in the menu except for CVS version. + ["Display draft" isar-display-draft + (string-match "repository" isabelle-version-string)] + ["Print draft" isar-print-draft + (string-match "repository" isabelle-version-string)]))) ;; undo proof commands (defun isar-count-undos (span) |