author | wenzelm |
Wed, 11 Oct 2023 10:46:50 +0200 | |
changeset 78753 | f40b59292288 |
parent 75440 | 39011d0d2128 |
permissions | -rw-r--r-- |
59720 | 1 |
/* Title: Pure/Tools/print_operation.scala |
56864 | 2 |
Author: Makarius |
3 |
||
4 |
Print operations as asynchronous query. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
75393 | 10 |
object Print_Operation { |
72215 | 11 |
def get(session: Session): List[(String, String)] = |
12 |
session.get_protocol_handler(classOf[Handler]) match { |
|
13 |
case Some(h) => h.get |
|
56864 | 14 |
case _ => Nil |
15 |
} |
|
16 |
||
17 |
||
18 |
/* protocol handler */ |
|
19 |
||
75393 | 20 |
class Handler extends Session.Protocol_Handler { |
61590 | 21 |
private val print_operations = Synchronized[List[(String, String)]](Nil) |
56864 | 22 |
|
72215 | 23 |
def get: List[(String, String)] = print_operations.value |
24 |
||
65220 | 25 |
override def init(session: Session): Unit = |
26 |
session.protocol_command(Markup.PRINT_OPERATIONS) |
|
27 |
||
75393 | 28 |
private def put(msg: Prover.Protocol_Output): Boolean = { |
29 |
val ops = { |
|
56864 | 30 |
import XML.Decode._ |
65344
b99283eed13c
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65220
diff
changeset
|
31 |
list(pair(string, string))(Symbol.decode_yxml(msg.text)) |
56864 | 32 |
} |
33 |
print_operations.change(_ => ops) |
|
34 |
true |
|
35 |
} |
|
36 |
||
75440 | 37 |
override val functions: Session.Protocol_Functions = |
38 |
List(Markup.PRINT_OPERATIONS -> put) |
|
56864 | 39 |
} |
40 |
} |