author | wenzelm |
Sat, 04 Mar 2023 12:43:35 +0100 | |
changeset 77502 | 2e2b2bd6b2d2 |
parent 77499 | 8fc94efa954a |
child 77503 | daf632e9ce7e |
permissions | -rw-r--r-- |
61276 | 1 |
/* Title: Pure/System/progress.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Progress context for system processes. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
73897 | 10 |
import java.util.{Map => JMap} |
64201 | 11 |
import java.io.{File => JFile} |
12 |
||
13 |
||
75393 | 14 |
object Progress { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
15 |
object Kind extends Enumeration { val writeln, warning, error_message = Value } |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
16 |
sealed case class Message(kind: Kind.Value, text: String) { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
17 |
def output_text: String = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
18 |
kind match { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
19 |
case Kind.writeln => Output.writeln_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
20 |
case Kind.warning => Output.warning_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
21 |
case Kind.error_message => Output.error_message_text(text) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
22 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
23 |
|
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
24 |
override def toString: String = output_text |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
25 |
} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
26 |
|
75393 | 27 |
sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None) { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
28 |
def message: Message = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
29 |
Message(Kind.writeln, print_session + print_theory + print_percentage) |
68987 | 30 |
|
31 |
def print_session: String = if (session == "") "" else session + ": " |
|
32 |
def print_theory: String = "theory " + theory |
|
33 |
def print_percentage: String = |
|
34 |
percentage match { case None => "" case Some(p) => " " + p + "%" } |
|
68957 | 35 |
} |
68410
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
36 |
} |
4e27f5c361d2
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm
parents:
68330
diff
changeset
|
37 |
|
75393 | 38 |
class Progress { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
39 |
def echo(message: Progress.Message) = {} |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
40 |
|
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
41 |
def echo(msg: String): Unit = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
42 |
echo(Progress.Message(Progress.Kind.writeln, msg)) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
43 |
def echo_warning(msg: String): Unit = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
44 |
echo(Progress.Message(Progress.Kind.warning, msg)) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
45 |
def echo_error_message(msg: String): Unit = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
46 |
echo(Progress.Message(Progress.Kind.error_message, msg)) |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
47 |
|
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
48 |
def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg) |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
49 |
|
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
50 |
def verbose: Boolean = false |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
51 |
def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message) |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
52 |
|
73340 | 53 |
def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {} |
64909 | 54 |
|
76593
badb5264f7b9
clarified signature: just one level of arguments to avoid type-inference problems;
wenzelm
parents:
76592
diff
changeset
|
55 |
def timeit[A](body: => A, message: Exn.Result[A] => String = null, enabled: Boolean = true): A = |
badb5264f7b9
clarified signature: just one level of arguments to avoid type-inference problems;
wenzelm
parents:
76592
diff
changeset
|
56 |
Timing.timeit(body, message = message, enabled = enabled, output = echo) |
65921 | 57 |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
58 |
@volatile protected var is_stopped = false |
73367 | 59 |
def stop(): Unit = { is_stopped = true } |
75393 | 60 |
def stopped: Boolean = { |
73367 | 61 |
if (Thread.interrupted()) is_stopped = true |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
62 |
is_stopped |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
63 |
} |
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
64 |
|
73367 | 65 |
def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e } |
73340 | 66 |
def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt() |
61276 | 67 |
override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
64201 | 68 |
|
69 |
def bash(script: String, |
|
70 |
cwd: JFile = null, |
|
73897 | 71 |
env: JMap[String, String] = Isabelle_System.settings(), |
64201 | 72 |
redirect: Boolean = false, |
65930 | 73 |
echo: Boolean = false, |
72599 | 74 |
watchdog: Time = Time.zero, |
75393 | 75 |
strict: Boolean = true |
76 |
): Process_Result = { |
|
72599 | 77 |
val result = |
78 |
Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
|
79 |
progress_stdout = echo_if(echo, _), |
|
80 |
progress_stderr = echo_if(echo, _), |
|
81 |
watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)), |
|
82 |
strict = strict) |
|
83 |
if (strict && stopped) throw Exn.Interrupt() else result |
|
64201 | 84 |
} |
61276 | 85 |
} |
86 |
||
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
87 |
class Console_Progress(override val verbose: Boolean = false, stderr: Boolean = false) |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
88 |
extends Progress { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
89 |
override def echo(message: Progress.Message): Unit = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
90 |
Output.output(message.output_text, stdout = !stderr, include_empty = true) |
61276 | 91 |
} |
65888 | 92 |
|
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
93 |
class File_Progress(path: Path, override val verbose: Boolean = false) extends Progress { |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
94 |
override def echo(message: Progress.Message): Unit = |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
95 |
File.append(path, message.output_text + "\n") |
65888 | 96 |
|
97 |
override def toString: String = path.toString |
|
98 |
} |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
99 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
100 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
101 |
/* structured program progress */ |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
102 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
103 |
object Program_Progress { |
77174 | 104 |
class Program private[Program_Progress](heading: String, title: String) { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
105 |
private val output_buffer = new StringBuffer(256) // synchronized |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
106 |
|
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
107 |
def echo(message: Progress.Message): Unit = synchronized { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
108 |
if (output_buffer.length() > 0) output_buffer.append('\n') |
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
109 |
output_buffer.append(message.output_text) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
110 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
111 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
112 |
val start_time: Time = Time.now() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
113 |
private var stop_time: Option[Time] = None |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
114 |
def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) } |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
115 |
|
77174 | 116 |
def output(): (Command.Results, XML.Body) = synchronized { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
117 |
val output_text = output_buffer.toString |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
118 |
val elapsed_time = stop_time.map(t => t - start_time) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
119 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
120 |
val message_prefix = heading + " " |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
121 |
val message_suffix = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
122 |
elapsed_time match { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
123 |
case None => " ..." |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
124 |
case Some(t) => " ... (" + t.message + " elapsed time)" |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
125 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
126 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
127 |
val (results, message) = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
128 |
if (output_text.isEmpty) { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
129 |
(Command.Results.empty, XML.string(message_prefix + title + message_suffix)) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
130 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
131 |
else { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
132 |
val i = Document_ID.make() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
133 |
val results = Command.Results.make(List(i -> Protocol.writeln_message(output_text))) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
134 |
val message = |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
135 |
XML.string(message_prefix) ::: |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
136 |
List(XML.Elem(Markup(Markup.WRITELN, Markup.Serial(i)), XML.string(title))) ::: |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
137 |
XML.string(message_suffix) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
138 |
(results, message) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
139 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
140 |
|
76997 | 141 |
(results, List(XML.elem(Markup.TRACING_MESSAGE, message))) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
142 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
143 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
144 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
145 |
|
77174 | 146 |
abstract class Program_Progress( |
147 |
default_heading: String = "Running", |
|
77499
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
148 |
default_title: String = "program", |
8fc94efa954a
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
wenzelm
parents:
77498
diff
changeset
|
149 |
override val verbose: Boolean = false |
77174 | 150 |
) extends Progress { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
151 |
private var _finished_programs: List[Program_Progress.Program] = Nil |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
152 |
private var _running_program: Option[Program_Progress.Program] = None |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
153 |
|
77174 | 154 |
def output(): (Command.Results, XML.Body) = synchronized { |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
155 |
val programs = (_running_program.toList ::: _finished_programs).reverse |
77174 | 156 |
val programs_output = programs.map(_.output()) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
157 |
val results = Command.Results.merge(programs_output.map(_._1)) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
158 |
val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
159 |
(results, body) |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
160 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
161 |
|
77174 | 162 |
private def start_program(heading: String, title: String): Unit = synchronized { |
163 |
_running_program = Some(new Program_Progress.Program(heading, title)) |
|
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
164 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
165 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
166 |
def stop_program(): Unit = synchronized { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
167 |
_running_program match { |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
168 |
case Some(program) => |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
169 |
program.stop_now() |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
170 |
_finished_programs ::= program |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
171 |
_running_program = None |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
172 |
case None => |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
173 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
174 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
175 |
|
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
176 |
def detect_program(s: String): Option[String] |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
177 |
|
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
178 |
override def echo(message: Progress.Message): Unit = synchronized { |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
179 |
val writeln_msg = if (message.kind == Progress.Kind.writeln) message.text else "" |
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
180 |
detect_program(writeln_msg).map(Word.explode) match { |
77174 | 181 |
case Some(a :: bs) => |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
182 |
stop_program() |
77174 | 183 |
start_program(a, Word.implode(bs)) |
184 |
case _ => |
|
185 |
if (_running_program.isEmpty) start_program(default_heading, default_title) |
|
77502
2e2b2bd6b2d2
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
wenzelm
parents:
77499
diff
changeset
|
186 |
_running_program.get.echo(message) |
76994
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
187 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
188 |
} |
7c23db6b857b
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
wenzelm
parents:
76593
diff
changeset
|
189 |
} |