src/Pure/PIDE/command.scala
changeset 38479 e628da370072
parent 38476 d72479a07882
child 38480 e5eed57913d0
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 18 14:04:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 18 23:44:50 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4      val command: Command,
     1.5      val status: List[Markup],
     1.6      val reverse_results: List[XML.Tree],
     1.7 -    val markup: Markup_Text)
     1.8 +    val markup: Markup_Tree)
     1.9    {
    1.10      /* content */
    1.11  
    1.12 @@ -37,23 +37,26 @@
    1.13  
    1.14      def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    1.15  
    1.16 -    def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
    1.17 +    def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
    1.18 +
    1.19 +    def markup_root_node: Markup_Tree.Node = new Markup_Tree.Node(command.range, status)
    1.20 +    def markup_root: Markup_Tree = markup + markup_root_node
    1.21  
    1.22  
    1.23      /* markup */
    1.24  
    1.25 -    lazy val highlight: Markup_Text =
    1.26 +    lazy val highlight: List[Markup_Tree.Node] =
    1.27      {
    1.28        markup.filter(_.info match {
    1.29          case Command.HighlightInfo(_, _) => true
    1.30          case _ => false
    1.31 -      })
    1.32 +      }).flatten(markup_root_node)
    1.33      }
    1.34  
    1.35 -    private lazy val types: List[Markup_Node] =
    1.36 +    private lazy val types: List[Markup_Tree.Node] =
    1.37        markup.filter(_.info match {
    1.38          case Command.TypeInfo(_) => true
    1.39 -        case _ => false }).flatten
    1.40 +        case _ => false }).flatten(markup_root_node)
    1.41  
    1.42      def type_at(pos: Text.Offset): Option[String] =
    1.43      {
    1.44 @@ -67,12 +70,12 @@
    1.45        }
    1.46      }
    1.47  
    1.48 -    private lazy val refs: List[Markup_Node] =
    1.49 +    private lazy val refs: List[Markup_Tree.Node] =
    1.50        markup.filter(_.info match {
    1.51          case Command.RefInfo(_, _, _, _) => true
    1.52 -        case _ => false }).flatten
    1.53 +        case _ => false }).flatten(markup_root_node)
    1.54  
    1.55 -    def ref_at(pos: Text.Offset): Option[Markup_Node] =
    1.56 +    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
    1.57        refs.find(_.range.contains(pos))
    1.58  
    1.59  
    1.60 @@ -88,18 +91,16 @@
    1.61              elem match {
    1.62                case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
    1.63                  atts match {
    1.64 -                  case Position.Range(begin, end) =>
    1.65 +                  case Position.Range(range) =>
    1.66                      if (kind == Markup.ML_TYPING) {
    1.67                        val info = Pretty.string_of(body, margin = 40)
    1.68 -                      state.add_markup(
    1.69 -                        command.markup_node(begin, end, Command.TypeInfo(info)))
    1.70 +                      state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
    1.71                      }
    1.72                      else if (kind == Markup.ML_REF) {
    1.73                        body match {
    1.74                          case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
    1.75                            state.add_markup(
    1.76 -                            command.markup_node(
    1.77 -                              begin, end,
    1.78 +                            command.decode_range(range,
    1.79                                Command.RefInfo(
    1.80                                  Position.get_file(props),
    1.81                                  Position.get_line(props),
    1.82 @@ -110,7 +111,7 @@
    1.83                      }
    1.84                      else {
    1.85                        state.add_markup(
    1.86 -                        command.markup_node(begin, end,
    1.87 +                        command.decode_range(range,
    1.88                            Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
    1.89                      }
    1.90                    case _ => state
    1.91 @@ -151,21 +152,18 @@
    1.92    val source: String = span.map(_.source).mkString
    1.93    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.94    def length: Int = source.length
    1.95 +  val range: Text.Range = Text.Range(0, length)
    1.96  
    1.97    lazy val symbol_index = new Symbol.Index(source)
    1.98  
    1.99  
   1.100    /* markup */
   1.101  
   1.102 -  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   1.103 -  {
   1.104 -    val start = symbol_index.decode(begin - 1)
   1.105 -    val stop = symbol_index.decode(end - 1)
   1.106 -    new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
   1.107 -  }
   1.108 +  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
   1.109 +    new Markup_Tree.Node(symbol_index.decode(range), info)
   1.110  
   1.111  
   1.112    /* accumulated results */
   1.113  
   1.114 -  val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
   1.115 +  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
   1.116  }