# HG changeset patch # User wenzelm # Date 1376770545 -7200 # Node ID 0fe8a9972eda8f8d003cb20ce6a1c258110fe4db # Parent 8365d7fca3ded9363bbda4401812d01b35869b63 some protocol to determine provers according to ML; diff -r 8365d7fca3de -r 0fe8a9972eda src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 22:08:21 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 22:15:45 2013 +0200 @@ -517,6 +517,15 @@ run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1 no_fact_override (minimize_command override_params 1) state in () end - | NONE => error "Unknown proof context")); + | NONE => error "Unknown proof context")) + +val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler" + +val _ = Isabelle_Process.protocol_command "Sledgehammer.provers" + (fn [] => + let + val this_ctxt = @{context} + val provers = space_implode " " (#provers (default_params this_ctxt [])) + in Output.protocol_message Markup.sledgehammer_provers provers end) end; diff -r 8365d7fca3de -r 0fe8a9972eda src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Aug 17 22:08:21 2013 +0200 +++ b/src/Pure/PIDE/markup.ML Sat Aug 17 22:15:45 2013 +0200 @@ -150,6 +150,7 @@ val protocol_handler: string -> Properties.T val invoke_scala: string -> string -> Properties.T val cancel_scala: string -> Properties.T + val sledgehammer_provers: Properties.T val ML_statistics: Properties.entry val task_statistics: Properties.entry val command_timing: Properties.entry @@ -480,6 +481,8 @@ fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; +val sledgehammer_provers = [(functionN, "sledgehammer_provers")]; + val ML_statistics = (functionN, "ML_statistics"); val task_statistics = (functionN, "task_statistics"); diff -r 8365d7fca3de -r 0fe8a9972eda src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Aug 17 22:08:21 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Aug 17 22:15:45 2013 +0200 @@ -353,6 +353,9 @@ } } + val SLEDGEHAMMER_PROVERS = "sledgehammer_provers" + val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS)) + object ML_Statistics { def unapply(props: Properties.T): Option[Properties.T] = diff -r 8365d7fca3de -r 0fe8a9972eda src/Pure/Tools/sledgehammer_params.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/sledgehammer_params.scala Sat Aug 17 22:15:45 2013 +0200 @@ -0,0 +1,52 @@ +/* Title: Pure/Tools/sledgehammer_params.scala + Author: Makarius + +Protocol for Sledgehammer parameters from ML (see also +HOL/Tools/Sledgehammer/sledgehammer_isar.ML). */ + +package isabelle + + +object Sledgehammer_Params +{ + /* global event bus */ + + case object Provers + val provers = new Event_Bus[Provers.type] + + + /* per session result */ + + def get_provers(session: Session): String = + session.protocol_handler("isabelle.Sledgehammer_Params$Handler") match { + case Some(handler: Handler) => handler.get_provers + case _ => "" + } + + + /* handler */ + + class Handler extends Session.Protocol_Handler + { + private var _provers: String = "" + private def update_provers(s: String) + { + synchronized { _provers = s } + provers.event(Provers) + } + def get_provers: String = synchronized { _provers } + + private def sledgehammer_provers( + prover: Session.Prover, output: Isabelle_Process.Output): Boolean = + { + output.body match { + case Nil => update_provers(""); true + case List(XML.Text(s)) => update_provers(s); true + case _ => false + } + } + + val functions = + Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _) + } +} diff -r 8365d7fca3de -r 0fe8a9972eda src/Pure/build-jars --- a/src/Pure/build-jars Sat Aug 17 22:08:21 2013 +0200 +++ b/src/Pure/build-jars Sat Aug 17 22:15:45 2013 +0200 @@ -77,6 +77,7 @@ Tools/keywords.scala Tools/main.scala Tools/ml_statistics.scala + Tools/sledgehammer_params.scala Tools/task_statistics.scala library.scala package.scala diff -r 8365d7fca3de -r 0fe8a9972eda src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 22:08:21 2013 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 17 22:15:45 2013 +0200 @@ -71,6 +71,24 @@ }) + /* provers according to ML */ + + private def update_provers() + { + val new_provers = Sledgehammer_Params.get_provers(PIDE.session) + if (new_provers != "" && provers.getText == "") { + provers.setText(new_provers) + if (provers.getCaret != null) + provers.getCaret.setDot(0) + } + } + + private def query_provers() + { + PIDE.session.protocol_command("Sledgehammer.provers") + } + + /* main actor */ private val main_actor = actor { @@ -78,6 +96,10 @@ react { case _: Session.Global_Options => Swing_Thread.later { handle_resize() } + query_provers() + case Session.Ready => query_provers() + case Sledgehammer_Params.Provers => + Swing_Thread.later { update_provers() } case bad => java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad) } @@ -88,7 +110,10 @@ { Swing_Thread.require() + PIDE.session.phase_changed += main_actor PIDE.session.global_options += main_actor + Sledgehammer_Params.provers += main_actor + if (PIDE.session.is_ready) query_provers() handle_resize() sledgehammer.activate() } @@ -98,7 +123,9 @@ Swing_Thread.require() sledgehammer.deactivate() + PIDE.session.phase_changed -= main_actor PIDE.session.global_options -= main_actor + Sledgehammer_Params.provers -= main_actor delay_resize.revoke() } @@ -120,7 +147,7 @@ super.processKeyEvent(evt) } setToolTipText(provers_label.tooltip) - setColumns(20) + setColumns(30) } private val timeout = new TextField("30.0", 5) {