src/Pure/PIDE/document.scala
changeset 55649 1532ab0dc67b
parent 55620 19dffae33cde
child 55650 349afd0fa0c4
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Feb 21 13:36:40 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Feb 21 15:12:50 2014 +0100
     1.3 @@ -357,6 +357,7 @@
     1.4      val state: State
     1.5      val version: Version
     1.6      val is_outdated: Boolean
     1.7 +
     1.8      def convert(i: Text.Offset): Text.Offset
     1.9      def revert(i: Text.Offset): Text.Offset
    1.10      def convert(range: Text.Range): Text.Range
    1.11 @@ -366,6 +367,16 @@
    1.12      val node: Node
    1.13      val thy_load_commands: List[Command]
    1.14      def eq_content(other: Snapshot): Boolean
    1.15 +
    1.16 +    def cumulate_status[A](
    1.17 +      range: Text.Range,
    1.18 +      info: A,
    1.19 +      elements: String => Boolean,
    1.20 +      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
    1.21 +    def select_status[A](
    1.22 +      range: Text.Range,
    1.23 +      elements: String => Boolean,
    1.24 +      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
    1.25      def cumulate_markup[A](
    1.26        range: Text.Range,
    1.27        info: A,
    1.28 @@ -601,14 +612,14 @@
    1.29          val version = stable.version.get_finished
    1.30          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.31  
    1.32 +
    1.33 +        /* local node content */
    1.34 +
    1.35          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.36          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.37          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.38          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.39  
    1.40 -
    1.41 -        /* local node content */
    1.42 -
    1.43          val node_name = name
    1.44          val node = version.nodes(name)
    1.45  
    1.46 @@ -629,37 +640,47 @@
    1.47            (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
    1.48          }
    1.49  
    1.50 -        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
    1.51 +
    1.52 +        /* cumulate markup */
    1.53 +
    1.54 +        private def cumulate[A](
    1.55 +          status: Boolean,
    1.56 +          range: Text.Range,
    1.57 +          info: A,
    1.58 +          elements: String => Boolean,
    1.59            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.60          {
    1.61            val former_range = revert(range)
    1.62            thy_load_commands match {
    1.63              case thy_load_command :: _ =>
    1.64                val file_name = node_name.node
    1.65 +              val markup_index = Command.Markup_Index(status, file_name)
    1.66                (for {
    1.67                  chunk <- thy_load_command.chunks.get(file_name).iterator
    1.68                  st = state.command_state(version, thy_load_command)
    1.69                  res = result(st)
    1.70 -                Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
    1.71 +                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
    1.72                    former_range.restrict(chunk.range), info, elements,
    1.73                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    1.74                  ).iterator
    1.75                } yield Text.Info(convert(r0), a)).toList
    1.76  
    1.77              case _ =>
    1.78 +              val markup_index = Command.Markup_Index(status, "")
    1.79                (for {
    1.80                  (command, command_start) <- node.command_range(former_range)
    1.81                  st = state.command_state(version, command)
    1.82                  res = result(st)
    1.83 -                Text.Info(r0, a) <- st.markup.cumulate[A](
    1.84 +                Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
    1.85                    (former_range - command_start).restrict(command.range), info, elements,
    1.86 -                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
    1.87 -                ).iterator
    1.88 +                  {
    1.89 +                    case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
    1.90 +                  }).iterator
    1.91                } yield Text.Info(convert(r0 + command_start), a)).toList
    1.92            }
    1.93          }
    1.94  
    1.95 -        def select_markup[A](range: Text.Range, elements: String => Boolean,
    1.96 +        private def select[A](status: Boolean, range: Text.Range, elements: String => Boolean,
    1.97            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
    1.98          {
    1.99            def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
   1.100 @@ -674,6 +695,22 @@
   1.101            for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
   1.102              yield Text.Info(r, x)
   1.103          }
   1.104 +
   1.105 +        def cumulate_status[A](range: Text.Range, info: A, elements: String => Boolean,
   1.106 +            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   1.107 +          cumulate(true, range, info, elements, result)
   1.108 +
   1.109 +        def select_status[A](range: Text.Range, elements: String => Boolean,
   1.110 +            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
   1.111 +          select(true, range, elements, result)
   1.112 +
   1.113 +        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
   1.114 +            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   1.115 +          cumulate(false, range, info, elements, result)
   1.116 +
   1.117 +        def select_markup[A](range: Text.Range, elements: String => Boolean,
   1.118 +            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
   1.119 +          select(false, range, elements, result)
   1.120        }
   1.121      }
   1.122    }