equal
deleted
inserted
replaced
110 Some((name, line, Text.Range(offset, end_offset))) |
110 Some((name, line, Text.Range(offset, end_offset))) |
111 case _ => None |
111 case _ => None |
112 } |
112 } |
113 } |
113 } |
114 |
114 |
115 object Identified |
|
116 { |
|
117 def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] = |
|
118 pos match { |
|
119 case Id(id) => |
|
120 val chunk_name = |
|
121 pos match { |
|
122 case File(name) => Symbol.Text_Chunk.File(name) |
|
123 case _ => Symbol.Text_Chunk.Default |
|
124 } |
|
125 Some((id, chunk_name)) |
|
126 case _ => None |
|
127 } |
|
128 } |
|
129 |
|
130 def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
115 def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
131 |
116 |
132 |
117 |
133 /* here: user output */ |
118 /* here: user output */ |
134 |
119 |