|
1 /* Title: Pure/System/program_progress.scala |
|
2 Author: Makarius |
|
3 |
|
4 Structured program progress. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Program_Progress { |
|
11 class Program private[Program_Progress](heading: String, title: String) { |
|
12 private val output_buffer = new StringBuffer(256) // synchronized |
|
13 |
|
14 def output(message: Progress.Message): Unit = synchronized { |
|
15 if (output_buffer.length() > 0) output_buffer.append('\n') |
|
16 output_buffer.append(message.output_text) |
|
17 } |
|
18 |
|
19 val start_time: Time = Time.now() |
|
20 private var stop_time: Option[Time] = None |
|
21 def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) } |
|
22 |
|
23 def output(): (Command.Results, XML.Body) = synchronized { |
|
24 val output_text = output_buffer.toString |
|
25 val elapsed_time = stop_time.map(t => t - start_time) |
|
26 |
|
27 val message_prefix = heading + " " |
|
28 val message_suffix = |
|
29 elapsed_time match { |
|
30 case None => " ..." |
|
31 case Some(t) => " ... (" + t.message + " elapsed time)" |
|
32 } |
|
33 |
|
34 val (results, message) = |
|
35 if (output_text.isEmpty) { |
|
36 (Command.Results.empty, XML.string(message_prefix + title + message_suffix)) |
|
37 } |
|
38 else { |
|
39 val i = Document_ID.make() |
|
40 val results = Command.Results.make(List(i -> Protocol.writeln_message(output_text))) |
|
41 val message = |
|
42 XML.string(message_prefix) ::: |
|
43 List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) ::: |
|
44 XML.string(message_suffix) |
|
45 (results, message) |
|
46 } |
|
47 |
|
48 (results, List(XML.elem(Markup.TRACING_MESSAGE, message))) |
|
49 } |
|
50 } |
|
51 } |
|
52 |
|
53 abstract class Program_Progress( |
|
54 default_heading: String = "Running", |
|
55 default_title: String = "program", |
|
56 override val verbose: Boolean = false |
|
57 ) extends Progress { |
|
58 private var _finished_programs: List[Program_Progress.Program] = Nil |
|
59 private var _running_program: Option[Program_Progress.Program] = None |
|
60 |
|
61 def output(): (Command.Results, XML.Body) = synchronized { |
|
62 val programs = (_running_program.toList ::: _finished_programs).reverse |
|
63 val programs_output = programs.map(_.output()) |
|
64 val results = Command.Results.merge(programs_output.map(_._1)) |
|
65 val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten |
|
66 (results, body) |
|
67 } |
|
68 |
|
69 private def start_program(heading: String, title: String): Unit = synchronized { |
|
70 _running_program = Some(new Program_Progress.Program(heading, title)) |
|
71 } |
|
72 |
|
73 def stop_program(): Unit = synchronized { |
|
74 _running_program match { |
|
75 case Some(program) => |
|
76 program.stop_now() |
|
77 _finished_programs ::= program |
|
78 _running_program = None |
|
79 case None => |
|
80 } |
|
81 } |
|
82 |
|
83 def detect_program(s: String): Option[String] |
|
84 |
|
85 override def output(message: Progress.Message): Unit = synchronized { |
|
86 val writeln_msg = if (message.kind == Progress.Kind.writeln) message.text else "" |
|
87 detect_program(writeln_msg).map(Word.explode) match { |
|
88 case Some(a :: bs) => |
|
89 stop_program() |
|
90 start_program(a, Word.implode(bs)) |
|
91 case _ => |
|
92 if (_running_program.isEmpty) start_program(default_heading, default_title) |
|
93 if (do_output(message)) _running_program.get.output(message) |
|
94 } |
|
95 } |
|
96 } |