equal
deleted
inserted
replaced
160 val root = data.root |
160 val root = data.root |
161 for ((command, command_start) <- snapshot.node.command_iterator() 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, Markup.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]]) => |
167 { |
167 { |
168 val range = info.range + command_start |
168 val range = info.range + command_start |
169 val content = command.source(info.range).replace('\n', ' ') |
169 val content = command.source(info.range).replace('\n', ' ') |
170 val info_text = |
170 val info_text = |