equal
deleted
inserted
replaced
32 |
32 |
33 /* protocol handler */ |
33 /* protocol handler */ |
34 |
34 |
35 class Handler extends Session.Protocol_Handler |
35 class Handler extends Session.Protocol_Handler |
36 { |
36 { |
|
37 private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
|
38 { |
|
39 msg.properties match { |
|
40 case Markup.Debugger_Output(name, serial) => |
|
41 // FIXME |
|
42 Output.writeln("debugger_output " + name + " " + serial + "\n" + msg.text) |
|
43 true |
|
44 case _ => false |
|
45 } |
|
46 } |
|
47 |
37 override def stop(prover: Prover) |
48 override def stop(prover: Prover) |
38 { |
49 { |
39 manager.shutdown() |
50 manager.shutdown() |
40 } |
51 } |
41 |
52 |
42 val functions = Map.empty[String, (Prover, Prover.Protocol_Output) => Boolean] // FIXME |
53 val functions = |
|
54 Map(Markup.DEBUGGER_OUTPUT -> debugger_output _) |
43 } |
55 } |
44 |
56 |
45 |
57 |
46 /* protocol commands */ |
58 /* protocol commands */ |
47 |
59 |