* Final overhaul including proper sorting.

src/run_spat-print_entities.adb

@@ -17,7 +17,10 @@ pragma License (Unrestricted);
 
 with Ada.Text_IO;
 
+with SPAT.Entity.Tree;
 with SPAT.Log;
+with SPAT.Proof_Attempt;
+with SPAT.Proof_Item;
 with SPAT.Strings;
 
 separate (Run_SPAT)
@@ -58,48 +61,74 @@ begin
               "/" & Image (Value => Info.Total_Proof_Time (Entity => Entity)));
 
          if SPAT.Command_Line.Details.Get then
-            for P of Info.Proof_List (Entity => Entity) loop
-               if
-                 Report_All                                   or else
-                 (Failed_Only and then P.Has_Failed_Attempts) or else
-                 (Unproved_Only and then P.Has_Unproved_Attempts)
-               then
-                  SPAT.Log.Message
-                    (Message =>
-                       "`-" & SPAT.To_String (P.Rule) & " " & P.Image &
-                       " => " & Image (P.Max_Time) & "/" &
-                       Image (P.Total_Time));
+            for PI_Position in Info.Proof_Tree (Entity => Entity) loop
+               declare
+                  The_Proof : SPAT.Proof_Item.T'Class renames
+                    SPAT.Proof_Item.T'Class
+                      (SPAT.Entity.Tree.Element (Position => PI_Position));
+               begin
+                  if
+                    Report_All                                           or else
+                    (Failed_Only and then The_Proof.Has_Failed_Attempts) or else
+                    (Unproved_Only and then The_Proof.Has_Unproved_Attempts)
+                  then
+                     SPAT.Log.Message
+                       (Message =>
+                          "`-" & SPAT.To_String (The_Proof.Rule) & " " &
+                          The_Proof.Image & " => " &
+                          Image (The_Proof.Max_Time) & "/" &
+                          Image (The_Proof.Total_Time));
 
-                  for Check of P.Check_Tree loop
-                     if
-                       Report_All                                       or else
-                       (Failed_Only and then Check.Has_Failed_Attempts) or else
-                       (Unproved_Only and then Check.Is_Unproved)
-                     then
-                        Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
-                                             To   => 2);
-                        SPAT.Log.Message (Message  => "`",
-                                          New_Line => False);
+                     for Check_Position in
+                       Info.Iterate_Children (Entity   => Entity,
+                                              Position => PI_Position)
+                     loop
+                        declare
+                           The_Check : SPAT.Proof_Item.Checks_Sentinel'Class renames
+                             SPAT.Proof_Item.Checks_Sentinel'Class
+                               (SPAT.Entity.Tree.Element (Position => Check_Position));
+                        begin
+                           if
+                             Report_All                                           or else
+                             (Failed_Only and then The_Check.Has_Failed_Attempts) or else
+                             (Unproved_Only and then The_Check.Is_Unproved)
+                           then
+                              Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
+                                                   To   => 2);
+                              SPAT.Log.Message (Message  => "`",
+                                                New_Line => False);
 
-                        for A of Check loop
-                           Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
-                                                To   => 3);
-                           SPAT.Log.Message
-                             (Message =>
-                                "-" & SPAT.To_String (A.Prover) & ": " &
-                                Image (A.Time) &
-                                " (" & SPAT.To_String (A.Result) & ")");
-                        end loop;
-                     end if;
-                  end loop;
+                              for Attempt_Position in
+                                Info.Iterate_Children (Entity   => Entity,
+                                                       Position => Check_Position)
+                              loop
+                                 declare
+                                    The_Attempt : SPAT.Proof_Attempt.T'Class renames
+                                      SPAT.Proof_Attempt.T'Class
+                                        (SPAT.Entity.Tree.Element
+                                           (Position => Attempt_Position));
+                                 begin
+                                    Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output,
+                                                         To   => 3);
+                                    SPAT.Log.Message
+                                      (Message =>
+                                         "-" & SPAT.To_String (The_Attempt.Prover) & ": " &
+                                         Image (The_Attempt.Time) &
+                                         " (" & SPAT.To_String (The_Attempt.Result) & ")");
+                                 end;
+                              end loop;
+                           end if;
+                        end;
+                     end loop;
 
