simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
authorwenzelm
Tue Sep 07 22:28:58 2010 +0200 (2010-09-07)
changeset 391770468964aec11
parent 39176 b8fdd3ae8815
child 39178 83e9f3ccea9f
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
tuned Snapshot.convert/revert;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Sep 07 21:06:58 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Sep 07 22:28:58 2010 +0200
     1.3 @@ -169,11 +169,11 @@
     1.4      def lookup_command(id: Command_ID): Option[Command]
     1.5      def state(command: Command): Command.State
     1.6      def convert(i: Text.Offset): Text.Offset
     1.7 -    def convert(range: Text.Range): Text.Range = range.map(convert(_))
     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 = range.map(revert(_))
    1.11 -    def select_markup[A](range: Text.Range)
    1.12 -      (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
    1.13 +    def revert(range: Text.Range): Text.Range
    1.14 +    def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    1.15 +      : Stream[Text.Info[Option[A]]]
    1.16    }
    1.17  
    1.18    object State
    1.19 @@ -304,18 +304,24 @@
    1.20          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.21          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.22  
    1.23 -        def select_markup[A](range: Text.Range)
    1.24 -          (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
    1.25 +        def convert(range: Text.Range): Text.Range =
    1.26 +          if (edits.isEmpty) range else range.map(convert(_))
    1.27 +
    1.28 +        def revert(range: Text.Range): Text.Range =
    1.29 +          if (edits.isEmpty) range else range.map(revert(_))
    1.30 +
    1.31 +        def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    1.32 +          : Stream[Text.Info[Option[A]]] =
    1.33          {
    1.34            val former_range = revert(range)
    1.35            for {
    1.36 -            (command, command_start) <- node.command_range(former_range)
    1.37 +            (command, command_start) <- node.command_range(former_range).toStream
    1.38              Text.Info(r0, x) <- state(command).markup.
    1.39                select((former_range - command_start).restrict(command.range)) {
    1.40                  case Text.Info(r0, info)
    1.41                  if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
    1.42                    result(Text.Info(convert(r0 + command_start), info))
    1.43 -              } { default }
    1.44 +              }
    1.45              val r = convert(r0 + command_start)
    1.46              if !r.is_singularity
    1.47            } yield Text.Info(r, x)
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 21:06:58 2010 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
     2.3 @@ -89,11 +89,13 @@
     2.4    private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
     2.5      Branches.overlapping(range, branches).toStream
     2.6  
     2.7 -  def select[A](root_range: Text.Range)
     2.8 -    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
     2.9 +  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    2.10 +    : Stream[Text.Info[Option[A]]] =
    2.11    {
    2.12 -    def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
    2.13 -      : Stream[Text.Info[A]] =
    2.14 +    def stream(
    2.15 +      last: Text.Offset,
    2.16 +      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
    2.17 +        : Stream[Text.Info[Option[A]]] =
    2.18      {
    2.19        stack match {
    2.20          case (parent, (range, (info, tree)) #:: more) :: rest =>
    2.21 @@ -102,7 +104,7 @@
    2.22            val start = subrange.start
    2.23  
    2.24            if (result.isDefinedAt(info)) {
    2.25 -            val next = Text.Info(subrange, result(info))
    2.26 +            val next = Text.Info[Option[A]](subrange, Some(result(info)))
    2.27              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    2.28              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    2.29              else nexts
    2.30 @@ -117,12 +119,11 @@
    2.31  
    2.32          case Nil =>
    2.33            val stop = root_range.stop
    2.34 -          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
    2.35 +          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
    2.36            else Stream.empty
    2.37        }
    2.38      }
    2.39 -    stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
    2.40 -      .iterator
    2.41 +    stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
    2.42    }
    2.43  
    2.44    def swing_tree(parent: DefaultMutableTreeNode)
     3.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 21:06:58 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 22:28:58 2010 +0200
     3.3 @@ -284,11 +284,12 @@
     3.4          }
     3.5  
     3.6          var last = start
     3.7 -        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
     3.8 +        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup).iterator) {
     3.9            val Text.Range(token_start, token_stop) = token.range
    3.10            if (last < token_start)
    3.11              handle_token(Token.COMMENT1, last - start, token_start - last)
    3.12 -          handle_token(token.info, token_start - start, token_stop - token_start)
    3.13 +          handle_token(token.info getOrElse Token.NULL,
    3.14 +            token_start - start, token_stop - token_start)
    3.15            last = token_stop
    3.16          }
    3.17          if (last < stop)
     4.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 21:06:58 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 22:28:58 2010 +0200
     4.3 @@ -222,14 +222,16 @@
     4.4  
     4.5    private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
     4.6    {
     4.7 -    val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
     4.8 +    val subexp_markup: PartialFunction[Text.Info[Any], Text.Range] =
     4.9      {
    4.10        case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
    4.11 -        Some(snapshot.convert(range))
    4.12 +        snapshot.convert(range)
    4.13      }
    4.14      val offset = text_area.xyToOffset(x, y)
    4.15 -    val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
    4.16 -    if (markup.hasNext) markup.next.info else None
    4.17 +    snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup) match {
    4.18 +      case Text.Info(_, r) #:: _ => r
    4.19 +      case _ => None
    4.20 +    }
    4.21    }
    4.22  
    4.23    private var highlight_range: Option[Text.Range] = None
    4.24 @@ -285,9 +287,8 @@
    4.25  
    4.26                // background color: markup
    4.27                for {
    4.28 -                Text.Info(range, color) <-
    4.29 -                  snapshot.select_markup(line_range)(Document_View.background_markup)(null)
    4.30 -                if color != null
    4.31 +                Text.Info(range, Some(color)) <-
    4.32 +                  snapshot.select_markup(line_range)(Document_View.background_markup).iterator
    4.33                  r <- Isabelle.gfx_range(text_area, range)
    4.34                } {
    4.35                  gfx.setColor(color)
    4.36 @@ -308,9 +309,8 @@
    4.37  
    4.38                // boxed text
    4.39                for {
    4.40 -                Text.Info(range, color) <-
    4.41 -                  snapshot.select_markup(line_range)(Document_View.box_markup)(null)
    4.42 -                if color != null
    4.43 +                Text.Info(range, Some(color)) <-
    4.44 +                  snapshot.select_markup(line_range)(Document_View.box_markup).iterator
    4.45                  r <- Isabelle.gfx_range(text_area, range)
    4.46                } {
    4.47                  gfx.setColor(color)
    4.48 @@ -319,8 +319,8 @@
    4.49  
    4.50                // squiggly underline
    4.51                for {
    4.52 -                Text.Info(range, color) <-
    4.53 -                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
    4.54 +                Text.Info(range, Some(color)) <-
    4.55 +                  snapshot.select_markup(line_range)(Document_View.message_markup).iterator
    4.56                  if color != null
    4.57                  r <- Isabelle.gfx_range(text_area, range)
    4.58                } {
    4.59 @@ -344,14 +344,10 @@
    4.60        Isabelle.swing_buffer_lock(model.buffer) {
    4.61          val snapshot = model.snapshot()
    4.62          val offset = text_area.xyToOffset(x, y)
    4.63 -        val markup =
    4.64 -          snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup)(null)
    4.65 -        if (markup.hasNext) {
    4.66 -          val text = markup.next.info
    4.67 -          if (text == null) null
    4.68 -          else Isabelle.tooltip(text)
    4.69 +        snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup) match {
    4.70 +          case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
    4.71 +          case _ => null
    4.72          }
    4.73 -        else null
    4.74        }
    4.75      }
    4.76    }
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Sep 07 21:06:58 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Sep 07 22:28:58 2010 +0200
     5.3 @@ -72,9 +72,11 @@
     5.4                        case _ => null
     5.5                      }
     5.6                  }
     5.7 -            } { null }
     5.8 -          if (markup.hasNext) markup.next.info else null
     5.9 -
    5.10 +            }
    5.11 +          markup match {
    5.12 +            case Text.Info(_, Some(link)) #:: _ => link
    5.13 +            case _ => null
    5.14 +          }
    5.15          case None => null
    5.16        }
    5.17      }