more robust treatment of partial range restriction;
authorwenzelm
Sat Jun 18 00:05:29 2011 +0200 (2011-06-18)
changeset 43428b41dea5772c6
parent 43427 5c716a68931a
child 43429 095f90f8dca3
more robust treatment of partial range restriction;
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Pure/PIDE/text.scala	Sat Jun 18 00:03:58 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sat Jun 18 00:05:29 2011 +0200
     1.3 @@ -43,6 +43,10 @@
     1.4  
     1.5      def restrict(that: Range): Range =
     1.6        Range(this.start max that.start, this.stop min that.stop)
     1.7 +
     1.8 +    def try_restrict(that: Range): Option[Range] =
     1.9 +      try { Some (restrict(that)) }
    1.10 +      catch { case _: RuntimeException => None }
    1.11    }
    1.12  
    1.13  
    1.14 @@ -51,6 +55,9 @@
    1.15    case class Info[A](val range: Text.Range, val info: A)
    1.16    {
    1.17      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    1.18 +    def try_restrict(r: Text.Range): Option[Info[A]] =
    1.19 +      try { Some(Info(range.restrict(r), info)) }
    1.20 +      catch { case _: RuntimeException => None }
    1.21    }
    1.22  
    1.23  
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 00:03:58 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 00:05:29 2011 +0200
     2.3 @@ -90,10 +90,10 @@
     2.4              val line_range = doc_view.proper_line_range(start(i), end(i))
     2.5  
     2.6              // background color: status
     2.7 -            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
     2.8              for {
     2.9 -              (command, command_start) <- cmds if !command.is_ignored
    2.10 -              val range = line_range.restrict(snapshot.convert(command.range + command_start))
    2.11 +              (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range))
    2.12 +              if !command.is_ignored
    2.13 +              range <- line_range.try_restrict(snapshot.convert(command.range + command_start))
    2.14                r <- Isabelle.gfx_range(text_area, range)
    2.15                color <- Isabelle_Markup.status_color(snapshot, command)
    2.16              } {
    2.17 @@ -220,8 +220,10 @@
    2.18          val chunk_color = chunk.style.getForegroundColor
    2.19  
    2.20          val markup =
    2.21 -          painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
    2.22 -            .map(_.restrict(chunk_range))
    2.23 +          for {
    2.24 +            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
    2.25 +            y <- x.try_restrict(chunk_range)
    2.26 +          } yield y
    2.27  
    2.28          gfx.setFont(chunk_font)
    2.29          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
    2.30 @@ -233,11 +235,10 @@
    2.31          else if (!markup.isEmpty) {
    2.32            var x1 = x + w
    2.33            for {
    2.34 -            Text.Info(r, info) <-
    2.35 +            Text.Info(range, info) <-
    2.36                Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
    2.37                markup.iterator ++
    2.38                Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
    2.39 -            val range = r.restrict(chunk_range)
    2.40              if !range.is_singularity
    2.41            } {
    2.42              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)