equal
deleted
inserted
replaced
|
1 /* Title: Pure/Tools/sledgehammer_params.scala |
|
2 Author: Makarius |
|
3 |
|
4 Protocol for Sledgehammer parameters from ML (see also |
|
5 HOL/Tools/Sledgehammer/sledgehammer_isar.ML). */ |
|
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 |
|
39 private def sledgehammer_provers( |
|
40 prover: Session.Prover, output: Isabelle_Process.Output): Boolean = |
|
41 { |
|
42 output.body match { |
|
43 case Nil => update_provers(""); true |
|
44 case List(XML.Text(s)) => update_provers(s); true |
|
45 case _ => false |
|
46 } |
|
47 } |
|
48 |
|
49 val functions = |
|
50 Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _) |
|
51 } |
|
52 } |