added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
authorwenzelm
Sun Aug 29 15:09:11 2010 +0200 (2010-08-29)
changeset 38845a9e37daf5bd0
parent 38844 f3221fd64426
child 38846 e54c33dbe77c
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Markup_Tree.select: plain Iterator;
misc tuning and simplification;
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	Sat Aug 28 22:58:24 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 29 15:09:11 2010 +0200
     1.3 @@ -147,6 +147,8 @@
     1.4      def convert(range: Text.Range): Text.Range = range.map(convert(_))
     1.5      def revert(i: Text.Offset): Text.Offset
     1.6      def revert(range: Text.Range): Text.Range = range.map(revert(_))
     1.7 +    def select_markup[A](range: Text.Range)
     1.8 +      (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
     1.9    }
    1.10  
    1.11    object State
    1.12 @@ -275,6 +277,23 @@
    1.13  
    1.14          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.15          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.16 +
    1.17 +        def select_markup[A](range: Text.Range)
    1.18 +          (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
    1.19 +        {
    1.20 +          val former_range = revert(range)
    1.21 +          for {
    1.22 +            (command, command_start) <- node.command_range(former_range)
    1.23 +            Text.Info(r0, x) <- state(command).markup.
    1.24 +              select((former_range - command_start).restrict(command.range)) {
    1.25 +                case Text.Info(r0, info)
    1.26 +                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
    1.27 +                  result(Text.Info(convert(r0 + command_start), info))
    1.28 +              } { default }
    1.29 +            val r = convert(r0 + command_start)
    1.30 +            if !r.is_singularity
    1.31 +          } yield Text.Info(r, x)
    1.32 +        }
    1.33        }
    1.34      }
    1.35    }
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Aug 28 22:58:24 2010 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 29 15:09:11 2010 +0200
     2.3 @@ -90,7 +90,7 @@
     2.4      Branches.overlapping(range, branches).toStream
     2.5  
     2.6    def select[A](root_range: Text.Range)
     2.7 -    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
     2.8 +    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
     2.9    {
    2.10      def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
    2.11        : Stream[Text.Info[A]] =
    2.12 @@ -122,6 +122,7 @@
    2.13        }
    2.14      }
    2.15      stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
    2.16 +      .iterator
    2.17    }
    2.18  
    2.19    def swing_tree(parent: DefaultMutableTreeNode)
     3.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 28 22:58:24 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 29 15:09:11 2010 +0200
     3.3 @@ -266,7 +266,6 @@
     3.4          val start = buffer.getLineStartOffset(line)
     3.5          val stop = start + line_segment.count
     3.6          val range = Text.Range(start, stop)
     3.7 -        val former_range = snapshot.revert(range)
     3.8  
     3.9          /* FIXME
    3.10          for (text_area <- Isabelle.jedit_text_areas(buffer)
    3.11 @@ -290,14 +289,8 @@
    3.12          }
    3.13  
    3.14          var next_x = start
    3.15 -        for {
    3.16 -          (command, command_start) <- snapshot.node.command_range(former_range)
    3.17 -          info <- snapshot.state(command).markup.
    3.18 -            select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
    3.19 -          val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
    3.20 -          if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
    3.21 -        }
    3.22 -        {
    3.23 +        for (info <- snapshot.select_markup(range)(token_markup)(Token.NULL)) {
    3.24 +          val Text.Range(abs_start, abs_stop) = info.range
    3.25            val token_start = (abs_start - start) max 0
    3.26            val token_length =
    3.27              (abs_stop - abs_start) -
     4.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 28 22:58:24 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 29 15:09:11 2010 +0200
     4.3 @@ -189,20 +189,15 @@
     4.4  
     4.5      override def getToolTipText(x: Int, y: Int): String =
     4.6      {
     4.7 -      Swing_Thread.assert()
     4.8 -
     4.9 -      val snapshot = model.snapshot()
    4.10 -      val offset = snapshot.revert(text_area.xyToOffset(x, y))
    4.11 -      snapshot.node.command_at(offset) match {
    4.12 -        case Some((command, command_start)) =>
    4.13 -          // FIXME Isar_Document.Tooltip extractor
    4.14 -          (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
    4.15 +      Isabelle.swing_buffer_lock(model.buffer) {
    4.16 +        val snapshot = model.snapshot()
    4.17 +        val offset = text_area.xyToOffset(x, y)
    4.18 +        val markup =
    4.19 +          snapshot.select_markup(Text.Range(offset, offset + 1)) {
    4.20              case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    4.21 -              val typing =
    4.22 -                Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
    4.23 -              Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
    4.24 -          } { null }).head.info
    4.25 -        case None => null
    4.26 +              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
    4.27 +          } { null }
    4.28 +        if (markup.hasNext) markup.next.info else null
    4.29        }
    4.30      }
    4.31    }
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sat Aug 28 22:58:24 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 29 15:09:11 2010 +0200
     5.3 @@ -45,38 +45,35 @@
     5.4        Document_Model(buffer) match {
     5.5          case Some(model) =>
     5.6            val snapshot = model.snapshot()
     5.7 -          val offset = snapshot.revert(buffer_offset)
     5.8 -          snapshot.node.command_at(offset) match {
     5.9 -            case Some((command, command_start)) =>
    5.10 +          val markup =
    5.11 +            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
    5.12                // FIXME Isar_Document.Hyperlink extractor
    5.13 -              (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) {
    5.14 -                case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
    5.15 -                    List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
    5.16 -                  val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
    5.17 -                  val line = buffer.getLineOfOffset(begin)
    5.18 +              case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
    5.19 +                  List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
    5.20 +                val Text.Range(begin, end) = info_range
    5.21 +                val line = buffer.getLineOfOffset(begin)
    5.22 +                (Position.File.unapply(props), Position.Line.unapply(props)) match {
    5.23 +                  case (Some(ref_file), Some(ref_line)) =>
    5.24 +                    new External_Hyperlink(begin, end, line, ref_file, ref_line)
    5.25 +                  case _ =>
    5.26 +                    (props, props) match {
    5.27 +                      case (Position.Id(ref_id), Position.Offset(ref_offset)) =>
    5.28 +                        snapshot.lookup_command(ref_id) match {
    5.29 +                          case Some(ref_cmd) =>
    5.30 +                            snapshot.node.command_start(ref_cmd) match {
    5.31 +                              case Some(ref_cmd_start) =>
    5.32 +                                new Internal_Hyperlink(begin, end, line,
    5.33 +                                  snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset)))
    5.34 +                              case None => null
    5.35 +                            }
    5.36 +                          case None => null
    5.37 +                        }
    5.38 +                      case _ => null
    5.39 +                    }
    5.40 +                }
    5.41 +            } { null }
    5.42 +          if (markup.hasNext) markup.next.info else null
    5.43  
    5.44 -                  (Position.File.unapply(props), Position.Line.unapply(props)) match {
    5.45 -                    case (Some(ref_file), Some(ref_line)) =>
    5.46 -                      new External_Hyperlink(begin, end, line, ref_file, ref_line)
    5.47 -                    case _ =>
    5.48 -                      (Position.Id.unapply(props), Position.Offset.unapply(props)) match {
    5.49 -                        case (Some(ref_id), Some(ref_offset)) =>
    5.50 -                          snapshot.lookup_command(ref_id) match {
    5.51 -                            case Some(ref_cmd) =>
    5.52 -                              snapshot.node.command_start(ref_cmd) match {
    5.53 -                                case Some(ref_cmd_start) =>
    5.54 -                                  new Internal_Hyperlink(begin, end, line,
    5.55 -                                    snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset)))
    5.56 -                                case None => null
    5.57 -                              }
    5.58 -                            case None => null
    5.59 -                          }
    5.60 -                        case _ => null
    5.61 -                      }
    5.62 -                  }
    5.63 -              } { null }).head.info
    5.64 -            case None => null
    5.65 -          }
    5.66          case None => null
    5.67        }
    5.68      }