tuned signature;
authorwenzelm
Sun Mar 15 22:05:08 2015 +0100 (2015-03-15 ago)
changeset 5970910effab11669
parent 59708 bf6ca55aae13
child 59710 aed304412e43
tuned signature;
src/Pure/General/position.scala
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/General/position.scala	Sun Mar 15 21:57:10 2015 +0100
     1.2 +++ b/src/Pure/General/position.scala	Sun Mar 15 22:05:08 2015 +0100
     1.3 @@ -102,11 +102,8 @@
     1.4  
     1.5    /* here: user output */
     1.6  
     1.7 -  def yxml_markup(pos: T, str: String): String =
     1.8 -    YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str))))
     1.9 -
    1.10    def here(pos: T): String =
    1.11 -    yxml_markup(pos,
    1.12 +    Markup(Markup.POSITION, pos).markup(
    1.13        (Line.unapply(pos), File.unapply(pos)) match {
    1.14          case (Some(i), None) => " (line " + i.toString + ")"
    1.15          case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
    1.16 @@ -115,7 +112,7 @@
    1.17        })
    1.18  
    1.19    def here_undelimited(pos: T): String =
    1.20 -    yxml_markup(pos,
    1.21 +    Markup(Markup.POSITION, pos).markup(
    1.22        (Line.unapply(pos), File.unapply(pos)) match {
    1.23          case (Some(i), None) => "line " + i.toString
    1.24          case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
     2.1 --- a/src/Pure/PIDE/markup.scala	Sun Mar 15 21:57:10 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 15 22:05:08 2015 +0100
     2.3 @@ -504,4 +504,7 @@
     2.4  
     2.5  
     2.6  sealed case class Markup(name: String, properties: Properties.T)
     2.7 -
     2.8 +{
     2.9 +  def markup(s: String): String =
    2.10 +    YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
    2.11 +}