36 /* content */ |
36 /* content */ |
37 |
37 |
38 override def toString = name |
38 override def toString = name |
39 |
39 |
40 val name = tokens.head.content |
40 val name = tokens.head.content |
41 val content:String = Token.string_from_tokens(tokens, starts) |
41 val content: String = Token.string_from_tokens(tokens, starts) |
42 |
42 |
43 def start(doc: ProofDocument) = doc.token_start(tokens.first) |
43 def start(doc: ProofDocument) = doc.token_start(tokens.first) |
44 def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length |
44 def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length |
45 |
45 |
46 /* command status */ |
46 /* command status */ |
79 |
79 |
80 |
80 |
81 /* markup */ |
81 /* markup */ |
82 |
82 |
83 val empty_root_node = |
83 val empty_root_node = |
84 new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, |
84 new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, |
85 id, content, RootInfo()) |
85 Nil, id, content, RootInfo()) |
86 |
86 |
87 var markup_root = empty_root_node |
87 var markup_root = empty_root_node |
88 |
88 |
89 def highlight_node: MarkupNode = { |
89 def highlight_node: MarkupNode = { |
90 import MarkupNode._ |
90 import MarkupNode._ |
94 }).head |
94 }).head |
95 } |
95 } |
96 |
96 |
97 def markup_node(begin: Int, end: Int, info: MarkupInfo) = |
97 def markup_node(begin: Int, end: Int, info: MarkupInfo) = |
98 new MarkupNode(this, begin, end, Nil, id, |
98 new MarkupNode(this, begin, end, Nil, id, |
99 if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??", |
99 if (end <= content.length && begin >= 0) content.substring(begin, end) |
100 info) |
100 else "wrong indices??", |
|
101 info) |
101 |
102 |
102 def type_at(pos: Int): String = { |
103 def type_at(pos: Int): String = { |
103 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 }) |
104 types.flatten(_.flatten). |
105 types.flatten(_.flatten). |
105 find(t => t.start <= pos && t.stop > pos). |
106 find(t => t.start <= pos && t.stop > pos). |
106 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 _ => "" })). |
107 getOrElse(null) |
108 getOrElse(null) |
108 } |
109 } |
109 |
110 |
110 def ref_at(pos: Int): Option[MarkupNode] = |
111 def ref_at(pos: Int): Option[MarkupNode] = |
111 markup_root.filter(_.info match {case RefInfo(_,_,_,_) => true case _ => false}). |
112 markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }). |
112 flatten(_.flatten). |
113 flatten(_.flatten). |
113 find(t => t.start <= pos && t.stop > pos) |
114 find(t => t.start <= pos && t.stop > pos) |
114 } |
115 } |