99 def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
99 def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
100 |
100 |
101 |
101 |
102 /* here: user output */ |
102 /* here: user output */ |
103 |
103 |
|
104 def yxml_markup(pos: T, str: String): String = |
|
105 YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str)))) |
|
106 |
104 def here(pos: T): String = |
107 def here(pos: T): String = |
105 (Line.unapply(pos), File.unapply(pos)) match { |
108 yxml_markup(pos, |
106 case (Some(i), None) => " (line " + i.toString + ")" |
109 (Line.unapply(pos), File.unapply(pos)) match { |
107 case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")" |
110 case (Some(i), None) => " (line " + i.toString + ")" |
108 case (None, Some(name)) => " (file " + quote(name) + ")" |
111 case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")" |
109 case _ => "" |
112 case (None, Some(name)) => " (file " + quote(name) + ")" |
110 } |
113 case _ => "" |
|
114 }) |
111 |
115 |
112 def here_undelimited(pos: T): String = |
116 def here_undelimited(pos: T): String = |
113 (Line.unapply(pos), File.unapply(pos)) match { |
117 yxml_markup(pos, |
114 case (Some(i), None) => "line " + i.toString |
118 (Line.unapply(pos), File.unapply(pos)) match { |
115 case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name) |
119 case (Some(i), None) => "line " + i.toString |
116 case (None, Some(name)) => "file " + quote(name) |
120 case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name) |
117 case _ => "" |
121 case (None, Some(name)) => "file " + quote(name) |
118 } |
122 case _ => "" |
|
123 }) |
119 } |
124 } |