-                  if P.Suppressed /= SPAT.Null_Name then
-                     SPAT.Log.Message
-                       (Message =>
-                          "Justified with: """ & SPAT.To_String (P.Suppressed) &
-                          """.");
+                     if The_Proof.Suppressed /= SPAT.Null_Name then
+                        SPAT.Log.Message
+                          (Message =>
+                             "Justified with: """ &
+                             SPAT.To_String (The_Proof.Suppressed) & """.");
+                     end if;
                   end if;
-               end if;
+               end;
             end loop;
          end if;
       end if;

src/run_spat.adb

@@ -149,8 +149,6 @@ begin
                end Parse_JSON_File;
             end loop;
 
-            Info.Update; --  Update internal caches.
-
             SPAT.Log.Debug
               (Message =>
                  "Reading completed in " &

src/spat-entity-tree.ads

@@ -28,10 +28,17 @@ package SPAT.Entity.Tree is
 
    type T is new Implementation.Trees.Tree with private;
 
+   subtype Forward_Iterator is
+     Implementation.Trees.Tree_Iterator_Interfaces.Forward_Iterator;
+
    subtype Cursor is Implementation.Trees.Cursor;
 
    No_Element : Cursor renames Implementation.Trees.No_Element;
 
+   function "=" (Left  : in Cursor;
+                 Right : in Cursor) return Boolean
+                 renames Implementation.Trees."=";
+
    function Child_Count (Parent : in Cursor) return Ada.Containers.Count_Type
                          renames Implementation.Trees.Child_Count;
 
@@ -41,12 +48,21 @@ package SPAT.Entity.Tree is
    function First_Child (Position : in Cursor) return Cursor
                          renames Implementation.Trees.First_Child;
 
+   function Last_Child (Position : in Cursor) return Cursor
+                        renames Implementation.Trees.Last_Child;
+
    function Next_Sibling (Position : in Cursor) return Cursor
                           renames Implementation.Trees.Next_Sibling;
 
    procedure Next_Sibling (Position : in out Cursor)
                            renames Implementation.Trees.Next_Sibling;
 
+   function Previous_Sibling (Position : in Cursor) return Cursor
+                              renames Implementation.Trees.Previous_Sibling;
+
+   procedure Previous_Sibling (Position : in out Cursor)
+                               renames Implementation.Trees.Previous_Sibling;
+
 private
 
    type T is new Implementation.Trees.Tree with null record;

src/spat-entity.ads

@@ -19,6 +19,8 @@ package SPAT.Entity is
 
    type T is abstract tagged private;
 
+   function Image (This : in T) return String is abstract;
+
 private
 
    type T is abstract tagged null record;

src/spat-entity_line.adb

@@ -22,7 +22,8 @@ package body SPAT.Entity_Line is
    ---------------------------------------------------------------------------
    --  Image
    ---------------------------------------------------------------------------
-   not overriding function Image (This : T) return String is
+   overriding
+   function Image (This : T) return String is
    begin
       return
         To_String (This.File) & ":" &

src/spat-entity_line.ads

@@ -47,7 +47,7 @@ package SPAT.Entity_Line is
    ---------------------------------------------------------------------------
    --  Image
    ---------------------------------------------------------------------------
-   not overriding
+   overriding
    function Image (This : T) return String;
 
    ---------------------------------------------------------------------------

src/spat-flow_item.adb

@@ -47,6 +47,8 @@ package body SPAT.Flow_Item is
       The_List.Sort_By_Location;
 
       --  Update the elements in the Tree.
+      --  FIXME: For now this works, because the structure here is just a list,
+      --         if it were an actual tree we would mix up parent and children.
       declare
          Position : Entity.Tree.Cursor :=
            Entity.Tree.First_Child (Position => Parent);

src/spat-proof_attempt.ads

@@ -15,6 +15,7 @@ pragma License (Unrestricted);
 --
 ------------------------------------------------------------------------------
 
+private with Ada.Tags;
 with SPAT.Entity;
 with SPAT.Field_Names;
 with SPAT.Preconditions;
@@ -89,6 +90,13 @@ private
          --  Steps -- part of the JSON data, but we don't care.
       end record;
 
+   overriding
+   function Image (This : in T) return String is
+     (Ada.Tags.External_Tag (T'Class (This)'Tag) & ": (" &
+        "Prover => " & To_String (This.Prover) &
+        ", Result => " & To_String (This.Result) &
+        ", Time => " & This.Time'Image & ")");
+
    Trivial_True : constant T := T'(Entity.T with
                                      Prover => To_Name ("Trivial"),
                                      Result => To_Name ("Valid"),