# HG changeset patch
# User wenzelm
# Date 1392992526 -3600
# Node ID 349afd0fa0c4b942203d91cdeefb10a62fac2365
# Parent  1532ab0dc67bcd6f0e4c24c821ebd742faa80377
tuned signature;

diff -r 1532ab0dc67b -r 349afd0fa0c4 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Feb 21 15:12:50 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Feb 21 15:22:06 2014 +0100
@@ -106,12 +106,10 @@
   {
     /* markup */
 
-    def get_markup(index: Markup_Index): Markup_Tree = markups(index)
-
-    def markup: Markup_Tree = get_markup(Markup_Index.markup)
+    def markup(index: Markup_Index): Markup_Tree = markups(index)
 
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
-      markup.to_XML(command.range, command.source, filter)
+      markup(Markup_Index.markup).to_XML(command.range, command.source, filter)
 
 
     /* content */
diff -r 1532ab0dc67b -r 349afd0fa0c4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Feb 21 15:12:50 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Feb 21 15:22:06 2014 +0100
@@ -659,7 +659,7 @@
                 chunk <- thy_load_command.chunks.get(file_name).iterator
                 st = state.command_state(version, thy_load_command)
                 res = result(st)
-                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
+                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
                   former_range.restrict(chunk.range), info, elements,
                   { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
                 ).iterator
@@ -671,7 +671,7 @@
                 (command, command_start) <- node.command_range(former_range)
                 st = state.command_state(version, command)
                 res = result(st)
-                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
+                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
                   (former_range - command_start).restrict(command.range), info, elements,
                   {
                     case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
diff -r 1532ab0dc67b -r 349afd0fa0c4 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Feb 21 15:12:50 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Feb 21 15:22:06 2014 +0100
@@ -159,9 +159,10 @@
       case Some(snapshot) =>
         val root = data.root
         for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-          Isabelle_Sidekick.swing_markup_tree(
-            snapshot.state.command_state(snapshot.version, command).markup, root,
-              (info: Text.Info[List[XML.Elem]]) =>
+          val markup =
+            snapshot.state.command_state(snapshot.version, command).
+              markup(Command.Markup_Index.markup)
+          Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
               {
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')