equal
deleted
inserted
replaced
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_range() if !stopped) { |
162 Isabelle_Sidekick.swing_markup_tree( |
162 val markup = |
163 snapshot.state.command_state(snapshot.version, command).markup, root, |
163 snapshot.state.command_state(snapshot.version, command). |
164 (info: Text.Info[List[XML.Elem]]) => |
164 markup(Command.Markup_Index.markup) |
|
165 Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) => |
165 { |
166 { |
166 val range = info.range + command_start |
167 val range = info.range + command_start |
167 val content = command.source(info.range).replace('\n', ' ') |
168 val content = command.source(info.range).replace('\n', ' ') |
168 val info_text = |
169 val info_text = |
169 Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0) |
170 Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0) |