# HG changeset patch
# User wenzelm
# Date 1426453508 -3600
# Node ID 10effab1166988a9b260abc2d8b4a1602e8f2785
# Parent  bf6ca55aae13c9248b5f9cd76bbd352dbd6129b2
tuned signature;

diff -r bf6ca55aae13 -r 10effab11669 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sun Mar 15 21:57:10 2015 +0100
+++ b/src/Pure/General/position.scala	Sun Mar 15 22:05:08 2015 +0100
@@ -102,11 +102,8 @@
 
   /* here: user output */
 
-  def yxml_markup(pos: T, str: String): String =
-    YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str))))
-
   def here(pos: T): String =
-    yxml_markup(pos,
+    Markup(Markup.POSITION, pos).markup(
       (Line.unapply(pos), File.unapply(pos)) match {
         case (Some(i), None) => " (line " + i.toString + ")"
         case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
@@ -115,7 +112,7 @@
       })
 
   def here_undelimited(pos: T): String =
-    yxml_markup(pos,
+    Markup(Markup.POSITION, pos).markup(
       (Line.unapply(pos), File.unapply(pos)) match {
         case (Some(i), None) => "line " + i.toString
         case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
diff -r bf6ca55aae13 -r 10effab11669 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Mar 15 21:57:10 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Mar 15 22:05:08 2015 +0100
@@ -504,4 +504,7 @@
 
 
 sealed case class Markup(name: String, properties: Properties.T)
-
+{
+  def markup(s: String): String =
+    YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
+}