Improve coverage reporting for partially covered expressions

I wanted to parse TLC coverage information to render a coverage report, but I realized that I didn't understand some parts of the TLC output.

I see that coverage statistics doesn't mention some parts of TLA+ source files. For example:

---- MODULE X ----

VARIABLE x

Init == x = 0

A1 == 
    /\ IF FALSE 
       THEN x /= 2
       ELSE TRUE
    /\ x' = 2

Next ==
    \/ A1
    \/ IF FALSE 
        THEN A1
        ELSE UNCHANGED x

Spec == Init /\ [][Next]_x
====

For this specification I got following statistics:

<Init line 5, col 1 to line 5, col 4 of module X>: 1:1
  line 5, col 9 to line 5, col 13 of module X: 1
<A1 line 7, col 1 to line 7, col 2 of module X>: 1:2
  line 8, col 5 to line 11, col 13 of module X: 2
<Next line 13, col 1 to line 13, col 4 of module X (15 8 17 24)>: 0:2
  line 15, col 11 to line 15, col 15 of module X: 2
  line 11, col 8 to line 11, col 13 of module X: 0
  line 17, col 14 to line 17, col 24 of module X: 2

1. Next itself and its first disjunct are not in the statistics. Spec line is also missing. Is there an easy way to understand in what cases missing lines were exercised?
2. In A1 action there seems to be no detailed information about IF ... statement: THEN ... branch is not covered, but statistics shows entire body of A1 as covered. Is it expected behavior?

Thank you!