more efficient Markup_Tree, based on branches sorted by quasi-order;
authorwenzelm
Wed Aug 18 23:44:50 2010 +0200 (2010-08-18)
changeset 38479e628da370072
parent 38478 7766812a01e7
child 38480 e5eed57913d0
more efficient Markup_Tree, based on branches sorted by quasi-order;
renamed markup_node.scala to markup_tree.scala and classes/objects accordingly;
Position.Range: produce actual Text.Range;
Symbol.Index.decode: convert 1-based Isabelle offsets here;
added static Command.range;
simplified Command.markup;
Document_Model.token_marker: flatten markup at most once;
tuned;
src/Pure/General/position.scala
src/Pure/General/symbol.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_node.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/build-jars
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/General/position.scala	Wed Aug 18 14:04:13 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Wed Aug 18 23:44:50 2010 +0200
     1.3 @@ -20,13 +20,13 @@
     1.4    def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
     1.5    def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
     1.6  
     1.7 -  def get_range(pos: T): Option[(Int, Int)] =
     1.8 +  def get_range(pos: T): Option[Text.Range] =
     1.9      (get_offset(pos), get_end_offset(pos)) match {
    1.10 -      case (Some(begin), Some(end)) => Some(begin, end)
    1.11 -      case (Some(begin), None) => Some(begin, begin + 1)
    1.12 +      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
    1.13 +      case (Some(start), None) => Some(Text.Range(start, start + 1))
    1.14        case (None, _) => None
    1.15      }
    1.16  
    1.17    object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
    1.18 -  object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
    1.19 +  object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
    1.20  }
     2.1 --- a/src/Pure/General/symbol.scala	Wed Aug 18 14:04:13 2010 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Wed Aug 18 23:44:50 2010 +0200
     2.3 @@ -106,8 +106,9 @@
     2.4        }
     2.5        buf.toArray
     2.6      }
     2.7 -    def decode(sym: Int): Int =
     2.8 +    def decode(sym1: Int): Int =
     2.9      {
    2.10 +      val sym = sym1 - 1
    2.11        val end = index.length
    2.12        def bisect(a: Int, b: Int): Int =
    2.13        {
    2.14 @@ -123,6 +124,7 @@
    2.15        if (i < 0) sym
    2.16        else index(i).chr + sym - index(i).sym
    2.17      }
    2.18 +    def decode(range: Text.Range): Text.Range = range.map(decode(_))
    2.19    }
    2.20  
    2.21  
     3.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 18 14:04:13 2010 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 18 23:44:50 2010 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4      val command: Command,
     3.5      val status: List[Markup],
     3.6      val reverse_results: List[XML.Tree],
     3.7 -    val markup: Markup_Text)
     3.8 +    val markup: Markup_Tree)
     3.9    {
    3.10      /* content */
    3.11  
    3.12 @@ -37,23 +37,26 @@
    3.13  
    3.14      def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    3.15  
    3.16 -    def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
    3.17 +    def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
    3.18 +
    3.19 +    def markup_root_node: Markup_Tree.Node = new Markup_Tree.Node(command.range, status)
    3.20 +    def markup_root: Markup_Tree = markup + markup_root_node
    3.21  
    3.22  
    3.23      /* markup */
    3.24  
    3.25 -    lazy val highlight: Markup_Text =
    3.26 +    lazy val highlight: List[Markup_Tree.Node] =
    3.27      {
    3.28        markup.filter(_.info match {
    3.29          case Command.HighlightInfo(_, _) => true
    3.30          case _ => false
    3.31 -      })
    3.32 +      }).flatten(markup_root_node)
    3.33      }
    3.34  
    3.35 -    private lazy val types: List[Markup_Node] =
    3.36 +    private lazy val types: List[Markup_Tree.Node] =
    3.37        markup.filter(_.info match {
    3.38          case Command.TypeInfo(_) => true
    3.39 -        case _ => false }).flatten
    3.40 +        case _ => false }).flatten(markup_root_node)
    3.41  
    3.42      def type_at(pos: Text.Offset): Option[String] =
    3.43      {
    3.44 @@ -67,12 +70,12 @@
    3.45        }
    3.46      }
    3.47  
    3.48 -    private lazy val refs: List[Markup_Node] =
    3.49 +    private lazy val refs: List[Markup_Tree.Node] =
    3.50        markup.filter(_.info match {
    3.51          case Command.RefInfo(_, _, _, _) => true
    3.52 -        case _ => false }).flatten
    3.53 +        case _ => false }).flatten(markup_root_node)
    3.54  
    3.55 -    def ref_at(pos: Text.Offset): Option[Markup_Node] =
    3.56 +    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
    3.57        refs.find(_.range.contains(pos))
    3.58  
    3.59  
    3.60 @@ -88,18 +91,16 @@
    3.61              elem match {
    3.62                case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
    3.63                  atts match {
    3.64 -                  case Position.Range(begin, end) =>
    3.65 +                  case Position.Range(range) =>
    3.66                      if (kind == Markup.ML_TYPING) {
    3.67                        val info = Pretty.string_of(body, margin = 40)
    3.68 -                      state.add_markup(
    3.69 -                        command.markup_node(begin, end, Command.TypeInfo(info)))
    3.70 +                      state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
    3.71                      }
    3.72                      else if (kind == Markup.ML_REF) {
    3.73                        body match {
    3.74                          case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
    3.75                            state.add_markup(
    3.76 -                            command.markup_node(
    3.77 -                              begin, end,
    3.78 +                            command.decode_range(range,
    3.79                                Command.RefInfo(
    3.80                                  Position.get_file(props),
    3.81                                  Position.get_line(props),
    3.82 @@ -110,7 +111,7 @@
    3.83                      }
    3.84                      else {
    3.85                        state.add_markup(
    3.86 -                        command.markup_node(begin, end,
    3.87 +                        command.decode_range(range,
    3.88                            Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
    3.89                      }
    3.90                    case _ => state
    3.91 @@ -151,21 +152,18 @@
    3.92    val source: String = span.map(_.source).mkString
    3.93    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    3.94    def length: Int = source.length
    3.95 +  val range: Text.Range = Text.Range(0, length)
    3.96  
    3.97    lazy val symbol_index = new Symbol.Index(source)
    3.98  
    3.99  
   3.100    /* markup */
   3.101  
   3.102 -  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   3.103 -  {
   3.104 -    val start = symbol_index.decode(begin - 1)
   3.105 -    val stop = symbol_index.decode(end - 1)
   3.106 -    new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
   3.107 -  }
   3.108 +  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
   3.109 +    new Markup_Tree.Node(symbol_index.decode(range), info)
   3.110  
   3.111  
   3.112    /* accumulated results */
   3.113  
   3.114 -  val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
   3.115 +  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
   3.116  }
     4.1 --- a/src/Pure/PIDE/markup_node.scala	Wed Aug 18 14:04:13 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,104 +0,0 @@
     4.4 -/*  Title:      Pure/PIDE/markup_node.scala
     4.5 -    Author:     Fabian Immler, TU Munich
     4.6 -    Author:     Makarius
     4.7 -
     4.8 -Text markup nodes.
     4.9 -*/
    4.10 -
    4.11 -package isabelle
    4.12 -
    4.13 -
    4.14 -import javax.swing.tree.DefaultMutableTreeNode
    4.15 -
    4.16 -
    4.17 -
    4.18 -case class Markup_Node(val range: Text.Range, val info: Any)
    4.19 -
    4.20 -case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
    4.21 -{
    4.22 -  private def add(branch: Markup_Tree) =   // FIXME avoid sort
    4.23 -    copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
    4.24 -
    4.25 -  private def remove(bs: List[Markup_Tree]) =
    4.26 -    copy(branches = branches.filterNot(bs.contains(_)))
    4.27 -
    4.28 -  def + (new_tree: Markup_Tree): Markup_Tree =
    4.29 -  {
    4.30 -    val new_node = new_tree.node
    4.31 -    if (node.range contains new_node.range) {
    4.32 -      var inserted = false
    4.33 -      val new_branches =
    4.34 -        branches.map(branch =>
    4.35 -          if ((branch.node.range contains new_node.range) && !inserted) {
    4.36 -            inserted = true
    4.37 -            branch + new_tree
    4.38 -          }
    4.39 -          else branch)
    4.40 -      if (!inserted) {
    4.41 -        // new_tree did not fit into children of this
    4.42 -        // -> insert between this and its branches
    4.43 -        val fitting = branches filter(new_node.range contains _.node.range)
    4.44 -        (this remove fitting) add ((new_tree /: fitting)(_ + _))
    4.45 -      }
    4.46 -      else copy(branches = new_branches)
    4.47 -    }
    4.48 -    else {
    4.49 -      System.err.println("Ignored nonfitting markup: " + new_node)
    4.50 -      this
    4.51 -    }
    4.52 -  }
    4.53 -
    4.54 -  def flatten: List[Markup_Node] =
    4.55 -  {
    4.56 -    var next_x = node.range.start
    4.57 -    if (branches.isEmpty) List(this.node)
    4.58 -    else {
    4.59 -      val filled_gaps =
    4.60 -        for {
    4.61 -          child <- branches
    4.62 -          markups =
    4.63 -            if (next_x < child.node.range.start)
    4.64 -              new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
    4.65 -            else child.flatten
    4.66 -          update = (next_x = child.node.range.stop)
    4.67 -          markup <- markups
    4.68 -        } yield markup
    4.69 -      if (next_x < node.range.stop)
    4.70 -        filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
    4.71 -      else filled_gaps
    4.72 -    }
    4.73 -  }
    4.74 -}
    4.75 -
    4.76 -
    4.77 -case class Markup_Text(val markup: List[Markup_Tree], val content: String)
    4.78 -{
    4.79 -  private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup)  // FIXME !?
    4.80 -
    4.81 -  def + (new_tree: Markup_Tree): Markup_Text =
    4.82 -    new Markup_Text((root + new_tree).branches, content)
    4.83 -
    4.84 -  def filter(pred: Markup_Node => Boolean): Markup_Text =
    4.85 -  {
    4.86 -    def filt(tree: Markup_Tree): List[Markup_Tree] =
    4.87 -    {
    4.88 -      val branches = tree.branches.flatMap(filt(_))
    4.89 -      if (pred(tree.node)) List(tree.copy(branches = branches))
    4.90 -      else branches
    4.91 -    }
    4.92 -    new Markup_Text(markup.flatMap(filt(_)), content)
    4.93 -  }
    4.94 -
    4.95 -  def flatten: List[Markup_Node] = markup.flatMap(_.flatten)
    4.96 -
    4.97 -  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
    4.98 -  {
    4.99 -    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
   4.100 -    {
   4.101 -      val node = swing_node(tree.node)
   4.102 -      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
   4.103 -      node
   4.104 -    }
   4.105 -    swing(root)
   4.106 -  }
   4.107 -}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 18 23:44:50 2010 +0200
     5.3 @@ -0,0 +1,113 @@
     5.4 +/*  Title:      Pure/PIDE/markup_tree.scala
     5.5 +    Author:     Fabian Immler, TU Munich
     5.6 +    Author:     Makarius
     5.7 +
     5.8 +Markup trees over nested / non-overlapping text ranges.
     5.9 +*/
    5.10 +
    5.11 +package isabelle
    5.12 +
    5.13 +
    5.14 +import javax.swing.tree.DefaultMutableTreeNode
    5.15 +
    5.16 +import scala.collection.immutable.SortedMap
    5.17 +import scala.collection.mutable
    5.18 +import scala.annotation.tailrec
    5.19 +
    5.20 +
    5.21 +object Markup_Tree
    5.22 +{
    5.23 +  case class Node(val range: Text.Range, val info: Any)
    5.24 +
    5.25 +
    5.26 +  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
    5.27 +
    5.28 +  object Branches
    5.29 +  {
    5.30 +    type Entry = (Node, Markup_Tree)
    5.31 +    type T = SortedMap[Node, Entry]
    5.32 +
    5.33 +    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
    5.34 +      {
    5.35 +        def compare(x: Node, y: Node): Int = x.range compare y.range
    5.36 +      })
    5.37 +    def update(branches: T, entries: Entry*): T =
    5.38 +      branches ++ entries.map(e => (e._1 -> e))
    5.39 +    def make(entries: List[Entry]): T = update(empty, entries:_*)
    5.40 +  }
    5.41 +
    5.42 +  val empty = new Markup_Tree(Branches.empty)
    5.43 +}
    5.44 +
    5.45 +
    5.46 +case class Markup_Tree(val branches: Markup_Tree.Branches.T)
    5.47 +{
    5.48 +  import Markup_Tree._
    5.49 +
    5.50 +  def + (new_node: Node): Markup_Tree =
    5.51 +  {
    5.52 +    // FIXME tune overlapping == branches && rest.isEmpty
    5.53 +    val (overlapping, rest) =
    5.54 +    {
    5.55 +      val overlapping = new mutable.ListBuffer[Branches.Entry]
    5.56 +      var rest = branches
    5.57 +      while (rest.isDefinedAt(new_node)) {
    5.58 +        overlapping += rest(new_node)
    5.59 +        rest -= new_node
    5.60 +      }
    5.61 +      (overlapping.toList, rest)
    5.62 +    }
    5.63 +    overlapping match {
    5.64 +      case Nil =>
    5.65 +        new Markup_Tree(Branches.update(branches, new_node -> empty))
    5.66 +
    5.67 +      case List((node, subtree))
    5.68 +        if node.range != new_node.range && (node.range contains new_node.range) =>
    5.69 +        new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
    5.70 +
    5.71 +      case _ if overlapping.forall(e => new_node.range contains e._1.range) =>
    5.72 +        val new_tree = new Markup_Tree(Branches.make(overlapping))
    5.73 +        new Markup_Tree(Branches.update(rest, new_node -> new_tree))
    5.74 +
    5.75 +      case _ => // FIXME split markup!?
    5.76 +        System.err.println("Ignored overlapping markup: " + new_node); this
    5.77 +    }
    5.78 +  }
    5.79 +
    5.80 +  // FIXME depth-first with result markup stack
    5.81 +  // FIXME projection to given range
    5.82 +  def flatten(parent: Node): List[Node] =
    5.83 +  {
    5.84 +    val result = new mutable.ListBuffer[Node]
    5.85 +    var offset = parent.range.start
    5.86 +    for ((_, (node, subtree)) <- branches.iterator) {
    5.87 +      if (offset < node.range.start)
    5.88 +        result += new Node(Text.Range(offset, node.range.start), parent.info)
    5.89 +      result ++= subtree.flatten(node)
    5.90 +      offset = node.range.stop
    5.91 +    }
    5.92 +    if (offset < parent.range.stop)
    5.93 +      result += new Node(Text.Range(offset, parent.range.stop), parent.info)
    5.94 +    result.toList
    5.95 +  }
    5.96 +
    5.97 +  def filter(pred: Node => Boolean): Markup_Tree =
    5.98 +  {
    5.99 +    val bs = branches.toList.flatMap(entry => {
   5.100 +      val (_, (node, subtree)) = entry
   5.101 +      if (pred(node)) List((node, (node, subtree.filter(pred))))
   5.102 +      else subtree.filter(pred).branches.toList
   5.103 +    })
   5.104 +    new Markup_Tree(Branches.empty ++ bs)
   5.105 +  }
   5.106 +
   5.107 +  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
   5.108 +  {
   5.109 +    for ((_, (node, subtree)) <- branches) {
   5.110 +      val current = swing_node(node)
   5.111 +      subtree.swing_tree(current)(swing_node)
   5.112 +      parent.add(current)
   5.113 +    }
   5.114 +  }
   5.115 +}
   5.116 +
     6.1 --- a/src/Pure/build-jars	Wed Aug 18 14:04:13 2010 +0200
     6.2 +++ b/src/Pure/build-jars	Wed Aug 18 23:44:50 2010 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4    Isar/token.scala
     6.5    PIDE/command.scala
     6.6    PIDE/document.scala
     6.7 -  PIDE/markup_node.scala
     6.8 +  PIDE/markup_tree.scala
     6.9    PIDE/text.scala
    6.10    System/cygwin.scala
    6.11    System/download.scala
     7.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Aug 18 14:04:13 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Aug 18 23:44:50 2010 +0200
     7.3 @@ -279,7 +279,7 @@
     7.4        for {
     7.5          (command, command_start) <-
     7.6            snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
     7.7 -        markup <- snapshot.state(command).highlight.flatten
     7.8 +        markup <- snapshot.state(command).highlight
     7.9          val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
    7.10          if (abs_stop > start)
    7.11          if (abs_start < stop)
     8.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 18 14:04:13 2010 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 18 23:44:50 2010 +0200
     8.3 @@ -79,7 +79,7 @@
     8.4        case Some((word, cs)) =>
     8.5          val ds =
     8.6            (if (Isabelle_Encoding.is_active(buffer))
     8.7 -            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
     8.8 +            cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
     8.9             else cs).filter(_ != word)
    8.10          if (ds.isEmpty) null
    8.11          else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
    8.12 @@ -129,7 +129,7 @@
    8.13      val root = data.root
    8.14      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
    8.15      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
    8.16 -      root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
    8.17 +      snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) =>
    8.18            {
    8.19              val content = command.source(node.range).replace('\n', ' ')
    8.20              val id = command.id
    8.21 @@ -146,7 +146,7 @@
    8.22                override def getEnd: Position = command_start + node.range.stop
    8.23                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    8.24              })
    8.25 -          }))
    8.26 +          })
    8.27      }
    8.28    }
    8.29  }