--- a/src/Tools/jEdit/src/graphview_dockable.scala Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun Nov 25 19:49:24 2012 +0100
@@ -81,9 +81,9 @@
val new_graph =
if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
new_state.markup.cumulate[Option[XML.Body]](
- new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
+ new_state.command.range, None, Some(Set(Markup.GRAPHVIEW)),
{
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.GRAPHVIEW, _), graph))) =>
Some(graph)
}).filter(_.info.isDefined) match {
case Text.Info(_, Some(graph)) #:: _ => graph