equal
deleted
inserted
replaced
79 } |
79 } |
80 |
80 |
81 val new_graph = |
81 val new_graph = |
82 if (!restriction.isDefined || restriction.get.contains(new_state.command)) { |
82 if (!restriction.isDefined || restriction.get.contains(new_state.command)) { |
83 new_state.markup.cumulate[Option[XML.Body]]( |
83 new_state.markup.cumulate[Option[XML.Body]]( |
84 new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)), |
84 new_state.command.range, None, Some(Set(Markup.GRAPHVIEW)), |
85 { |
85 { |
86 case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) => |
86 case (_, Text.Info(_, XML.Elem(Markup(Markup.GRAPHVIEW, _), graph))) => |
87 Some(graph) |
87 Some(graph) |
88 }).filter(_.info.isDefined) match { |
88 }).filter(_.info.isDefined) match { |
89 case Text.Info(_, Some(graph)) #:: _ => graph |
89 case Text.Info(_, Some(graph)) #:: _ => graph |
90 case _ => Nil |
90 case _ => Nil |
91 } |
91 } |