diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-26 13:00:03 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-26 13:00:03 +0000 |
| commit | 6f8bee51a431528f6c3d8b508538d30ea3b3023a (patch) | |
| tree | 8057c88a488a49a4990c8096ac65efbdb82e3702 /isar/isar-syntax.el | |
| parent | 1b12b1be9ca41f80f58ae1ca8aaf3198d29d0d9a (diff) | |
Add pr to print state in case of linear_undo. See Trac #292.
Still not ideal: when there is no proof state, we'd prefer
that an empty goal screen is displayed.
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 7bd45aa9..1f7d3ea6 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -1,5 +1,5 @@ ;; isar-syntax.el Syntax expressions for Isabelle/Isar -;; Copyright (C) 1994-2004 LFCS Edinburgh. +;; Copyright (C) 1994-2004, 2009 LFCS Edinburgh. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> @@ -479,7 +479,8 @@ matches contents of quotes for quoted identifiers.") (defun isar-undos (linearp i) (if (> i 0) (concat (if linearp "linear_undo " "undos_proof ") - (int-to-string i) ";") + (int-to-string i) ";" + (if linearp " pr; ")) ; See Trac #292 nil)) ; was proof-no-command (defun isar-cannot-undo (cmd) |