parameterized type Markup_Tree.Node;
authorwenzelm
Thu Aug 19 22:52:00 2010 +0200 (2010-08-19)
changeset 38564a6e2715fac5f
parent 38563 f6c9a4f9f66f
child 38565 32b924a832c4
parameterized type Markup_Tree.Node;
Markup_Tree.select: allow arbitrary interpretations, not just filtering;
renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 19 22:26:15 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 19 22:52:00 2010 +0200
     1.3 @@ -37,16 +37,16 @@
     1.4  
     1.5      def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
     1.6  
     1.7 -    def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
     1.8 +    def add_markup(node: Markup_Tree.Node[Any]): State = copy(markup = markup + node)
     1.9  
    1.10 -    def markup_root_node: Markup_Tree.Node =
    1.11 +    def markup_root_node: Markup_Tree.Node[Any] =
    1.12        new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
    1.13      def markup_root: Markup_Tree = markup + markup_root_node
    1.14  
    1.15  
    1.16      /* markup */
    1.17  
    1.18 -    lazy val highlight: List[Markup_Tree.Node] =
    1.19 +    lazy val highlight: List[Markup_Tree.Node[Any]] =
    1.20      {
    1.21        markup.filter(_.info match {
    1.22          case Command.HighlightInfo(_, _) => true
    1.23 @@ -54,7 +54,7 @@
    1.24        }).flatten(markup_root_node)
    1.25      }
    1.26  
    1.27 -    private lazy val types: List[Markup_Tree.Node] =
    1.28 +    private lazy val types: List[Markup_Tree.Node[Any]] =
    1.29        markup.filter(_.info match {
    1.30          case Command.TypeInfo(_) => true
    1.31          case _ => false }).flatten(markup_root_node)
    1.32 @@ -71,12 +71,12 @@
    1.33        }
    1.34      }
    1.35  
    1.36 -    private lazy val refs: List[Markup_Tree.Node] =
    1.37 +    private lazy val refs: List[Markup_Tree.Node[Any]] =
    1.38        markup.filter(_.info match {
    1.39          case Command.RefInfo(_, _, _, _) => true
    1.40          case _ => false }).flatten(markup_root_node)
    1.41  
    1.42 -    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
    1.43 +    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] =
    1.44        refs.find(_.range.contains(pos))
    1.45  
    1.46  
    1.47 @@ -159,7 +159,7 @@
    1.48  
    1.49    /* markup */
    1.50  
    1.51 -  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
    1.52 +  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node[Any] =
    1.53      new Markup_Tree.Node(symbol_index.decode(range), info)
    1.54  
    1.55  
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:26:15 2010 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 22:52:00 2010 +0200
     2.3 @@ -17,10 +17,10 @@
     2.4  
     2.5  object Markup_Tree
     2.6  {
     2.7 -  case class Node(val range: Text.Range, val info: Any)
     2.8 +  case class Node[A](val range: Text.Range, val info: A)
     2.9    {
    2.10 -    def contains(that: Node): Boolean = this.range contains that.range
    2.11 -    def restrict(r: Text.Range): Node = Node(range.intersect(r), info)
    2.12 +    def contains[B](that: Node[B]): Boolean = this.range contains that.range
    2.13 +    def restrict(r: Text.Range): Node[A] = Node(range.restrict(r), info)
    2.14    }
    2.15  
    2.16  
    2.17 @@ -28,12 +28,12 @@
    2.18  
    2.19    object Branches
    2.20    {
    2.21 -    type Entry = (Node, Markup_Tree)
    2.22 -    type T = SortedMap[Node, Entry]
    2.23 +    type Entry = (Node[Any], Markup_Tree)
    2.24 +    type T = SortedMap[Node[Any], Entry]
    2.25  
    2.26 -    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
    2.27 +    val empty = SortedMap.empty[Node[Any], Entry](new scala.math.Ordering[Node[Any]]
    2.28        {
    2.29 -        def compare(x: Node, y: Node): Int = x.range compare y.range
    2.30 +        def compare(x: Node[Any], y: Node[Any]): Int = x.range compare y.range
    2.31        })
    2.32  
    2.33      def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
    2.34 @@ -56,7 +56,7 @@
    2.35        case list => list.mkString("Tree(", ",", ")")
    2.36      }
    2.37  
    2.38 -  def + (new_node: Node): Markup_Tree =
    2.39 +  def + (new_node: Node[Any]): Markup_Tree =
    2.40    {
    2.41      branches.get(new_node) match {
    2.42        case None =>
    2.43 @@ -82,9 +82,9 @@
    2.44  
    2.45    // FIXME depth-first with result markup stack
    2.46    // FIXME projection to given range
    2.47 -  def flatten(parent: Node): List[Node] =
    2.48 +  def flatten(parent: Node[Any]): List[Node[Any]] =
    2.49    {
    2.50 -    val result = new mutable.ListBuffer[Node]
    2.51 +    val result = new mutable.ListBuffer[Node[Any]]
    2.52      var offset = parent.range.start
    2.53      for ((_, (node, subtree)) <- branches.iterator) {
    2.54        if (offset < node.range.start)
    2.55 @@ -97,7 +97,7 @@
    2.56      result.toList
    2.57    }
    2.58  
    2.59 -  def filter(pred: Node => Boolean): Markup_Tree =
    2.60 +  def filter(pred: Node[Any] => Boolean): Markup_Tree =
    2.61    {
    2.62      val bs = branches.toList.flatMap(entry => {
    2.63        val (_, (node, subtree)) = entry
    2.64 @@ -107,24 +107,26 @@
    2.65      new Markup_Tree(Branches.empty ++ bs)
    2.66    }
    2.67  
    2.68 -  def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
    2.69 +  def select[A](range: Text.Range)(sel: PartialFunction[Any, A]): Stream[Node[List[A]]] =
    2.70    {
    2.71 -    def stream(parent: Node, bs: Branches.T): Stream[Node] =
    2.72 +    def stream(parent: Node[List[A]], bs: Branches.T): Stream[Node[List[A]]] =
    2.73      {
    2.74        val substream =
    2.75          (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
    2.76 -          if (sel.isDefinedAt(node))
    2.77 -            stream(node.restrict(parent.range), subtree.branches)
    2.78 +          if (sel.isDefinedAt(node.info)) {
    2.79 +            val current = Node(node.range.restrict(parent.range), List(sel(node.info)))
    2.80 +            stream(current, subtree.branches)
    2.81 +          }
    2.82            else stream(parent, subtree.branches)
    2.83          }).flatten
    2.84  
    2.85 -      def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
    2.86 +      def padding(last: Text.Offset, s: Stream[Node[List[A]]]): Stream[Node[List[A]]] =
    2.87          s match {
    2.88            case (node @ Node(Text.Range(start, stop), _)) #:: rest =>
    2.89              if (last < start)
    2.90                parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest)
    2.91              else node #:: padding(stop, rest)
    2.92 -          case Stream.Empty =>  // FIXME
    2.93 +          case Stream.Empty =>
    2.94              if (last < parent.range.stop)
    2.95                Stream(parent.restrict(Text.Range(last, parent.range.stop)))
    2.96              else Stream.Empty
    2.97 @@ -134,7 +136,7 @@
    2.98      stream(Node(range, Nil), branches)
    2.99    }
   2.100  
   2.101 -  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
   2.102 +  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode)
   2.103    {
   2.104      for ((_, (node, subtree)) <- branches) {
   2.105        val current = swing_node(node)
     3.1 --- a/src/Pure/PIDE/text.scala	Thu Aug 19 22:26:15 2010 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Thu Aug 19 22:52:00 2010 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4      def start_range: Range = Range(start, start)
     3.5      def stop_range: Range = Range(stop, stop)
     3.6  
     3.7 -    def intersect(that: Range): Range =
     3.8 +    def restrict(that: Range): Range =
     3.9        Range(this.start max that.start, this.stop min that.stop)
    3.10    }
    3.11  
     4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 19 22:26:15 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 19 22:52:00 2010 +0200
     4.3 @@ -129,7 +129,7 @@
     4.4      val root = data.root
     4.5      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     4.6      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
     4.7 -      snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) =>
     4.8 +      snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node[Any]) =>
     4.9            {
    4.10              val content = command.source(node.range).replace('\n', ' ')
    4.11              val id = command.id