59 markup_root.filter(_.info match { |
59 markup_root.filter(_.info match { |
60 case RefInfo(_, _, _, _) => true |
60 case RefInfo(_, _, _, _) => true |
61 case _ => false }).flatten(_.flatten) |
61 case _ => false }).flatten(_.flatten) |
62 |
62 |
63 def ref_at(pos: Int): Option[MarkupNode] = |
63 def ref_at(pos: Int): Option[MarkupNode] = |
64 refs.find(t => t.start <= pos && t.stop > pos) |
64 refs.find(t => t.start <= pos && pos < t.stop) |
65 |
65 |
66 |
66 |
67 |
67 |
68 /* message dispatch */ |
68 /* message dispatch */ |
69 |
69 |
70 def + (message: XML.Tree): State = |
70 def + (message: XML.Tree): State = |
71 { |
71 { |
72 val changed: State = |
72 val changed: State = |
73 message match { |
73 message match { |
74 case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _) |
74 case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _) |
75 | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _) |
75 | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _) |
76 | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) => |
76 | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) => |
77 add_result(message) |
77 add_result(message) |
78 case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) => |
78 case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) => |
79 set_status(Command.Status.FAILED).add_result(message) |
79 set_status(Command.Status.FAILED).add_result(message) |
80 case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => |
80 case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => |
81 (this /: elems) ((st, e) => |
81 (this /: elems) ((st, e) => |
82 e match { |
82 e match { |
83 // command status |
83 // command status |
84 case XML.Elem(Markup.UNPROCESSED, _, _) => |
84 case XML.Elem(Markup.UNPROCESSED, _, _) => |
85 st.set_status(Command.Status.UNPROCESSED) |
85 st.set_status(Command.Status.UNPROCESSED) |
86 case XML.Elem(Markup.FINISHED, _, _) => |
86 case XML.Elem(Markup.FINISHED, _, _) => |
87 st.set_status(Command.Status.FINISHED) |
87 st.set_status(Command.Status.FINISHED) |
88 case XML.Elem(Markup.FAILED, _, _) => |
88 case XML.Elem(Markup.FAILED, _, _) => |
89 st.set_status(Command.Status.FAILED) |
89 st.set_status(Command.Status.FAILED) |
90 case XML.Elem(kind, attr, body) => |
90 case XML.Elem(kind, attr, body) => |
91 val (begin, end) = Position.offsets_of(attr) |
91 val (begin, end) = Position.offsets_of(attr) |
92 if (begin.isDefined && end.isDefined) { |
92 if (begin.isDefined && end.isDefined) { |
93 if (kind == Markup.ML_TYPING) { |
93 if (kind == Markup.ML_TYPING) { |
94 val info = body.first.asInstanceOf[XML.Text].content |
94 val info = body.first.asInstanceOf[XML.Text].content |
95 st.add_markup(command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))) |
95 st.add_markup(command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))) |
96 } |
96 } |
97 else if (kind == Markup.ML_REF) { |
97 else if (kind == Markup.ML_REF) { |
98 body match { |
98 body match { |
99 case List(XML.Elem(Markup.ML_DEF, attr, _)) => |
99 case List(XML.Elem(Markup.ML_DEF, attr, _)) => |
100 st.add_markup(command.markup_node( |
100 st.add_markup(command.markup_node( |
101 begin.get - 1, end.get - 1, |
101 begin.get - 1, end.get - 1, |
102 RefInfo( |
102 RefInfo( |
103 Position.file_of(attr), |
103 Position.file_of(attr), |
104 Position.line_of(attr), |
104 Position.line_of(attr), |
105 Position.id_of(attr), |
105 Position.id_of(attr), |
106 Position.offset_of(attr)))) |
106 Position.offset_of(attr)))) |
107 case _ => st |
107 case _ => st |
|
108 } |
|
109 } |
|
110 else { |
|
111 st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))) |
108 } |
112 } |
109 } |
113 } |
110 else { |
114 else st |
111 st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))) |
115 case _ => st |
112 } |
116 }) |
113 } |
117 case _ => |
114 else st |
118 System.err.println("ignored: " + message) |
115 case _ => st |
119 this |
116 }) |
120 } |
117 case _ => |
|
118 System.err.println("ignored: " + message) |
|
119 this |
|
120 } |
|
121 command.changed() |
121 command.changed() |
122 changed |
122 changed |
123 } |
123 } |
124 |
|
125 } |
124 } |