more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
authorwenzelm
Sat Apr 19 19:52:02 2014 +0200 (2014-04-19 ago)
changeset 566234675df68450e
parent 56622 891d1b8b64fb
child 56624 7eed0fee0241
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/etc/options
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Tools/sledgehammer_params.scala
src/Pure/build-jars
src/Tools/jEdit/src/sledgehammer_dockable.scala
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 19 19:03:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Apr 19 19:52:02 2014 +0200
     1.3 @@ -498,13 +498,4 @@
     1.4          in () end
     1.5      | NONE => error "Unknown proof context"))
     1.6  
     1.7 -val _ = Session.protocol_handler "isabelle.Sledgehammer_Params$Handler"
     1.8 -
     1.9 -val _ = Isabelle_Process.protocol_command "Sledgehammer.provers"
    1.10 -  (fn [] =>
    1.11 -    let
    1.12 -      val this_thy = @{theory}
    1.13 -      val provers = space_implode " " (#provers (default_params this_thy []))
    1.14 -    in Output.protocol_message Markup.sledgehammer_provers [provers] end)
    1.15 -
    1.16  end;
     2.1 --- a/src/HOL/Tools/etc/options	Sat Apr 19 19:03:32 2014 +0200
     2.2 +++ b/src/HOL/Tools/etc/options	Sat Apr 19 19:52:02 2014 +0200
     2.3 @@ -26,6 +26,9 @@
     2.4  
     2.5  section "Miscellaneous Tools"
     2.6  
     2.7 +public option sledgehammer_provers : string = "e spass remote_vampire"
     2.8 +  -- "ATPs for Sledgehammer (separated by blanks)"
     2.9 +
    2.10  public option sledgehammer_timeout : int = 30
    2.11    -- "ATPs will be interrupted after this time (in seconds)"
    2.12  
     3.1 --- a/src/Pure/PIDE/markup.ML	Sat Apr 19 19:03:32 2014 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Sat Apr 19 19:52:02 2014 +0200
     3.3 @@ -178,7 +178,6 @@
     3.4    val protocol_handler: string -> Properties.T
     3.5    val invoke_scala: string -> string -> Properties.T
     3.6    val cancel_scala: string -> Properties.T
     3.7 -  val sledgehammer_provers: Properties.T
     3.8    val ML_statistics: Properties.entry
     3.9    val task_statistics: Properties.entry
    3.10    val command_timing: Properties.entry
    3.11 @@ -568,8 +567,6 @@
    3.12  fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
    3.13  fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
    3.14  
    3.15 -val sledgehammer_provers = [(functionN, "sledgehammer_provers")];
    3.16 -
    3.17  val ML_statistics = (functionN, "ML_statistics");
    3.18  
    3.19  val task_statistics = (functionN, "task_statistics");
     4.1 --- a/src/Pure/PIDE/markup.scala	Sat Apr 19 19:03:32 2014 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 19 19:52:02 2014 +0200
     4.3 @@ -399,9 +399,6 @@
     4.4        }
     4.5    }
     4.6  
     4.7 -  val SLEDGEHAMMER_PROVERS = "sledgehammer_provers"
     4.8 -  val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS))
     4.9 -
    4.10    object ML_Statistics
    4.11    {
    4.12      def unapply(props: Properties.T): Option[Properties.T] =
     5.1 --- a/src/Pure/Tools/sledgehammer_params.scala	Sat Apr 19 19:03:32 2014 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,48 +0,0 @@
     5.4 -/*  Title:      Pure/Tools/sledgehammer_params.scala
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Protocol for Sledgehammer parameters from ML (see also
     5.8 -HOL/Tools/Sledgehammer/sledgehammer_commands.ML).  */
     5.9 -
    5.10 -package isabelle
    5.11 -
    5.12 -
    5.13 -object Sledgehammer_Params
    5.14 -{
    5.15 -  /* global event bus */
    5.16 -
    5.17 -  case object Provers
    5.18 -  val provers = new Event_Bus[Provers.type]
    5.19 -
    5.20 -
    5.21 -  /* per session result */
    5.22 -
    5.23 -  def get_provers(session: Session): String =
    5.24 -    session.protocol_handler("isabelle.Sledgehammer_Params$Handler") match {
    5.25 -      case Some(handler: Handler) => handler.get_provers
    5.26 -      case _ => ""
    5.27 -    }
    5.28 -
    5.29 -
    5.30 -  /* handler */
    5.31 -
    5.32 -  class Handler extends Session.Protocol_Handler
    5.33 -  {
    5.34 -    private var _provers: String = ""
    5.35 -    private def update_provers(s: String)
    5.36 -    {
    5.37 -      synchronized { _provers = s }
    5.38 -      provers.event(Provers)
    5.39 -    }
    5.40 -    def get_provers: String = synchronized { _provers }
    5.41 -
    5.42 -    private def sledgehammer_provers(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    5.43 -    {
    5.44 -      update_provers(msg.text)
    5.45 -      true
    5.46 -    }
    5.47 -
    5.48 -    val functions =
    5.49 -      Map(Markup.SLEDGEHAMMER_PROVERS -> sledgehammer_provers _)
    5.50 -  }
    5.51 -}
     6.1 --- a/src/Pure/build-jars	Sat Apr 19 19:03:32 2014 +0200
     6.2 +++ b/src/Pure/build-jars	Sat Apr 19 19:52:02 2014 +0200
     6.3 @@ -85,7 +85,6 @@
     6.4    Tools/main.scala
     6.5    Tools/ml_statistics.scala
     6.6    Tools/simplifier_trace.scala
     6.7 -  Tools/sledgehammer_params.scala
     6.8    Tools/task_statistics.scala
     6.9    library.scala
    6.10    package.scala
     7.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 19:03:32 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sat Apr 19 19:52:02 2014 +0200
     7.3 @@ -69,39 +69,13 @@
     7.4    })
     7.5  
     7.6  
     7.7 -  /* provers according to ML */
     7.8 -
     7.9 -  private def update_provers()
    7.10 -  {
    7.11 -    val new_provers = Sledgehammer_Params.get_provers(PIDE.session)
    7.12 -    if (new_provers != "" && provers.getText == "") {
    7.13 -      provers.setText(new_provers)
    7.14 -      if (provers.getCaret != null)
    7.15 -        provers.getCaret.setDot(0)
    7.16 -    }
    7.17 -  }
    7.18 -
    7.19 -  private def query_provers()
    7.20 -  {
    7.21 -    if (PIDE.session.is_ready)
    7.22 -      PIDE.session.protocol_command("Sledgehammer.provers")
    7.23 -  }
    7.24 -
    7.25 -
    7.26    /* main actor */
    7.27  
    7.28    private val main_actor = actor {
    7.29      loop {
    7.30        react {
    7.31          case _: Session.Global_Options =>
    7.32 -          Swing_Thread.later { handle_resize() }
    7.33 -          query_provers()
    7.34 -
    7.35 -        case Session.Ready =>
    7.36 -          query_provers()
    7.37 -
    7.38 -        case Sledgehammer_Params.Provers =>
    7.39 -          Swing_Thread.later { update_provers() }
    7.40 +          Swing_Thread.later { update_provers(); handle_resize() }
    7.41  
    7.42          case bad =>
    7.43            System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
    7.44 @@ -113,8 +87,6 @@
    7.45    {
    7.46      PIDE.session.phase_changed += main_actor
    7.47      PIDE.session.global_options += main_actor
    7.48 -    Sledgehammer_Params.provers += main_actor
    7.49 -    query_provers()
    7.50      handle_resize()
    7.51      sledgehammer.activate()
    7.52    }
    7.53 @@ -124,7 +96,6 @@
    7.54      sledgehammer.deactivate()
    7.55      PIDE.session.phase_changed -= main_actor
    7.56      PIDE.session.global_options -= main_actor
    7.57 -    Sledgehammer_Params.provers -= main_actor
    7.58      delay_resize.revoke()
    7.59    }
    7.60  
    7.61 @@ -132,6 +103,7 @@
    7.62    /* controls */
    7.63  
    7.64    private def clicked {
    7.65 +    PIDE.options.string("sledgehammer_provers") = provers.getText
    7.66      sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString))
    7.67    }
    7.68  
    7.69 @@ -151,6 +123,16 @@
    7.70      setColumns(30)
    7.71    }
    7.72  
    7.73 +  private def update_provers()
    7.74 +  {
    7.75 +    val new_provers = PIDE.options.string("sledgehammer_provers")
    7.76 +    if (new_provers != provers.getText) {
    7.77 +      provers.setText(new_provers)
    7.78 +      if (provers.getCaret != null)
    7.79 +        provers.getCaret.setDot(0)
    7.80 +    }
    7.81 +  }
    7.82 +
    7.83    private val isar_proofs = new CheckBox("Isar proofs") {
    7.84      tooltip = "Specify whether Isar proofs should be output in addition to metis line"
    7.85      selected = false