more robust treatment of partial range restriction;

--- a/src/Pure/PIDE/text.scala	Sat Jun 18 00:03:58 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Sat Jun 18 00:05:29 2011 +0200
@@ -43,6 +43,10 @@
 
     def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
+
+    def try_restrict(that: Range): Option[Range] =
+      try { Some (restrict(that)) }
+      catch { case _: RuntimeException => None }
   }
 
 
@@ -51,6 +55,9 @@
   case class Info[A](val range: Text.Range, val info: A)
   {
     def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
+    def try_restrict(r: Text.Range): Option[Info[A]] =
+      try { Some(Info(range.restrict(r), info)) }
+      catch { case _: RuntimeException => None }
   }
 
 

--- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 00:03:58 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 00:05:29 2011 +0200
@@ -90,10 +90,10 @@
             val line_range = doc_view.proper_line_range(start(i), end(i))
 
             // background color: status
-            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
             for {
-              (command, command_start) <- cmds if !command.is_ignored
-              val range = line_range.restrict(snapshot.convert(command.range + command_start))
+              (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range))
+              if !command.is_ignored
+              range <- line_range.try_restrict(snapshot.convert(command.range + command_start))
               r <- Isabelle.gfx_range(text_area, range)
               color <- Isabelle_Markup.status_color(snapshot, command)
             } {
@@ -220,8 +220,10 @@
         val chunk_color = chunk.style.getForegroundColor
 
         val markup =
-          painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
-            .map(_.restrict(chunk_range))
+          for {
+            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
+            y <- x.try_restrict(chunk_range)
+          } yield y
 
         gfx.setFont(chunk_font)
         if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
@@ -233,11 +235,10 @@
         else if (!markup.isEmpty) {
           var x1 = x + w
           for {
-            Text.Info(r, info) <-
+            Text.Info(range, info) <-
               Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
               markup.iterator ++
               Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
-            val range = r.restrict(chunk_range)
             if !range.is_singularity
           } {
             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)