more general / abstract Command.Markups, with separate index for status elements;
authorwenzelm
Fri Feb 21 15:12:50 2014 +0100 (2014-02-21 ago)
changeset 556491532ab0dc67b
parent 55648 38f264741609
child 55650 349afd0fa0c4
more general / abstract Command.Markups, with separate index for status elements;
slightly faster Rendering.overview_color;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Feb 21 13:36:40 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Feb 21 15:12:50 2014 +0100
     1.3 @@ -56,18 +56,59 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* markup */
     1.8 +
     1.9 +  object Markup_Index
    1.10 +  {
    1.11 +    val markup: Markup_Index = Markup_Index(false, "")
    1.12 +  }
    1.13 +
    1.14 +  sealed case class Markup_Index(status: Boolean, file_name: String)
    1.15 +
    1.16 +  object Markups
    1.17 +  {
    1.18 +    val empty: Markups = new Markups(Map.empty)
    1.19 +
    1.20 +    def init(markup: Markup_Tree): Markups =
    1.21 +      new Markups(Map(Markup_Index.markup -> markup))
    1.22 +  }
    1.23 +
    1.24 +  final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
    1.25 +  {
    1.26 +    def apply(index: Markup_Index): Markup_Tree =
    1.27 +      rep.getOrElse(index, Markup_Tree.empty)
    1.28 +
    1.29 +    def add(index: Markup_Index, markup: Text.Markup): Markups =
    1.30 +      new Markups(rep + (index -> (this(index) + markup)))
    1.31 +
    1.32 +    def ++ (other: Markups): Markups =
    1.33 +      new Markups(
    1.34 +        (rep.keySet ++ other.rep.keySet)
    1.35 +          .map(index => index -> (this(index) ++ other(index))).toMap)
    1.36 +
    1.37 +    override def hashCode: Int = rep.hashCode
    1.38 +    override def equals(that: Any): Boolean =
    1.39 +      that match {
    1.40 +        case other: Markups => rep == other.rep
    1.41 +        case _ => false
    1.42 +      }
    1.43 +    override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
    1.44 +  }
    1.45 +
    1.46 +
    1.47    /* state */
    1.48  
    1.49    sealed case class State(
    1.50      command: Command,
    1.51      status: List[Markup] = Nil,
    1.52      results: Results = Results.empty,
    1.53 -    markups: Map[String, Markup_Tree] = Map.empty)
    1.54 +    markups: Markups = Markups.empty)
    1.55    {
    1.56 -    def get_markup(file_name: String): Markup_Tree =
    1.57 -      markups.getOrElse(file_name, Markup_Tree.empty)
    1.58 +    /* markup */
    1.59  
    1.60 -    def markup: Markup_Tree = get_markup("")
    1.61 +    def get_markup(index: Markup_Index): Markup_Tree = markups(index)
    1.62 +
    1.63 +    def markup: Markup_Tree = get_markup(Markup_Index.markup)
    1.64  
    1.65      def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
    1.66        markup.to_XML(command.range, command.source, filter)
    1.67 @@ -81,10 +122,17 @@
    1.68        results == other.results &&
    1.69        markups == other.markups
    1.70  
    1.71 -    private def add_status(st: Markup): State = copy(status = st :: status)
    1.72 +    private def add_status(st: Markup): State =
    1.73 +      copy(status = st :: status)
    1.74  
    1.75 -    private def add_markup(file_name: String, m: Text.Markup): State =
    1.76 -      copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
    1.77 +    private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
    1.78 +    {
    1.79 +      val markups1 =
    1.80 +        if (status || Protocol.status_elements(m.info.name))
    1.81 +          markups.add(Markup_Index(true, file_name), m)
    1.82 +        else markups
    1.83 +      copy(markups = markups1.add(Markup_Index(false, file_name), m))
    1.84 +    }
    1.85  
    1.86      def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
    1.87        message match {
    1.88 @@ -92,8 +140,9 @@
    1.89            (this /: msgs)((state, msg) =>
    1.90              msg match {
    1.91                case elem @ XML.Elem(markup, Nil) =>
    1.92 -                state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
    1.93 -
    1.94 +                state.
    1.95 +                  add_status(markup).
    1.96 +                  add_markup(true, "", Text.Info(command.proper_range, elem))
    1.97                case _ =>
    1.98                  System.err.println("Ignored status message: " + msg)
    1.99                  state
   1.100 @@ -113,8 +162,8 @@
   1.101                          case Some(range) =>
   1.102                            if (!range.is_singularity) {
   1.103                              val props = Position.purge(atts)
   1.104 -                            state.add_markup(file_name,
   1.105 -                              Text.Info(range, XML.Elem(Markup(name, props), args)))
   1.106 +                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
   1.107 +                            state.add_markup(false, file_name, info)
   1.108                            }
   1.109                            else state
   1.110                          case None => bad(); state
   1.111 @@ -127,7 +176,7 @@
   1.112                    val range = command.proper_range
   1.113                    val props = Position.purge(atts)
   1.114                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
   1.115 -                  state.add_markup("", info)
   1.116 +                  state.add_markup(false, "", info)
   1.117  
   1.118                  case _ => /* FIXME bad(); */ state
   1.119                }
   1.120 @@ -143,7 +192,7 @@
   1.121                  for {
   1.122                    (file_name, chunk) <- command.chunks
   1.123                    range <- Protocol.message_positions(command.id, alt_id, chunk, message)
   1.124 -                } st = st.add_markup(file_name, Text.Info(range, message2))
   1.125 +                } st = st.add_markup(false, file_name, Text.Info(range, message2))
   1.126                }
   1.127                st
   1.128  
   1.129 @@ -157,9 +206,7 @@
   1.130        copy(
   1.131          status = other.status ::: status,
   1.132          results = results ++ other.results,
   1.133 -        markups =
   1.134 -          (markups.keySet ++ other.markups.keySet)
   1.135 -            .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
   1.136 +        markups = markups ++ other.markups
   1.137        )
   1.138    }
   1.139  
   1.140 @@ -324,7 +371,7 @@
   1.141    /* accumulated results */
   1.142  
   1.143    val init_state: Command.State =
   1.144 -    Command.State(this, results = init_results, markups = Map("" -> init_markup))
   1.145 +    Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
   1.146  
   1.147    val empty_state: Command.State = Command.State(this)
   1.148  }
     2.1 --- a/src/Pure/PIDE/document.scala	Fri Feb 21 13:36:40 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Feb 21 15:12:50 2014 +0100
     2.3 @@ -357,6 +357,7 @@
     2.4      val state: State
     2.5      val version: Version
     2.6      val is_outdated: Boolean
     2.7 +
     2.8      def convert(i: Text.Offset): Text.Offset
     2.9      def revert(i: Text.Offset): Text.Offset
    2.10      def convert(range: Text.Range): Text.Range
    2.11 @@ -366,6 +367,16 @@
    2.12      val node: Node
    2.13      val thy_load_commands: List[Command]
    2.14      def eq_content(other: Snapshot): Boolean
    2.15 +
    2.16 +    def cumulate_status[A](
    2.17 +      range: Text.Range,
    2.18 +      info: A,
    2.19 +      elements: String => Boolean,
    2.20 +      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
    2.21 +    def select_status[A](
    2.22 +      range: Text.Range,
    2.23 +      elements: String => Boolean,
    2.24 +      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
    2.25      def cumulate_markup[A](
    2.26        range: Text.Range,
    2.27        info: A,
    2.28 @@ -601,14 +612,14 @@
    2.29          val version = stable.version.get_finished
    2.30          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    2.31  
    2.32 +
    2.33 +        /* local node content */
    2.34 +
    2.35          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    2.36          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.37          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    2.38          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    2.39  
    2.40 -
    2.41 -        /* local node content */
    2.42 -
    2.43          val node_name = name
    2.44          val node = version.nodes(name)
    2.45  
    2.46 @@ -629,37 +640,47 @@
    2.47            (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
    2.48          }
    2.49  
    2.50 -        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
    2.51 +
    2.52 +        /* cumulate markup */
    2.53 +
    2.54 +        private def cumulate[A](
    2.55 +          status: Boolean,
    2.56 +          range: Text.Range,
    2.57 +          info: A,
    2.58 +          elements: String => Boolean,
    2.59            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    2.60          {
    2.61            val former_range = revert(range)
    2.62            thy_load_commands match {
    2.63              case thy_load_command :: _ =>
    2.64                val file_name = node_name.node
    2.65 +              val markup_index = Command.Markup_Index(status, file_name)
    2.66                (for {
    2.67                  chunk <- thy_load_command.chunks.get(file_name).iterator
    2.68                  st = state.command_state(version, thy_load_command)
    2.69                  res = result(st)
    2.70 -                Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
    2.71 +                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
    2.72                    former_range.restrict(chunk.range), info, elements,
    2.73                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    2.74                  ).iterator
    2.75                } yield Text.Info(convert(r0), a)).toList
    2.76  
    2.77              case _ =>
    2.78 +              val markup_index = Command.Markup_Index(status, "")
    2.79                (for {
    2.80                  (command, command_start) <- node.command_range(former_range)
    2.81                  st = state.command_state(version, command)
    2.82                  res = result(st)
    2.83 -                Text.Info(r0, a) <- st.markup.cumulate[A](
    2.84 +                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
    2.85                    (former_range - command_start).restrict(command.range), info, elements,
    2.86 -                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
    2.87 -                ).iterator
    2.88 +                  {
    2.89 +                    case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
    2.90 +                  }).iterator
    2.91                } yield Text.Info(convert(r0 + command_start), a)).toList
    2.92            }
    2.93          }
    2.94  
    2.95 -        def select_markup[A](range: Text.Range, elements: String => Boolean,
    2.96 +        private def select[A](status: Boolean, range: Text.Range, elements: String => Boolean,
    2.97            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
    2.98          {
    2.99            def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
   2.100 @@ -674,6 +695,22 @@
   2.101            for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
   2.102              yield Text.Info(r, x)
   2.103          }
   2.104 +
   2.105 +        def cumulate_status[A](range: Text.Range, info: A, elements: String => Boolean,
   2.106 +            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   2.107 +          cumulate(true, range, info, elements, result)
   2.108 +
   2.109 +        def select_status[A](range: Text.Range, elements: String => Boolean,
   2.110 +            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
   2.111 +          select(true, range, elements, result)
   2.112 +
   2.113 +        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
   2.114 +            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   2.115 +          cumulate(false, range, info, elements, result)
   2.116 +
   2.117 +        def select_markup[A](range: Text.Range, elements: String => Boolean,
   2.118 +            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
   2.119 +          select(false, range, elements, result)
   2.120        }
   2.121      }
   2.122    }
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 13:36:40 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 15:12:50 2014 +0100
     3.3 @@ -301,7 +301,7 @@
     3.4      if (snapshot.is_outdated) None
     3.5      else {
     3.6        val results =
     3.7 -        snapshot.cumulate_markup[(Protocol.Status, Int)](
     3.8 +        snapshot.cumulate_status[(Protocol.Status, Int)](
     3.9            range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
    3.10            {
    3.11              case ((status, pri), Text.Info(_, elem)) =>