renamed Markup_Tree.Node to Text.Info;
authorwenzelm
Sun Aug 22 18:46:16 2010 +0200 (2010-08-22 ago)
changeset 385774e4d3ea3725a
parent 38576 ce3eed2b16f7
child 38578 1ebc6b76e5ff
renamed Markup_Tree.Node to Text.Info;
Markup_Tree.select: body may depend on full Text.Info, including range;
tuned;
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.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
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 22 16:43:20 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 22 18:46:16 2010 +0200
     1.3 @@ -28,11 +28,11 @@
     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[Any]): State = copy(markup = markup + node)
     1.8 +    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
     1.9  
    1.10 -    def markup_root_node: Markup_Tree.Node[Any] =
    1.11 -      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
    1.12 -    def markup_root: Markup_Tree = markup + markup_root_node
    1.13 +    def markup_root_info: Text.Info[Any] =
    1.14 +      new Text.Info(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
    1.15 +    def markup_root: Markup_Tree = markup + markup_root_info
    1.16  
    1.17  
    1.18      /* message dispatch */
    1.19 @@ -47,8 +47,8 @@
    1.20                if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
    1.21                  val range = command.decode_range(Position.get_range(atts).get)
    1.22                  val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    1.23 -                val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args))
    1.24 -                add_markup(node)
    1.25 +                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    1.26 +                add_markup(info)
    1.27                case _ => System.err.println("Ignored report message: " + msg); state
    1.28              })
    1.29          case _ => add_result(message)
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 16:43:20 2010 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 18:46:16 2010 +0200
     2.3 @@ -17,31 +17,24 @@
     2.4  
     2.5  object Markup_Tree
     2.6  {
     2.7 -  case class Node[A](val range: Text.Range, val info: A)
     2.8 -  {
     2.9 -    def contains[B](that: Node[B]): Boolean = this.range contains that.range
    2.10 -    def restrict(r: Text.Range): Node[A] = Node(range.restrict(r), info)
    2.11 -  }
    2.12 -
    2.13 -
    2.14    /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
    2.15  
    2.16    object Branches
    2.17    {
    2.18 -    type Entry = (Node[Any], Markup_Tree)
    2.19 -    type T = SortedMap[Node[Any], Entry]
    2.20 +    type Entry = (Text.Info[Any], Markup_Tree)
    2.21 +    type T = SortedMap[Text.Info[Any], Entry]
    2.22  
    2.23 -    val empty = SortedMap.empty[Node[Any], Entry](new scala.math.Ordering[Node[Any]]
    2.24 +    val empty = SortedMap.empty[Text.Info[Any], Entry](new scala.math.Ordering[Text.Info[Any]]
    2.25        {
    2.26 -        def compare(x: Node[Any], y: Node[Any]): Int = x.range compare y.range
    2.27 +        def compare(x: Text.Info[Any], y: Text.Info[Any]): Int = x.range compare y.range
    2.28        })
    2.29  
    2.30      def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
    2.31  
    2.32      def overlapping(range: Text.Range, branches: T): T =
    2.33      {
    2.34 -      val start = Node[Any](Text.Range(range.start), Nil)
    2.35 -      val stop = Node[Any](Text.Range(range.stop), Nil)
    2.36 +      val start = Text.Info[Any](Text.Range(range.start), Nil)
    2.37 +      val stop = Text.Info[Any](Text.Range(range.stop), Nil)
    2.38        branches.get(stop) match {
    2.39          case Some(end) if range overlaps end._1.range =>
    2.40            update(branches.range(start, stop), end)
    2.41 @@ -64,49 +57,50 @@
    2.42        case list => list.mkString("Tree(", ",", ")")
    2.43      }
    2.44  
    2.45 -  def + (new_node: Node[Any]): Markup_Tree =
    2.46 +  def + (new_info: Text.Info[Any]): Markup_Tree =
    2.47    {
    2.48 -    branches.get(new_node) match {
    2.49 +    branches.get(new_info) match {
    2.50        case None =>
    2.51 -        new Markup_Tree(Branches.update(branches, new_node -> empty))
    2.52 -      case Some((node, subtree)) =>
    2.53 -        if (node.range != new_node.range && node.contains(new_node))
    2.54 -          new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
    2.55 -        else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
    2.56 -          new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
    2.57 +        new Markup_Tree(Branches.update(branches, new_info -> empty))
    2.58 +      case Some((info, subtree)) =>
    2.59 +        if (info.range != new_info.range && info.contains(new_info))
    2.60 +          new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
    2.61 +        else if (new_info.contains(branches.head._1) && new_info.contains(branches.last._1))
    2.62 +          new Markup_Tree(Branches.update(Branches.empty, (new_info -> this)))
    2.63          else {
    2.64 -          val body = Branches.overlapping(new_node.range, branches)
    2.65 -          if (body.forall(e => new_node.contains(e._1))) {
    2.66 +          val body = Branches.overlapping(new_info.range, branches)
    2.67 +          if (body.forall(e => new_info.contains(e._1))) {
    2.68              val rest = (branches /: body) { case (bs, (e, _)) => bs - e }
    2.69 -            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(body)))
    2.70 +            new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
    2.71            }
    2.72            else { // FIXME split markup!?
    2.73 -            System.err.println("Ignored overlapping markup: " + new_node)
    2.74 +            System.err.println("Ignored overlapping markup information: " + new_info)
    2.75              this
    2.76            }
    2.77          }
    2.78      }
    2.79    }
    2.80  
    2.81 -  def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
    2.82 +  def select[A](root: Text.Info[A])(sel: PartialFunction[Text.Info[Any], A]): Stream[Text.Info[A]] =
    2.83    {
    2.84 -    def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =
    2.85 +    def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
    2.86      {
    2.87        val substream =
    2.88 -        (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
    2.89 -          if (sel.isDefinedAt(node.info)) {
    2.90 -            val current = Node(node.range.restrict(parent.range), sel(node.info))
    2.91 +        (for ((_, (info, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
    2.92 +          if (sel.isDefinedAt(info)) {
    2.93 +            val current = Text.Info(info.range.restrict(parent.range), sel(info))
    2.94              stream(current, subtree.branches)
    2.95            }
    2.96 -          else stream(parent.restrict(node.range), subtree.branches)
    2.97 +          else stream(parent.restrict(info.range), subtree.branches)
    2.98          }).flatten
    2.99  
   2.100 -      def padding(last: Text.Offset, s: Stream[Node[A]]): Stream[Node[A]] =
   2.101 +      def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] =
   2.102          s match {
   2.103 -          case (node @ Node(Text.Range(start, stop), _)) #:: rest =>
   2.104 +          case info #:: rest =>
   2.105 +            val Text.Range(start, stop) = info.range
   2.106              if (last < start)
   2.107 -              parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest)
   2.108 -            else node #:: padding(stop, rest)
   2.109 +              parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest)
   2.110 +            else info #:: padding(stop, rest)
   2.111            case Stream.Empty =>
   2.112              if (last < parent.range.stop)
   2.113                Stream(parent.restrict(Text.Range(last, parent.range.stop)))
   2.114 @@ -118,10 +112,11 @@
   2.115      stream(root, branches)
   2.116    }
   2.117  
   2.118 -  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode)
   2.119 +  def swing_tree(parent: DefaultMutableTreeNode)
   2.120 +    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
   2.121    {
   2.122 -    for ((_, (node, subtree)) <- branches) {
   2.123 -      val current = swing_node(node)
   2.124 +    for ((_, (info, subtree)) <- branches) {
   2.125 +      val current = swing_node(info)
   2.126        subtree.swing_tree(current)(swing_node)
   2.127        parent.add(current)
   2.128      }
     3.1 --- a/src/Pure/PIDE/text.scala	Sun Aug 22 16:43:20 2010 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 22 18:46:16 2010 +0200
     3.3 @@ -42,6 +42,15 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* information associated with text range */
     3.8 +
     3.9 +  case class Info[A](val range: Text.Range, val info: A)
    3.10 +  {
    3.11 +    def contains[B](that: Info[B]): Boolean = this.range contains that.range
    3.12 +    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    3.13 +  }
    3.14 +
    3.15 +
    3.16    /* editing */
    3.17  
    3.18    object Edit
     4.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 16:43:20 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 18:46:16 2010 +0200
     4.3 @@ -279,13 +279,13 @@
     4.4          handler.handleToken(line_segment, style, offset, length, context)
     4.5  
     4.6        val syntax = session.current_syntax()
     4.7 -      val token_markup: PartialFunction[Any, Byte] =
     4.8 +      val token_markup: PartialFunction[Text.Info[Any], Byte] =
     4.9        {
    4.10 -        case XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)
    4.11 +        case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
    4.12          if syntax.keyword_kind(name).isDefined =>
    4.13            Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
    4.14  
    4.15 -        case XML.Elem(Markup(name, _), _)
    4.16 +        case Text.Info(_, XML.Elem(Markup(name, _), _))
    4.17          if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
    4.18            Document_Model.Token_Markup.token_style(name)
    4.19        }
    4.20 @@ -293,10 +293,9 @@
    4.21        var next_x = start
    4.22        for {
    4.23          (command, command_start) <- snapshot.node.command_range(former_range)
    4.24 -        val root_node =
    4.25 -          Markup_Tree.Node((former_range - command_start).restrict(command.range), Token.NULL)
    4.26 -        node <- snapshot.state(command).markup.select(root_node)(token_markup)
    4.27 -        val Text.Range(abs_start, abs_stop) = snapshot.convert(node.range + command_start)
    4.28 +        val root = Text.Info((former_range - command_start).restrict(command.range), Token.NULL)
    4.29 +        info <- snapshot.state(command).markup.select(root)(token_markup)
    4.30 +        val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
    4.31          if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
    4.32        }
    4.33        {
    4.34 @@ -307,7 +306,7 @@
    4.35            ((abs_stop - stop) max 0)
    4.36          if (start + token_start > next_x)  // FIXME ??
    4.37            handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
    4.38 -        handle_token(node.info, token_start, token_length)
    4.39 +        handle_token(info.info, token_start, token_length)
    4.40          next_x = start + token_start + token_length
    4.41        }
    4.42        if (next_x < stop)  // FIXME ??
     5.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 16:43:20 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 18:46:16 2010 +0200
     5.3 @@ -202,13 +202,12 @@
     5.4        val offset = snapshot.revert(text_area.xyToOffset(x, y))
     5.5        snapshot.node.command_at(offset) match {
     5.6          case Some((command, command_start)) =>
     5.7 -          val root_node =
     5.8 -            Markup_Tree.Node[Option[XML.Body]]((Text.Range(offset) - command_start), None)
     5.9 -          snapshot.state(command).markup.select(root_node) {
    5.10 -            case XML.Elem(Markup(Markup.ML_TYPING, _), body) => Some(body)
    5.11 +          val root = Text.Info[Option[XML.Body]]((Text.Range(offset) - command_start), None)
    5.12 +          snapshot.state(command).markup.select(root) {
    5.13 +            case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => Some(body)
    5.14            } match {
    5.15              // FIXME use original node range, not restricted version
    5.16 -            case Markup_Tree.Node(range, Some(body)) #:: _ =>
    5.17 +            case Text.Info(range, Some(body)) #:: _ =>
    5.18                val typing =
    5.19                  Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
    5.20                Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
     6.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 16:43:20 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 18:46:16 2010 +0200
     6.3 @@ -47,15 +47,13 @@
     6.4          val offset = snapshot.revert(buffer_offset)
     6.5          snapshot.node.command_at(offset) match {
     6.6            case Some((command, command_start)) =>
     6.7 -            val root_node =
     6.8 -              Markup_Tree.Node[Hyperlink]((Text.Range(offset) - command_start), null)
     6.9 -
    6.10 -            (snapshot.state(command).markup.select(root_node) {
    6.11 -              case XML.Elem(Markup(Markup.ML_REF, _),
    6.12 -                  List(XML.Elem(Markup(Markup.ML_DEF, props), _))) =>
    6.13 +            val root = Text.Info[Hyperlink]((Text.Range(offset) - command_start), null)
    6.14 +            (snapshot.state(command).markup.select(root) {
    6.15 +              case Text.Info(_, XML.Elem(Markup(Markup.ML_REF, _),
    6.16 +                  List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
    6.17  //{{{
    6.18 -                val node_range = root_node.range // FIXME proper range
    6.19 -                val Text.Range(begin, end) = snapshot.convert(node_range + command_start)
    6.20 +                val info_range = root.range // FIXME proper range
    6.21 +                val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
    6.22                  val line = buffer.getLineOfOffset(begin)
    6.23  
    6.24                  (Position.get_file(props), Position.get_line(props)) match {
     7.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 22 16:43:20 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 22 18:46:16 2010 +0200
     7.3 @@ -129,21 +129,21 @@
     7.4      val root = data.root
     7.5      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     7.6      for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     7.7 -      snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node[Any]) =>
     7.8 +      snapshot.state(command).markup_root.swing_tree(root)((info: Text.Info[Any]) =>
     7.9            {
    7.10 -            val content = command.source(node.range).replace('\n', ' ')
    7.11 +            val content = command.source(info.range).replace('\n', ' ')
    7.12              val id = command.id
    7.13  
    7.14              new DefaultMutableTreeNode(new IAsset {
    7.15                override def getIcon: Icon = null
    7.16                override def getShortString: String = content
    7.17 -              override def getLongString: String = node.info.toString
    7.18 +              override def getLongString: String = info.info.toString
    7.19                override def getName: String = Markup.Long(id)
    7.20                override def setName(name: String) = ()
    7.21                override def setStart(start: Position) = ()
    7.22 -              override def getStart: Position = command_start + node.range.start
    7.23 +              override def getStart: Position = command_start + info.range.start
    7.24                override def setEnd(end: Position) = ()
    7.25 -              override def getEnd: Position = command_start + node.range.stop
    7.26 +              override def getEnd: Position = command_start + info.range.stop
    7.27                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    7.28              })
    7.29            })