equal
deleted
inserted
replaced
102 |
102 |
103 def type_at(pos: Int): String = { |
103 def type_at(pos: Int): String = { |
104 val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false }) |
104 val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false }) |
105 types.flatten(_.flatten). |
105 types.flatten(_.flatten). |
106 find(t => t.start <= pos && t.stop > pos). |
106 find(t => t.start <= pos && t.stop > pos). |
107 map(t => "\"" + t.content + "\" : " + (t.info match { case TypeInfo(i) => i case _ => "" })). |
107 map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })). |
108 getOrElse(null) |
108 getOrElse(null) |
109 } |
109 } |
110 |
110 |
111 def ref_at(pos: Int): Option[MarkupNode] = |
111 def ref_at(pos: Int): Option[MarkupNode] = |
112 markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }). |
112 markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }). |