[nongnu] elpa/proof-general 7a28fa207a: proof-shell, pg-response: indentation fixes

[ELPA Syncer]

branch: elpa/proof-general
commit 7a28fa207a5992224c32abc988f936596f13a6b2
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>

    proof-shell, pg-response: indentation fixes
---
 generic/pg-response.el |  60 +++++++++++++--------------
 generic/proof-shell.el | 107 +++++++++++++++++++++++++------------------------
 2 files changed, 84 insertions(+), 83 deletions(-)

diff --git a/generic/pg-response.el b/generic/pg-response.el
index cd611ad946..ac1978740d 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -151,36 +151,36 @@ See ‘proof-layout-windows’ for more details about POLICY."
   (delete-other-windows)
   (switch-to-buffer b1)
   (let ((pol (proof-guess-3win-display-policy policy)))
-  (save-selected-window
-    (cond
-     ((eq pol 'hybrid)
-      (split-window-horizontally)
-      (other-window 1)
-      (switch-to-buffer b2)
-      (proof-safe-split-window-vertically) ; enlarge vertically if necessary
-      (set-window-dedicated-p (selected-window) proof-three-window-enable)
-      (other-window 1)
-      (switch-to-buffer b3)
-      (set-window-dedicated-p (selected-window) proof-three-window-enable))
-     ((eq pol 'vertical)
-      (split-window-vertically)
-      (other-window 1)
-      (switch-to-buffer b2)
-      (proof-safe-split-window-vertically) ; enlarge vertically if necessary
-      (set-window-dedicated-p (selected-window) proof-three-window-enable)
-      (other-window 1)
-      (switch-to-buffer b3)
-      (set-window-dedicated-p (selected-window) proof-three-window-enable))
-     ((eq pol 'horizontal)
-      (split-window-horizontally) ; horizontally again
-      (other-window 1)
-      (switch-to-buffer b2)
-      (enlarge-window (/ (frame-width) 6) t) ; take 2/3 of width before 
splitting again
-      (split-window-horizontally) ; horizontally again
-      (set-window-dedicated-p (selected-window) proof-three-window-enable)
-      (other-window 1)
-      (switch-to-buffer b3)
-      (set-window-dedicated-p (selected-window) proof-three-window-enable))))))
+    (save-selected-window
+      (cond
+       ((eq pol 'hybrid)
+        (split-window-horizontally)
+        (other-window 1)
+        (switch-to-buffer b2)
+        (proof-safe-split-window-vertically) ; enlarge vertically if necessary
+        (set-window-dedicated-p (selected-window) proof-three-window-enable)
+        (other-window 1)
+        (switch-to-buffer b3)
+        (set-window-dedicated-p (selected-window) proof-three-window-enable))
+       ((eq pol 'vertical)
+        (split-window-vertically)
+        (other-window 1)
+        (switch-to-buffer b2)
+        (proof-safe-split-window-vertically) ; enlarge vertically if necessary
+        (set-window-dedicated-p (selected-window) proof-three-window-enable)
+        (other-window 1)
+        (switch-to-buffer b3)
+        (set-window-dedicated-p (selected-window) proof-three-window-enable))
+       ((eq pol 'horizontal)
+        (split-window-horizontally) ; horizontally again
+        (other-window 1)
+        (switch-to-buffer b2)
+        (enlarge-window (/ (frame-width) 6) t) ; take 2/3 of width before 
splitting again
+        (split-window-horizontally) ; horizontally again
+        (set-window-dedicated-p (selected-window) proof-three-window-enable)
+        (other-window 1)
+        (switch-to-buffer b3)
+        (set-window-dedicated-p (selected-window) 
proof-three-window-enable))))))
 
 
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4de85ddf9f..e2bf02301d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1297,8 +1297,8 @@ contains only invisible elements for Prooftree 
synchronization."
                    proof-action-list)
                   ;; If the last command in proof-action-list is a "Show 
Proof" form then return t
                   (when last-command
-             (proof-shell-string-match-safe
-              proof-show-proof-diffs-regexp last-command)))))))))
+                     (proof-shell-string-match-safe
+                      proof-show-proof-diffs-regexp last-command)))))))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)
@@ -1780,58 +1780,59 @@ i.e., 'goals or 'response."
   (let ((start proof-shell-delayed-output-start)
        (end   proof-shell-delayed-output-end)
        (flags proof-shell-delayed-output-flags))
-  (goto-char start)
-  (cond
-   ((and proof-shell-start-goals-regexp
-        (proof-re-search-forward proof-shell-start-goals-regexp end t))
-     (let* ((gmark  (match-beginning 0)) ; start of goals message
-           (gstart (or (match-end 1)    ; start of actual display
-                       gmark))
-           (rstart start)               ; possible response before goals
-           (gend   end)
-           both)                        ; flag for response+goals
-
-       (goto-char gstart)
-       (while (re-search-forward proof-shell-start-goals-regexp end t)
-        (setq gmark (match-beginning 0))
-        (setq gstart (or (match-end 1) gmark))
-        (setq gend
-              (if (and proof-shell-end-goals-regexp
-                       (re-search-forward proof-shell-end-goals-regexp end t))
-                  (progn
-                    (setq rstart (match-end 0))
-                    (match-beginning 0))
-                end)))
-       (setq proof-shell-last-goals-output
-            (buffer-substring-no-properties gstart gend))
-
-       ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp [is it 
needed?]
-       (setq both
-            (> (- gmark rstart) 4))
-       (if both
-          (proof-shell-display-output-as-response
-           flags
-           (buffer-substring-no-properties rstart gmark)))
-       ;; display goals output second so it persists in 2-pane mode
-       (unless (memq 'no-goals-display flags)
-        (pg-goals-display proof-shell-last-goals-output both))
-       ;; indicate a goals output has been given
-       'goals))
-
-   (t
-    (proof-shell-display-output-as-response flags proof-shell-last-output)
-    ;; indicate that (only) a response output has been given
-    'response))
+    (goto-char start)
+    (cond
+     ((and proof-shell-start-goals-regexp
+          (proof-re-search-forward proof-shell-start-goals-regexp end t))
+      (let* ((gmark  (match-beginning 0)) ; start of goals message
+            (gstart (or (match-end 1)    ; start of actual display
+                        gmark))
+            (rstart start)              ; possible response before goals
+            (gend   end)
+            both)                       ; flag for response+goals
+
+        (goto-char gstart)
+        (while (re-search-forward proof-shell-start-goals-regexp end t)
+         (setq gmark (match-beginning 0))
+         (setq gstart (or (match-end 1) gmark))
+         (setq gend
+               (if (and proof-shell-end-goals-regexp
+                        (re-search-forward proof-shell-end-goals-regexp end t))
+                   (progn
+                     (setq rstart (match-end 0))
+                     (match-beginning 0))
+                 end)))
+        (setq proof-shell-last-goals-output
+             (buffer-substring-no-properties gstart gend))
+
+        ;; FIXME heuristic: 4 allows for annotation in
+        ;; end-goals-regexp [is it needed?]
+        (setq both
+             (> (- gmark rstart) 4))
+        (if both
+           (proof-shell-display-output-as-response
+            flags
+            (buffer-substring-no-properties rstart gmark)))
+        ;; display goals output second so it persists in 2-pane mode
+        (unless (memq 'no-goals-display flags)
+         (pg-goals-display proof-shell-last-goals-output both))
+        ;; indicate a goals output has been given
+        'goals))
+
+     (t
+      (proof-shell-display-output-as-response flags proof-shell-last-output)
+      ;; indicate that (only) a response output has been given
+      'response))
   
-  ;; FIXME (CPC 2015-12-31): The documentation of this hook suggests that it
-  ;; only gets run after new output has been displayed, but this isn't true at
-  ;; the moment: indeed, it gets run even for invisible commands.
-  ;;
-  ;; This causes issues in company-coq, where completion uses invisible
-  ;; commands to display the types of completion candidates; this causes the
-  ;; goals and response buffers to scroll. I fixed it by adding checks to
-  ;; coq-mode's hooks, but maybe we should do more.
-  (run-hooks 'proof-shell-handle-delayed-output-hook)))
+    ;; FIXME (CPC 2015-12-31): The documentation of this hook suggests that it
+    ;; only gets run after new output has been displayed, but this isn't true 
at
+    ;; the moment: indeed, it gets run even for invisible commands.
+    ;;
+    ;; This causes issues in company-coq, where completion uses invisible
+    ;; commands to display the types of completion candidates; this causes the
+    ;; goals and response buffers to scroll. I fixed it by adding checks to
+    ;; coq-mode's hooks, but maybe we should do more.
+    (run-hooks 'proof-shell-handle-delayed-output-hook)))