tuned signature;
authorwenzelm
Sat Nov 12 11:45:49 2011 +0100 (2011-11-12 ago)
changeset 454673f290b6288cf
parent 45466 98af01f897c9
child 45468 33e946d3f449
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_markup.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Nov 11 22:09:07 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Nov 12 11:45:49 2011 +0100
     1.3 @@ -240,8 +240,7 @@
     1.4      def convert(range: Text.Range): Text.Range
     1.5      def revert(i: Text.Offset): Text.Offset
     1.6      def revert(range: Text.Range): Text.Range
     1.7 -    def cumulate_markup[A](info: Text.Info[A])(result: Markup_Tree.Cumulate[A])
     1.8 -      : Stream[Text.Info[A]]
     1.9 +    def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
    1.10      def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.11        : Stream[Text.Info[Option[A]]]
    1.12    }
    1.13 @@ -473,18 +472,23 @@
    1.14          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.15          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.16  
    1.17 -        def cumulate_markup[A](root: Text.Info[A])(result: Markup_Tree.Cumulate[A])
    1.18 +        def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
    1.19            : Stream[Text.Info[A]] =
    1.20          {
    1.21 -          val former_range = revert(root.range)
    1.22 +          val info = body.info
    1.23 +          val result = body.result
    1.24 +
    1.25 +          val former_range = revert(range)
    1.26            for {
    1.27              (command, command_start) <- node.command_range(former_range).toStream
    1.28              Text.Info(r0, a) <- command_state(command).markup.
    1.29 -              cumulate(Text.Info((former_range - command_start).restrict(command.range), root.info)) {
    1.30 -                case (a, Text.Info(r0, b))
    1.31 -                if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.32 -                  result((a, Text.Info(convert(r0 + command_start), b)))
    1.33 -              }
    1.34 +              cumulate((former_range - command_start).restrict(command.range))(
    1.35 +                Markup_Tree.Cumulate[A](info,
    1.36 +                  {
    1.37 +                    case (a, Text.Info(r0, b))
    1.38 +                    if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.39 +                      result((a, Text.Info(convert(r0 + command_start), b)))
    1.40 +                  }))
    1.41            } yield Text.Info(convert(r0 + command_start), a)
    1.42          }
    1.43  
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 22:09:07 2011 +0100
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 11:45:49 2011 +0100
     2.3 @@ -15,7 +15,7 @@
     2.4  
     2.5  object Markup_Tree
     2.6  {
     2.7 -  type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
     2.8 +  sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A])
     2.9    type Select[A] = PartialFunction[Text.Markup, A]
    2.10  
    2.11    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    2.12 @@ -84,15 +84,18 @@
    2.13      }
    2.14    }
    2.15  
    2.16 -  def cumulate[A](root: Text.Info[A])(result: Cumulate[A]): Stream[Text.Info[A]] =
    2.17 +  def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] =
    2.18    {
    2.19 +    val root_info = body.info
    2.20 +    val result = body.result
    2.21 +
    2.22      def stream(
    2.23        last: Text.Offset,
    2.24        stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]): Stream[Text.Info[A]] =
    2.25      {
    2.26        stack match {
    2.27          case (parent, (range, (info, tree)) #:: more) :: rest =>
    2.28 -          val subrange = range.restrict(root.range)
    2.29 +          val subrange = range.restrict(root_range)
    2.30            val subtree = tree.overlapping(subrange).toStream
    2.31            val start = subrange.start
    2.32  
    2.33 @@ -112,12 +115,13 @@
    2.34            else nexts
    2.35  
    2.36          case Nil =>
    2.37 -          val stop = root.range.stop
    2.38 -          if (last < stop) Stream(root.restrict(Text.Range(last, stop)))
    2.39 +          val stop = root_range.stop
    2.40 +          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
    2.41            else Stream.empty
    2.42        }
    2.43      }
    2.44 -    stream(root.range.start, List((root, overlapping(root.range).toStream)))
    2.45 +    stream(root_range.start,
    2.46 +      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
    2.47    }
    2.48  
    2.49    def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Nov 11 22:09:07 2011 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Nov 12 11:45:49 2011 +0100
     3.3 @@ -293,8 +293,7 @@
     3.4            else Isabelle.tooltip(tooltips.mkString("\n"))
     3.5          }
     3.6          else {
     3.7 -          snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
     3.8 -            Isabelle_Markup.tooltip_message) match
     3.9 +          snapshot.cumulate_markup(range)(Isabelle_Markup.tooltip_message) match
    3.10            {
    3.11              case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
    3.12                Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Fri Nov 11 22:09:07 2011 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 11:45:49 2011 +0100
     4.3 @@ -94,13 +94,14 @@
     4.4      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
     4.5    }
     4.6  
     4.7 -  val tooltip_message: Markup_Tree.Cumulate[SortedMap[Long, String]] =
     4.8 -  {
     4.9 -    case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
    4.10 -    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
    4.11 -      msgs + (serial ->
    4.12 -        Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    4.13 -  }
    4.14 +  val tooltip_message =
    4.15 +    Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
    4.16 +      {
    4.17 +        case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
    4.18 +        if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
    4.19 +          msgs + (serial ->
    4.20 +            Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    4.21 +      })
    4.22  
    4.23    val gutter_message: Markup_Tree.Select[Icon] =
    4.24    {