equal
deleted
inserted
replaced
156 } |
156 } |
157 } |
157 } |
158 opt_snapshot match { |
158 opt_snapshot match { |
159 case Some(snapshot) => |
159 case Some(snapshot) => |
160 val root = data.root |
160 val root = data.root |
161 for ((command, command_start) <- snapshot.node.command_range() if !stopped) { |
161 for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) { |
162 val markup = |
162 val markup = |
163 snapshot.state.command_markup( |
163 snapshot.state.command_markup( |
164 snapshot.version, command, Command.Markup_Index.markup, |
164 snapshot.version, command, Command.Markup_Index.markup, |
165 command.range, Document.Elements.full) |
165 command.range, Document.Elements.full) |
166 Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) => |
166 Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) => |