| changeset 62806 | de9bf8171626 |
| parent 62797 | e08c44eed27f |
| child 67147 | dea94b1aabc3 |
--- a/src/Pure/Tools/rail.ML Fri Apr 01 19:01:34 2016 +0200 +++ b/src/Pure/Tools/rail.ML Fri Apr 01 21:34:17 2016 +0200 @@ -188,7 +188,7 @@ let fun reports r = if r = Position.no_range then [] - else [(Position.range_position r, Markup.expression)]; + else [(Position.range_position r, Markup.expression "")]; fun trees (CAT (ts, r)) = reports r @ maps tree ts and tree (BAR (Ts, r)) = reports r @ maps trees Ts | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2