diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2002-05-10 12:43:18 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2002-05-10 12:43:18 +0000 |
| commit | 4f84c294f44913ebd291539b583f085db75ec240 (patch) | |
| tree | 11f4f044c406eb1725c1c6a3b0fc28398fcca90a /isar | |
| parent | b9841b21c21c4bee30cf1f008bd1e475f49faf88 (diff) | |
tuned isar-strip-terminators;
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el index c2aa847d..b7829822 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -92,7 +92,9 @@ (goto-char (point-min)) (while (search-forward ";" (point-max) t) (if (not (proof-buffer-syntactic-context)) - (delete-backward-char 1))))) + (progn + (delete-backward-char 1) + (or (proof-looking-at ";\\|\s-\\|$") (insert " "))))))) (defun isar-markup-ml (string) |