src/Tools/jEdit/src/rendering.scala
changeset 55622 ce575c2212fc
parent 55620 19dffae33cde
child 55623 7aea773c5574
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:08:39 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:56:51 2014 +0100
     1.3 @@ -298,18 +298,18 @@
     1.4  
     1.5    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
     1.6    {
     1.7 -    snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
     1.8 -      range, Nil, hyperlink_elements, _ =>
     1.9 +    snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    1.10 +      range, Vector.empty, hyperlink_elements, _ =>
    1.11          {
    1.12            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    1.13            if Path.is_ok(name) =>
    1.14              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    1.15              val link = PIDE.editor.hyperlink_file(jedit_file)
    1.16 -            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.17 +            Some(links :+ Text.Info(snapshot.convert(info_range), link))
    1.18  
    1.19            case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    1.20              val link = PIDE.editor.hyperlink_url(name)
    1.21 -            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.22 +            Some(links :+ Text.Info(snapshot.convert(info_range), link))
    1.23  
    1.24            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    1.25            if !props.exists(
    1.26 @@ -323,7 +323,7 @@
    1.27                  case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
    1.28                  case _ => None
    1.29                }
    1.30 -            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    1.31 +            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.32  
    1.33            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    1.34              val opt_link =
    1.35 @@ -332,15 +332,15 @@
    1.36                  case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
    1.37                  case _ => None
    1.38                }
    1.39 -            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    1.40 +            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
    1.41  
    1.42            case _ => None
    1.43 -        }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
    1.44 +        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
    1.45    }
    1.46  
    1.47  
    1.48    private val active_elements =
    1.49 -    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
    1.50 +    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
    1.51  
    1.52    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    1.53      snapshot.select_markup(range, active_elements, command_state =>
    1.54 @@ -348,6 +348,7 @@
    1.55          case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    1.56          if !command_state.results.defined(serial) =>
    1.57            Some(Text.Info(snapshot.convert(info_range), elem))
    1.58 +
    1.59          case Text.Info(info_range, elem) =>
    1.60            if (elem.name == Markup.BROWSER ||
    1.61                elem.name == Markup.GRAPHVIEW ||
    1.62 @@ -420,17 +421,19 @@
    1.63  
    1.64    def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    1.65    {
    1.66 -    def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])],
    1.67 -      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] =
    1.68 +    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    1.69 +      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    1.70      {
    1.71        val r = snapshot.convert(r0)
    1.72        val (t, info) = prev.info
    1.73 -      if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
    1.74 +      if (prev.range == r)
    1.75 +        Text.Info(r, (t, info :+ p))
    1.76 +      else Text.Info(r, (t, Vector(p)))
    1.77      }
    1.78  
    1.79      val results =
    1.80 -      snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
    1.81 -        range, Text.Info(range, (Timing.zero, Nil)), tooltip_elements, _ =>
    1.82 +      snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    1.83 +        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
    1.84          {
    1.85            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    1.86              Some(Text.Info(r, (t1 + t2, info)))
    1.87 @@ -462,7 +465,7 @@
    1.88              else None
    1.89          }).map(_.info)
    1.90  
    1.91 -    results.map(_.info).flatMap(_._2) match {
    1.92 +    results.map(_.info).flatMap(res => res._2.toList) match {
    1.93        case Nil => None
    1.94        case tips =>
    1.95          val r = Text.Range(results.head.range.start, results.last.range.stop)