--- a/src/HOL/Tools/Nitpick/kodkod.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Fri Aug 28 12:04:53 2020 +0100
@@ -133,11 +133,19 @@
context.result()
}
+
+ /** protocol handler **/
+
def warmup(): String =
execute(
"solver: \"MiniSat\"\n" +
File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
+ class Handler extends Session.Protocol_Handler
+ {
+ override def init(session: Session): Unit = warmup()
+ }
+
/** scala function **/
--- a/src/HOL/Tools/etc/settings Fri Aug 28 12:04:36 2020 +0100
+++ b/src/HOL/Tools/etc/settings Fri Aug 28 12:04:53 2020 +0100
@@ -1,3 +1,4 @@
# -*- shell-script -*- :mode=shellscript:
+isabelle_scala_service 'isabelle.nitpick.Kodkod$Handler'
isabelle_scala_service 'isabelle.nitpick.Scala_Functions'
--- a/src/Pure/ML/ml_statistics.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala Fri Aug 28 12:04:53 2020 +0100
@@ -85,9 +85,9 @@
private var session: Session = null
private var monitoring: Future[Unit] = Future.value(())
- override def init(init_session: Session): Unit = synchronized
+ override def init(session: Session): Unit = synchronized
{
- session = init_session
+ this.session = session
}
override def exit(): Unit = synchronized
@@ -117,7 +117,7 @@
}
}
- val functions = List(Markup.ML_Statistics.name -> ml_statistics)
+ override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
}
--- a/src/Pure/PIDE/protocol.ML Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML Fri Aug 28 12:04:53 2020 +0100
@@ -13,7 +13,9 @@
val _ =
Isabelle_Process.protocol_command "Prover.stop"
- (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc));
+ (fn rc :: msgs =>
+ (List.app Output.system_message msgs;
+ raise Isabelle_Process.STOP (Value.parse_int rc)));
val _ =
Isabelle_Process.protocol_command "Prover.options"
--- a/src/Pure/PIDE/protocol_handlers.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala Fri Aug 28 12:04:53 2020 +0100
@@ -9,9 +9,8 @@
object Protocol_Handlers
{
- private def bad_handler(exn: Throwable, name: String): Unit =
- Output.error_message(
- "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+ private def err_handler(exn: Throwable, name: String): Nothing =
+ error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
sealed case class State(
session: Session,
@@ -32,18 +31,18 @@
copy(handlers = handlers + (name -> handler), functions = functions ++ handler.functions)
}
}
- catch { case exn: Throwable => bad_handler(exn, name); this }
+ catch { case exn: Throwable => err_handler(exn, name) }
}
def init(name: String): State =
{
- val new_handler =
+ val handler =
try {
- Some(Class.forName(name).getDeclaredConstructor().newInstance()
- .asInstanceOf[Session.Protocol_Handler])
+ Class.forName(name).getDeclaredConstructor().newInstance()
+ .asInstanceOf[Session.Protocol_Handler]
}
- catch { case exn: Throwable => bad_handler(exn, name); None }
- new_handler match { case Some(handler) => init(handler) case None => this }
+ catch { case exn: Throwable => err_handler(exn, name) }
+ init(handler)
}
def invoke(msg: Prover.Protocol_Output): Boolean =
@@ -74,6 +73,10 @@
{
private val state = Synchronized(Protocol_Handlers.State(session))
+ def prover_options(options: Options): Options =
+ (options /: state.value.handlers)(
+ { case (opts, (_, handler)) => handler.prover_options(opts) })
+
def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
def init(name: String): Unit = state.change(_.init(name))
--- a/src/Pure/PIDE/session.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/PIDE/session.scala Fri Aug 28 12:04:53 2020 +0100
@@ -117,7 +117,8 @@
{
def init(session: Session): Unit = {}
def exit(): Unit = {}
- val functions: List[(String, Protocol_Function)]
+ def functions: List[(String, Protocol_Function)] = Nil
+ def prover_options(options: Options): Options = options
}
}
@@ -353,22 +354,25 @@
}
- /* file formats */
+ /* file formats and protocol handlers */
- lazy val file_formats: File_Format.Session =
+ private lazy val file_formats: File_Format.Session =
File_Format.registry.start_session(session)
-
- /* protocol handlers */
-
private val protocol_handlers = Protocol_Handlers.init(session)
- def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
- protocol_handlers.get(name)
+ def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] =
+ protocol_handlers.get(c.getName) match {
+ case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C])
+ case _ => None
+ }
def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
protocol_handlers.init(handler)
+ def prover_options(options: Options): Options =
+ protocol_handlers.prover_options(file_formats.prover_options(options))
+
/* debugger */
@@ -540,14 +544,25 @@
change_command(_.accumulate(state_id, output.message, xml_cache))
case _ if output.is_init =>
- prover.get.options(file_formats.prover_options(session_options))
- prover.get.init_session(resources)
+ val init_ok =
+ try {
+ Isabelle_System.make_services(classOf[Session.Protocol_Handler])
+ .foreach(init_protocol_handler)
+ true
+ }
+ catch {
+ case exn: Throwable =>
+ prover.get.protocol_command("Prover.stop", "1", Exn.message(exn))
+ false
+ }
- Isabelle_System.make_services(classOf[Session.Protocol_Handler])
- .foreach(init_protocol_handler)
+ if (init_ok) {
+ prover.get.options(prover_options(session_options))
+ prover.get.init_session(resources)
- phase = Session.Ready
- debugger.ready()
+ phase = Session.Ready
+ debugger.ready()
+ }
case Markup.Process_Result(result) if output.is_exit =>
if (prover.defined) protocol_handlers.exit()
@@ -622,7 +637,7 @@
case Update_Options(options) =>
if (prover.defined && is_ready) {
- prover.get.options(file_formats.prover_options(options))
+ prover.get.options(prover_options(options))
handle_raw_edits()
}
global_options.post(Session.Global_Options(options))
--- a/src/Pure/System/isabelle_system.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Aug 28 12:04:53 2020 +0100
@@ -64,18 +64,8 @@
}
def make_services[C](c: Class[C]): List[C] =
- {
- @tailrec def is_subclass(c1: Class[_]): Boolean =
- {
- c1 == c ||
- {
- val c2 = c1.getSuperclass
- c2 != null && is_subclass(c2)
- }
- }
- for { c1 <- services() if is_subclass(c1) }
+ for { c1 <- services() if Library.is_subclass(c1, c) }
yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
- }
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
{
--- a/src/Pure/System/scala.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/System/scala.scala Fri Aug 28 12:04:53 2020 +0100
@@ -160,8 +160,8 @@
private var session: Session = null
private var futures = Map.empty[String, Future[Unit]]
- override def init(init_session: Session): Unit =
- synchronized { session = init_session }
+ override def init(session: Session): Unit =
+ synchronized { this.session = session }
override def exit(): Unit = synchronized
{
@@ -211,7 +211,7 @@
}
}
- val functions =
+ override val functions =
List(
Markup.Invoke_Scala.name -> invoke_scala,
Markup.Cancel_Scala.name -> cancel_scala)
--- a/src/Pure/Tools/build.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/Tools/build.scala Fri Aug 28 12:04:53 2020 +0100
@@ -308,7 +308,7 @@
if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
} yield props1.filter(p => Markup.command_timing_properties(p._1))
- val functions =
+ override val functions =
List(
Markup.Build_Session_Finished.name -> build_session_finished,
Markup.Loading_Theory.name -> loading_theory,
--- a/src/Pure/Tools/debugger.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/Tools/debugger.scala Fri Aug 28 12:04:53 2020 +0100
@@ -141,7 +141,7 @@
}
}
- val functions =
+ override val functions =
List(
Markup.DEBUGGER_STATE -> debugger_state,
Markup.DEBUGGER_OUTPUT -> debugger_output)
--- a/src/Pure/Tools/print_operation.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/Tools/print_operation.scala Fri Aug 28 12:04:53 2020 +0100
@@ -9,9 +9,9 @@
object Print_Operation
{
- def print_operations(session: Session): List[(String, String)] =
- session.get_protocol_handler(classOf[Handler].getName) match {
- case Some(handler: Handler) => handler.get
+ def get(session: Session): List[(String, String)] =
+ session.get_protocol_handler(classOf[Handler]) match {
+ case Some(h) => h.get
case _ => Nil
}
@@ -22,11 +22,11 @@
{
private val print_operations = Synchronized[List[(String, String)]](Nil)
+ def get: List[(String, String)] = print_operations.value
+
override def init(session: Session): Unit =
session.protocol_command(Markup.PRINT_OPERATIONS)
- def get: List[(String, String)] = print_operations.value
-
private def put(msg: Prover.Protocol_Output): Boolean =
{
val ops =
@@ -38,6 +38,6 @@
true
}
- val functions = List(Markup.PRINT_OPERATIONS -> put)
+ override val functions = List(Markup.PRINT_OPERATIONS -> put)
}
}
--- a/src/Pure/Tools/simplifier_trace.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Fri Aug 28 12:04:53 2020 +0100
@@ -326,6 +326,6 @@
false
}
- val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel)
+ override val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel)
}
}
--- a/src/Pure/library.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Pure/library.scala Fri Aug 28 12:04:53 2020 +0100
@@ -276,4 +276,20 @@
def proper_list[A](list: List[A]): Option[List[A]] =
if (list == null || list.isEmpty) None else Some(list)
+
+
+ /* reflection */
+
+ def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
+ {
+ @tailrec def subclass(c: Class[_]): Boolean =
+ {
+ c == b ||
+ {
+ val d = c.getSuperclass
+ d != null && subclass(d)
+ }
+ }
+ subclass(a)
+ }
}
--- a/src/Tools/jEdit/src/query_dockable.scala Fri Aug 28 12:04:36 2020 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Fri Aug 28 12:04:53 2020 +0100
@@ -215,10 +215,8 @@
}
_items =
- Print_Operation.print_operations(PIDE.session).map(
- {
- case (name, description) => new Item(name, description, was_selected(name))
- })
+ for ((name, description) <- Print_Operation.get(PIDE.session))
+ yield new Item(name, description, was_selected(name))
_items
}