author | wenzelm |
Thu, 03 Apr 2014 14:54:17 +0200 | |
changeset 56387 | d92eb5c3960d |
parent 56385 | 76acce58aeab |
permissions | -rw-r--r-- |
53055 | 1 |
/* Title: Pure/Tools/sledgehammer_params.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Protocol for Sledgehammer parameters from ML (see also |
|
55200 | 5 |
HOL/Tools/Sledgehammer/sledgehammer_commands.ML). */ |
53055 | 6 |
|
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Sledgehammer_Params |
|
11 |
{ |
|
12 |
/* global event bus */ |
|
13 |
||
14 |
case object Provers |
|
15 |
val provers = new Event_Bus[Provers.type] |
|
16 |
||
17 |
||
18 |
/* per session result */ |
|
19 |
||
20 |
def get_provers(session: Session): String = |
|
21 |
session.protocol_handler("isabelle.Sledgehammer_Params$Handler") match { |
|
22 |
case Some(handler: Handler) => handler.get_provers |
|
23 |
case _ => "" |
|
24 |
} |
|
25 |
||
26 |
||
27 |
/* handler */ |
|
28 |
||
29 |
class Handler extends Session.Protocol_Handler |
|
30 |
{ |
|
31 |
private var _provers: String = "" |
|
32 |
private def update_provers(s: String) |
|
33 |
{ |
|
34 |
synchronized { _provers = s } |
|
35 |
provers.event(Provers) |
|
36 |
} |
|
37 |
def get_provers: String = synchronized { _provers } |
|
38 |
||
56387 | 39 |
private def sledgehammer_provers(prover: Prover, msg: Prover.Protocol_Output): Boolean = |
53055 | 40 |
{ |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
53055
diff
changeset
|
41 |
update_provers(msg.text) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
53055
diff
changeset
|
42 |
true |
53055 | 43 |
} |
44 |
||
45 |
val functions = |
|
46 |
Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _) |
|
47 |
} |
|
48 |
} |