more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
authorwenzelm
Wed Aug 07 13:46:32 2013 +0200 (2013-08-07)
changeset 52889ea3338812e67
parent 52888 671421cef590
child 52890 36e2c0c308eb
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 07 11:50:14 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 07 13:46:32 2013 +0200
     1.3 @@ -320,19 +320,19 @@
     1.4      val node: Node
     1.5      val is_outdated: Boolean
     1.6      def convert(i: Text.Offset): Text.Offset
     1.7 +    def revert(i: Text.Offset): Text.Offset
     1.8      def convert(range: Text.Range): Text.Range
     1.9 -    def revert(i: Text.Offset): Text.Offset
    1.10      def revert(range: Text.Range): Text.Range
    1.11      def eq_content(other: Snapshot): Boolean
    1.12      def cumulate_markup[A](
    1.13        range: Text.Range,
    1.14        info: A,
    1.15        elements: Option[Set[String]],
    1.16 -      result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
    1.17 +      result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]]
    1.18      def select_markup[A](
    1.19        range: Text.Range,
    1.20        elements: Option[Set[String]],
    1.21 -      result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
    1.22 +      result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]]
    1.23    }
    1.24  
    1.25    type Assign_Update =
    1.26 @@ -564,33 +564,30 @@
    1.27              })
    1.28  
    1.29          def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.30 -          result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.31 +          result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
    1.32          {
    1.33            val former_range = revert(range)
    1.34            for {
    1.35              (command, command_start) <- node.command_range(former_range).toStream
    1.36              st = state.command_state(version, command)
    1.37              res = result(st)
    1.38 -            Text.Info(r0, a) <- st.markup.
    1.39 -              cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
    1.40 -                {
    1.41 -                  case (a, Text.Info(r0, b))
    1.42 -                  if res.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.43 -                    res((a, Text.Info(convert(r0 + command_start), b)))
    1.44 -                })
    1.45 +            Text.Info(r0, a) <- st.markup.cumulate[A](
    1.46 +              (former_range - command_start).restrict(command.range), info, elements,
    1.47 +              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) })
    1.48            } yield Text.Info(convert(r0 + command_start), a)
    1.49          }
    1.50  
    1.51          def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.52 -          result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
    1.53 +          result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]] =
    1.54          {
    1.55 -          def result1(st: Command.State) =
    1.56 +          def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
    1.57            {
    1.58              val res = result(st)
    1.59 -            new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.60 -              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = res.isDefinedAt(arg._2)
    1.61 -              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(res(arg._2))
    1.62 -            }
    1.63 +            (_: Option[A], x: Text.Markup) =>
    1.64 +              res(x) match {
    1.65 +                case None => None
    1.66 +                case some => Some(some)
    1.67 +              }
    1.68            }
    1.69            for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
    1.70              yield Text.Info(r, x)
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 11:50:14 2013 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 13:46:32 2013 +0200
     2.3 @@ -223,7 +223,7 @@
     2.4      to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
     2.5  
     2.6    def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
     2.7 -    result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
     2.8 +    result: (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
     2.9    {
    2.10      val notable: Elements => Boolean =
    2.11        result_elements match {
    2.12 @@ -233,15 +233,12 @@
    2.13  
    2.14      def results(x: A, entry: Entry): Option[A] =
    2.15      {
    2.16 -      val (y, changed) =
    2.17 -        // FIXME proper cumulation order (including status markup) (!?)
    2.18 -        ((x, false) /: entry.rev_markup)((res, info) =>
    2.19 -          {
    2.20 -            val (y, changed) = res
    2.21 -            val arg = (y, Text.Info(entry.range, info))
    2.22 -            if (result.isDefinedAt(arg)) (result(arg), true)
    2.23 -            else res
    2.24 -          })
    2.25 +      var y = x
    2.26 +      var changed = false
    2.27 +      for {
    2.28 +        info <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
    2.29 +        y1 <- result(y, Text.Info(entry.range, info))
    2.30 +      } { y = y1; changed = true }
    2.31        if (changed) Some(y) else None
    2.32      }
    2.33  
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 11:50:14 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 13:46:32 2013 +0200
     3.3 @@ -154,11 +154,12 @@
     3.4          snapshot.cumulate_markup[(Protocol.Status, Int)](
     3.5            range, (Protocol.Status.init, 0), Some(overview_include), _ =>
     3.6            {
     3.7 -            case ((status, pri), Text.Info(_, XML.Elem(markup, _)))
     3.8 -            if overview_include(markup.name) =>
     3.9 +            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
    3.10                if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
    3.11 -                (status, pri max Rendering.message_pri(markup.name))
    3.12 -              else (Protocol.command_status(status, markup), pri)
    3.13 +                Some((status, pri max Rendering.message_pri(markup.name)))
    3.14 +              else if (overview_include(markup.name))
    3.15 +                Some((Protocol.command_status(status, markup), pri))
    3.16 +              else None
    3.17            })
    3.18        if (results.isEmpty) None
    3.19        else {
    3.20 @@ -188,8 +189,10 @@
    3.21    {
    3.22      snapshot.select_markup(range, Some(highlight_include), _ =>
    3.23          {
    3.24 -          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
    3.25 -            Text.Info(snapshot.convert(info_range), highlight_color)
    3.26 +          case Text.Info(info_range, XML.Elem(markup, _)) =>
    3.27 +            if (highlight_include(markup.name))
    3.28 +              Some(Text.Info(snapshot.convert(info_range), highlight_color))
    3.29 +            else None
    3.30          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    3.31    }
    3.32  
    3.33 @@ -203,7 +206,8 @@
    3.34            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    3.35            if Path.is_ok(name) =>
    3.36              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    3.37 -            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
    3.38 +            val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
    3.39 +            Some(link :: links)
    3.40  
    3.41            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    3.42            if !props.exists(
    3.43 @@ -216,8 +220,10 @@
    3.44                  Isabelle_System.source_file(Path.explode(name)) match {
    3.45                    case Some(path) =>
    3.46                      val jedit_file = Isabelle_System.platform_path(path)
    3.47 -                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
    3.48 -                  case None => links
    3.49 +                    val link =
    3.50 +                      Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
    3.51 +                    Some(link :: links)
    3.52 +                  case None => None
    3.53                  }
    3.54  
    3.55                case Position.Def_Id_Offset(id, offset) =>
    3.56 @@ -227,13 +233,17 @@
    3.57                        node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    3.58                          Iterator.single(command.source(Text.Range(0, command.decode(offset))))
    3.59                      val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    3.60 -                    Text.Info(snapshot.convert(info_range),
    3.61 -                      Hyperlink(command.node_name.node, line, column)) :: links
    3.62 -                  case None => links
    3.63 +                    val link =
    3.64 +                      Text.Info(snapshot.convert(info_range),
    3.65 +                        Hyperlink(command.node_name.node, line, column))
    3.66 +                    Some(link :: links)
    3.67 +                  case None => None
    3.68                  }
    3.69  
    3.70 -              case _ => links
    3.71 +              case _ => None
    3.72              }
    3.73 +
    3.74 +          case _ => None
    3.75          }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
    3.76    }
    3.77  
    3.78 @@ -246,10 +256,11 @@
    3.79          {
    3.80            case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    3.81            if !command_state.results.defined(serial) =>
    3.82 -            Text.Info(snapshot.convert(info_range), elem)
    3.83 -          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
    3.84 -          if name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
    3.85 -            Text.Info(snapshot.convert(info_range), elem)
    3.86 +            Some(Text.Info(snapshot.convert(info_range), elem))
    3.87 +          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) =>
    3.88 +            if (name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK)
    3.89 +              Some(Text.Info(snapshot.convert(info_range), elem))
    3.90 +            else None
    3.91          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    3.92  
    3.93  
    3.94 @@ -257,7 +268,7 @@
    3.95    {
    3.96      val results =
    3.97        snapshot.select_markup[Command.Results](range, None, command_state =>
    3.98 -        { case _ => command_state.results }).map(_.info)
    3.99 +        { case _ => Some(command_state.results) }).map(_.info)
   3.100      (Command.Results.empty /: results)(_ ++ _)
   3.101    }
   3.102  
   3.103 @@ -272,12 +283,14 @@
   3.104            if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
   3.105              val entry: Command.Results.Entry =
   3.106                (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   3.107 -            Text.Info(snapshot.convert(info_range), entry) :: msgs
   3.108 +            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   3.109  
   3.110            case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   3.111            if !body.isEmpty =>
   3.112              val entry: Command.Results.Entry = (Document_ID.make(), msg)
   3.113 -            Text.Info(snapshot.convert(info_range), entry) :: msgs
   3.114 +            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   3.115 +
   3.116 +          case _ => None
   3.117          }).toList.flatMap(_.info)
   3.118      if (results.isEmpty) None
   3.119      else {
   3.120 @@ -328,7 +341,7 @@
   3.121          range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
   3.122          {
   3.123            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   3.124 -            Text.Info(r, (t1 + t2, info))
   3.125 +            Some(Text.Info(r, (t1 + t2, info)))
   3.126            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   3.127              val kind1 = space_explode('_', kind).mkString(" ")
   3.128              val txt1 = kind1 + " " + quote(name)
   3.129 @@ -337,19 +350,20 @@
   3.130                if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   3.131                  "\n" + t.message
   3.132                else ""
   3.133 -            add(prev, r, (true, XML.Text(txt1 + txt2)))
   3.134 +            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   3.135            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   3.136            if Path.is_ok(name) =>
   3.137              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   3.138 -            add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
   3.139 +            Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
   3.140            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   3.141            if name == Markup.SORTING || name == Markup.TYPING =>
   3.142 -            add(prev, r, (true, pretty_typing("::", body)))
   3.143 +            Some(add(prev, r, (true, pretty_typing("::", body))))
   3.144            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   3.145 -            add(prev, r, (false, pretty_typing("ML:", body)))
   3.146 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   3.147 -          if tooltips.isDefinedAt(name) =>
   3.148 -            add(prev, r, (true, XML.Text(tooltips(name))))
   3.149 +            Some(add(prev, r, (false, pretty_typing("ML:", body))))
   3.150 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   3.151 +            if (tooltips.isDefinedAt(name))
   3.152 +              Some(add(prev, r, (true, XML.Text(tooltips(name)))))
   3.153 +            else None
   3.154          }).toList.map(_.info)
   3.155  
   3.156      results.map(_.info).flatMap(_._2) match {
   3.157 @@ -383,15 +397,17 @@
   3.158          {
   3.159            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
   3.160                List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
   3.161 -            pri max Rendering.information_pri
   3.162 +            Some(pri max Rendering.information_pri)
   3.163            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
   3.164              body match {
   3.165                case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
   3.166 -                pri max Rendering.legacy_pri
   3.167 -              case _ => pri max Rendering.warning_pri
   3.168 +                Some(pri max Rendering.legacy_pri)
   3.169 +              case _ =>
   3.170 +                Some(pri max Rendering.warning_pri)
   3.171              }
   3.172            case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
   3.173 -            pri max Rendering.error_pri
   3.174 +            Some(pri max Rendering.error_pri)
   3.175 +          case _ => None
   3.176          })
   3.177      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   3.178      gutter_icons.get(pri)
   3.179 @@ -404,19 +420,19 @@
   3.180      Rendering.warning_pri -> warning_color,
   3.181      Rendering.error_pri -> error_color)
   3.182  
   3.183 -  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   3.184 +  private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   3.185  
   3.186    def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   3.187    {
   3.188      val results =
   3.189 -      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
   3.190 +      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
   3.191          {
   3.192 -          case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _)))
   3.193 -          if name == Markup.WRITELN ||
   3.194 -            name == Markup.WARNING ||
   3.195 -            name == Markup.ERROR =>
   3.196 -              if (Protocol.is_information(msg)) pri max Rendering.information_pri
   3.197 -              else pri max Rendering.message_pri(name)
   3.198 +          case (pri, Text.Info(_, msg @ XML.Elem(markup, _))) =>
   3.199 +            if (Protocol.is_information(msg))
   3.200 +              Some(pri max Rendering.information_pri)
   3.201 +            else if (squiggly_include.contains(markup.name))
   3.202 +              Some(pri max Rendering.message_pri(markup.name))
   3.203 +            else None
   3.204          })
   3.205      for {
   3.206        Text.Info(r, pri) <- results
   3.207 @@ -442,19 +458,20 @@
   3.208        snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
   3.209          {
   3.210            case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
   3.211 -            pri max Rendering.information_pri
   3.212 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   3.213 -          if name == Markup.WRITELN_MESSAGE ||
   3.214 -            name == Markup.TRACING_MESSAGE ||
   3.215 -            name == Markup.WARNING_MESSAGE ||
   3.216 -            name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
   3.217 +            Some(pri max Rendering.information_pri)
   3.218 +          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
   3.219 +            if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
   3.220 +                name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
   3.221 +              Some(pri max Rendering.message_pri(name))
   3.222 +            else None
   3.223          })
   3.224      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   3.225  
   3.226      val is_separator = pri > 0 &&
   3.227        snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
   3.228          {
   3.229 -          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
   3.230 +          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => Some(true)
   3.231 +          case _ => None
   3.232          }).exists(_.info)
   3.233  
   3.234      message_colors.get(pri).map((_, is_separator))
   3.235 @@ -483,20 +500,21 @@
   3.236              {
   3.237                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   3.238                if (Protocol.command_status_markup(markup.name)) =>
   3.239 -                (Some(Protocol.command_status(status, markup)), color)
   3.240 +                Some((Some(Protocol.command_status(status, markup)), color))
   3.241                case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   3.242 -                (None, Some(bad_color))
   3.243 +                Some((None, Some(bad_color)))
   3.244                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   3.245 -                (None, Some(intensify_color))
   3.246 +                Some((None, Some(intensify_color)))
   3.247                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   3.248                  command_state.results.get(serial) match {
   3.249                    case Some(Protocol.Dialog_Result(res)) if res == result =>
   3.250 -                    (None, Some(active_result_color))
   3.251 +                    Some((None, Some(active_result_color)))
   3.252                    case _ =>
   3.253 -                    (None, Some(active_color))
   3.254 +                    Some((None, Some(active_color)))
   3.255                  }
   3.256 -              case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
   3.257 -                (None, Some(active_color))
   3.258 +              case (_, Text.Info(_, XML.Elem(markup, _))) =>
   3.259 +                if (active_include(markup.name)) Some((None, Some(active_color)))
   3.260 +                else None
   3.261              })
   3.262          color <-
   3.263            (result match {
   3.264 @@ -513,14 +531,16 @@
   3.265    def background2(range: Text.Range): Stream[Text.Info[Color]] =
   3.266      snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
   3.267        {
   3.268 -        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   3.269 +        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => Some(light_color)
   3.270 +        case _ => None
   3.271        })
   3.272  
   3.273  
   3.274    def bullet(range: Text.Range): Stream[Text.Info[Color]] =
   3.275      snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
   3.276        {
   3.277 -        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
   3.278 +        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => Some(bullet_color)
   3.279 +        case _ => None
   3.280        })
   3.281  
   3.282  
   3.283 @@ -530,10 +550,11 @@
   3.284    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   3.285      snapshot.select_markup(range, Some(foreground_elements), _ =>
   3.286        {
   3.287 -        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
   3.288 -        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
   3.289 -        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   3.290 -        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => antiquoted_color
   3.291 +        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => Some(quoted_color)
   3.292 +        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => Some(quoted_color)
   3.293 +        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => Some(quoted_color)
   3.294 +        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => Some(antiquoted_color)
   3.295 +        case _ => None
   3.296        })
   3.297  
   3.298  
   3.299 @@ -570,8 +591,7 @@
   3.300      else
   3.301        snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
   3.302          {
   3.303 -          case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   3.304 -          if text_colors.isDefinedAt(m) => text_colors(m)
   3.305 +          case (_, Text.Info(_, XML.Elem(markup, _))) => text_colors.get(markup.name)
   3.306          })
   3.307    }
   3.308  
   3.309 @@ -583,7 +603,7 @@
   3.310    def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
   3.311      snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
   3.312        {
   3.313 -        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
   3.314 -        if fold_depth_include(name) => depth + 1
   3.315 +        case (depth, Text.Info(_, XML.Elem(markup, _))) =>
   3.316 +          if (fold_depth_include(markup.name)) Some(depth + 1) else None
   3.317        })
   3.318  }