equal
deleted
inserted
replaced
79 } |
79 } |
80 } |
80 } |
81 |
81 |
82 def detect_program(s: String): Option[String] |
82 def detect_program(s: String): Option[String] |
83 |
83 |
84 override def output(message: Progress.Message): Unit = synchronized { |
84 override def output(msgs: Progress.Output): Unit = synchronized { |
85 val writeln_msg = if (message.kind == Progress.Kind.writeln) message.text else "" |
85 for (msg <- msgs) { |
86 detect_program(writeln_msg).map(Word.explode) match { |
86 val message = msg.message |
87 case Some(a :: bs) => |
87 val writeln_msg = if (message.kind == Progress.Kind.writeln) message.text else "" |
88 stop_program() |
88 detect_program(writeln_msg).map(Word.explode) match { |
89 start_program(a, Word.implode(bs)) |
89 case Some(a :: bs) => |
90 case _ => |
90 stop_program() |
91 if (_running_program.isEmpty) start_program(default_heading, default_title) |
91 start_program(a, Word.implode(bs)) |
92 if (do_output(message)) _running_program.get.output(message) |
92 case _ => |
|
93 if (_running_program.isEmpty) start_program(default_heading, default_title) |
|
94 if (do_output(message)) _running_program.get.output(message) |
|
95 } |
93 } |
96 } |
94 } |
97 } |
95 } |
98 } |