46 if id == command.id && command.range.contains(command.decode(raw_range)) => |
46 if id == command.id && command.range.contains(command.decode(raw_range)) => |
47 val range = command.decode(raw_range) |
47 val range = command.decode(raw_range) |
48 val props = Position.purge(atts) |
48 val props = Position.purge(atts) |
49 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
49 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
50 state.add_markup(info) |
50 state.add_markup(info) |
51 case XML.Elem(Markup(name, atts), args) => |
51 case XML.Elem(Markup(name, atts), args) |
|
52 if !atts.exists({ case (a, _) => Isabelle_Markup.POSITION_PROPERTIES(a) }) => |
52 val range = command.proper_range |
53 val range = command.proper_range |
53 val props = Position.purge(atts) |
54 val props = Position.purge(atts) |
54 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
55 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
55 state.add_markup(info) |
56 state.add_markup(info) |
56 case _ => |
57 case _ => |