equal
deleted
inserted
replaced
189 NONTERMINAL of string * Position.range | |
189 NONTERMINAL of string * Position.range | |
190 TERMINAL of (bool * string) * Position.range | |
190 TERMINAL of (bool * string) * Position.range | |
191 ANTIQUOTE of (bool * Antiquote.antiq) * Position.range; |
191 ANTIQUOTE of (bool * Antiquote.antiq) * Position.range; |
192 |
192 |
193 fun reports_of_tree ctxt = |
193 fun reports_of_tree ctxt = |
194 if Context_Position.is_visible ctxt then |
194 if Context_Position.reports_enabled ctxt then |
195 let |
195 let |
196 fun reports r = |
196 fun reports r = |
197 if r = Position.no_range then [] |
197 if r = Position.no_range then [] |
198 else [(Position.range_position r, Markup.expression "")]; |
198 else [(Position.range_position r, Markup.expression "")]; |
199 fun trees (CAT (ts, r)) = reports r @ maps tree ts |
199 fun trees (CAT (ts, r)) = reports r @ maps tree ts |