full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
authorwenzelm
Sat Jul 13 12:39:45 2013 +0200 (2013-07-13)
changeset 5264284eb792224a8
parent 52641 c56b6fa636e8
child 52643 34c29356930e
full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Jul 13 00:50:49 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Jul 13 12:39:45 2013 +0200
     1.3 @@ -130,7 +130,10 @@
     1.4        }
     1.5  
     1.6      def ++ (other: State): State =
     1.7 -      copy(results = results ++ other.results)  // FIXME merge more content!?
     1.8 +      copy(
     1.9 +        status = other.status ::: status,
    1.10 +        results = results ++ other.results,
    1.11 +        markup = markup ++ other.markup)
    1.12    }
    1.13  
    1.14  
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Jul 13 00:50:49 2013 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Jul 13 12:39:45 2013 +0200
     2.3 @@ -184,6 +184,10 @@
     2.4      }
     2.5    }
     2.6  
     2.7 +  def ++ (other: Markup_Tree): Markup_Tree =
     2.8 +    (this /: other.branches)({ case (tree, (range, entry)) =>
     2.9 +      ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
    2.10 +
    2.11    def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
    2.12    {
    2.13      def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =