changeset 56743 | 81370dfadb1d |
parent 56609 | 5ac67041ccf8 |
child 56814 | eb8f2a5a57ad |
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Apr 26 06:43:06 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Apr 26 13:07:20 2014 +0200 @@ -162,7 +162,7 @@ val markup = snapshot.state.command_markup( snapshot.version, command, Command.Markup_Index.markup, - command.range, Document.Elements.full) + command.range, Markup.Elements.full) Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) => { val range = info.range + command_start