From 01248339f4f18cc1635b591447d343a1b4565a80 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 28 Jul 2015 14:13:15 +0200
Subject: ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix
 #4308)

---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 8af1aaafdc..de8752f41d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2451,7 +2451,7 @@ let get_script prf =
   let branch, test =
     match prf with
     | None -> VCS.Branch.master, fun _ -> true
-    | Some name -> VCS.current_branch (),  List.mem name in
+    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
   let rec find acc id =
     if Stateid.equal id Stateid.initial ||
        Stateid.equal id Stateid.dummy then acc else
@@ -2462,7 +2462,9 @@ let get_script prf =
     | `Sideff (`Ast (x,_)) ->
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
     | `Sideff (`Id id)  -> find acc id
-    | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd _ -> find acc view.next
     | `Alias (id,_) -> find acc id
     | `Fork _ -> find acc view.next
     in
-- 
cgit v1.2.3