more operations (see also properties.ML);
authorwenzelm
Sun Oct 23 13:16:23 2016 +0200 (2016-10-23 ago)
changeset 6435815c90b744481
parent 64357 e10fa8afc96c
child 64359 27739e1d7978
more operations (see also properties.ML);
src/Pure/General/properties.scala
src/Pure/PIDE/markup.scala
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/General/properties.scala	Sun Oct 23 12:35:48 2016 +0200
     1.2 +++ b/src/Pure/General/properties.scala	Sun Oct 23 13:16:23 2016 +0200
     1.3 @@ -10,11 +10,30 @@
     1.4  
     1.5  object Properties
     1.6  {
     1.7 -  /* named entries */
     1.8 -
     1.9    type Entry = (java.lang.String, java.lang.String)
    1.10    type T = List[Entry]
    1.11  
    1.12 +  def defined(props: T, name: java.lang.String): java.lang.Boolean =
    1.13 +    props.exists({ case (x, _) => x == name })
    1.14 +
    1.15 +  def get(props: T, name: java.lang.String): Option[java.lang.String] =
    1.16 +    props.collectFirst({ case (x, y) if x == name => y })
    1.17 +
    1.18 +  def put(props: T, entry: Entry): T =
    1.19 +  {
    1.20 +    val (x, y) = entry
    1.21 +    def update(ps: T): T =
    1.22 +      ps match {
    1.23 +        case (p @ (x1, _)) :: rest =>
    1.24 +          if (x1 == x) (x1, y) :: rest else p :: update(rest)
    1.25 +        case Nil => Nil
    1.26 +      }
    1.27 +    if (defined(props, x)) update(props) else entry :: props
    1.28 +  }
    1.29 +
    1.30 +
    1.31 +  /* named entries */
    1.32 +
    1.33    class String(val name: java.lang.String)
    1.34    {
    1.35      def apply(value: java.lang.String): T = List((name, value))
     2.1 --- a/src/Pure/PIDE/markup.scala	Sun Oct 23 12:35:48 2016 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sun Oct 23 13:16:23 2016 +0200
     2.3 @@ -602,4 +602,8 @@
     2.4  {
     2.5    def markup(s: String): String =
     2.6      YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
     2.7 +
     2.8 +  def update_properties(more_props: Properties.T): Markup =
     2.9 +    if (more_props.isEmpty) this
    2.10 +    else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
    2.11  }
     3.1 --- a/src/Pure/PIDE/xml.scala	Sun Oct 23 12:35:48 2016 +0200
     3.2 +++ b/src/Pure/PIDE/xml.scala	Sun Oct 23 13:16:23 2016 +0200
     3.3 @@ -26,6 +26,9 @@
     3.4    case class Elem(markup: Markup, body: Body) extends Tree
     3.5    {
     3.6      def name: String = markup.name
     3.7 +    def update_attributes(more_attributes: Attributes): Elem =
     3.8 +      if (more_attributes.isEmpty) this
     3.9 +      else Elem(markup.update_properties(more_attributes), body)
    3.10    }
    3.11    case class Text(content: String) extends Tree
    3.12