equal
deleted
inserted
replaced
116 /* information associated with text range */ |
116 /* information associated with text range */ |
117 |
117 |
118 sealed case class Info[A](val range: Text.Range, val info: A) |
118 sealed case class Info[A](val range: Text.Range, val info: A) |
119 { |
119 { |
120 def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) |
120 def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) |
121 def try_restrict(r: Text.Range): Option[Info[A]] = |
121 def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info)) |
122 try { Some(Info(range.restrict(r), info)) } |
|
123 catch { case ERROR(_) => None } |
|
124 } |
122 } |
125 |
123 |
126 type Markup = Info[XML.Elem] |
124 type Markup = Info[XML.Elem] |
127 |
125 |
128 |
126 |