1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 22:08:21 2013 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 22:15:45 2013 +0200
1.3 @@ -517,6 +517,15 @@
1.4 run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
1.5 no_fact_override (minimize_command override_params 1) state
1.6 in () end
1.7 - | NONE => error "Unknown proof context"));
1.8 + | NONE => error "Unknown proof context"))
1.9 +
1.10 +val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
1.11 +
1.12 +val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
1.13 + (fn [] =>
1.14 + let
1.15 + val this_ctxt = @{context}
1.16 + val provers = space_implode " " (#provers (default_params this_ctxt []))
1.17 + in Output.protocol_message Markup.sledgehammer_provers provers end)
1.18
1.19 end;
2.1 --- a/src/Pure/PIDE/markup.ML Sat Aug 17 22:08:21 2013 +0200
2.2 +++ b/src/Pure/PIDE/markup.ML Sat Aug 17 22:15:45 2013 +0200
2.3 @@ -150,6 +150,7 @@
2.4 val protocol_handler: string -> Properties.T
2.5 val invoke_scala: string -> string -> Properties.T
2.6 val cancel_scala: string -> Properties.T
2.7 + val sledgehammer_provers: Properties.T
2.8 val ML_statistics: Properties.entry
2.9 val task_statistics: Properties.entry
2.10 val command_timing: Properties.entry
2.11 @@ -480,6 +481,8 @@
2.12 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
2.13 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
2.14
2.15 +val sledgehammer_provers = [(functionN, "sledgehammer_provers")];
2.16 +
2.17 val ML_statistics = (functionN, "ML_statistics");
2.18
2.19 val task_statistics = (functionN, "task_statistics");
3.1 --- a/src/Pure/PIDE/markup.scala Sat Aug 17 22:08:21 2013 +0200
3.2 +++ b/src/Pure/PIDE/markup.scala Sat Aug 17 22:15:45 2013 +0200
3.3 @@ -353,6 +353,9 @@
3.4 }
3.5 }
3.6
3.7 + val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
3.8 + val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
3.9 +
3.10 object ML_Statistics
3.11 {
3.12 def unapply(props: Properties.T): Option[Properties.T] =
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Tools/sledgehammer_params.scala Sat Aug 17 22:15:45 2013 +0200
4.3 @@ -0,0 +1,52 @@
4.4 +/* Title: Pure/Tools/sledgehammer_params.scala
4.5 + Author: Makarius
4.6 +
4.7 +Protocol for Sledgehammer parameters from ML (see also
4.8 +HOL/Tools/Sledgehammer/sledgehammer_isar.ML). */
4.9 +
4.10 +package isabelle
4.11 +
4.12 +
4.13 +object Sledgehammer_Params
4.14 +{
4.15 + /* global event bus */
4.16 +
4.17 + case object Provers
4.18 + val provers = new Event_Bus[Provers.type]
4.19 +
4.20 +
4.21 + /* per session result */
4.22 +
4.23 + def get_provers(session: Session): String =
4.24 + session.protocol_handler("isabelle.Sledgehammer_Params$Handler") match {
4.25 + case Some(handler: Handler) => handler.get_provers
4.26 + case _ => ""
4.27 + }
4.28 +
4.29 +
4.30 + /* handler */
4.31 +
4.32 + class Handler extends Session.Protocol_Handler
4.33 + {
4.34 + private var _provers: String = ""
4.35 + private def update_provers(s: String)
4.36 + {
4.37 + synchronized { _provers = s }
4.38 + provers.event(Provers)
4.39 + }
4.40 + def get_provers: String = synchronized { _provers }
4.41 +
4.42 + private def sledgehammer_provers(
4.43 + prover: Session.Prover, output: Isabelle_Process.Output): Boolean =
4.44 + {
4.45 + output.body match {
4.46 + case Nil => update_provers(""); true
4.47 + case List(XML.Text(s)) => update_provers(s); true
4.48 + case _ => false
4.49 + }
4.50 + }
4.51 +
4.52 + val functions =
4.53 + Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _)
4.54 + }
4.55 +}
5.1 --- a/src/Pure/build-jars Sat Aug 17 22:08:21 2013 +0200
5.2 +++ b/src/Pure/build-jars Sat Aug 17 22:15:45 2013 +0200
5.3 @@ -77,6 +77,7 @@
5.4 Tools/keywords.scala
5.5 Tools/main.scala
5.6 Tools/ml_statistics.scala
5.7 + Tools/sledgehammer_params.scala
5.8 Tools/task_statistics.scala
5.9 library.scala
5.10 package.scala
6.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 22:08:21 2013 +0200
6.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 22:15:45 2013 +0200
6.3 @@ -71,6 +71,24 @@
6.4 })
6.5
6.6
6.7 + /* provers according to ML */
6.8 +
6.9 + private def update_provers()
6.10 + {
6.11 + val new_provers = Sledgehammer_Params.get_provers(PIDE.session)
6.12 + if (new_provers != "" && provers.getText == "") {
6.13 + provers.setText(new_provers)
6.14 + if (provers.getCaret != null)
6.15 + provers.getCaret.setDot(0)
6.16 + }
6.17 + }
6.18 +
6.19 + private def query_provers()
6.20 + {
6.21 + PIDE.session.protocol_command("Sledgehammer.provers")
6.22 + }
6.23 +
6.24 +
6.25 /* main actor */
6.26
6.27 private val main_actor = actor {
6.28 @@ -78,6 +96,10 @@
6.29 react {
6.30 case _: Session.Global_Options =>
6.31 Swing_Thread.later { handle_resize() }
6.32 + query_provers()
6.33 + case Session.Ready => query_provers()
6.34 + case Sledgehammer_Params.Provers =>
6.35 + Swing_Thread.later { update_provers() }
6.36 case bad =>
6.37 java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
6.38 }
6.39 @@ -88,7 +110,10 @@
6.40 {
6.41 Swing_Thread.require()
6.42
6.43 + PIDE.session.phase_changed += main_actor
6.44 PIDE.session.global_options += main_actor
6.45 + Sledgehammer_Params.provers += main_actor
6.46 + if (PIDE.session.is_ready) query_provers()
6.47 handle_resize()
6.48 sledgehammer.activate()
6.49 }
6.50 @@ -98,7 +123,9 @@
6.51 Swing_Thread.require()
6.52
6.53 sledgehammer.deactivate()
6.54 + PIDE.session.phase_changed -= main_actor
6.55 PIDE.session.global_options -= main_actor
6.56 + Sledgehammer_Params.provers -= main_actor
6.57 delay_resize.revoke()
6.58 }
6.59
6.60 @@ -120,7 +147,7 @@
6.61 super.processKeyEvent(evt)
6.62 }
6.63 setToolTipText(provers_label.tooltip)
6.64 - setColumns(20)
6.65 + setColumns(30)
6.66 }
6.67
6.68 private val timeout = new TextField("30.0", 5) {