equal
deleted
inserted
replaced
4 |
4 |
5 Prover commands with semantic state. |
5 Prover commands with semantic state. |
6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
|
10 |
|
11 import scala.actors.Actor, Actor._ |
|
12 import scala.collection.mutable |
|
13 |
9 |
14 |
10 |
15 object Command |
11 object Command |
16 { |
12 { |
17 /** accumulated results from prover **/ |
13 /** accumulated results from prover **/ |
38 |
34 |
39 /* message dispatch */ |
35 /* message dispatch */ |
40 |
36 |
41 def accumulate(message: XML.Tree): Command.State = |
37 def accumulate(message: XML.Tree): Command.State = |
42 message match { |
38 message match { |
43 case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit checks!? |
39 case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit body check!? |
44 copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status) |
40 copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status) |
45 |
41 |
46 case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
42 case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
47 (this /: msgs)((state, msg) => |
43 (this /: msgs)((state, msg) => |
48 msg match { |
44 msg match { |