src/Tools/jEdit/src/isabelle_sidekick.scala
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