# HG changeset patch # User paulson # Date 1598612693 -3600 # Node ID 3afe53e8b2bab0ff7884429f48e7ba2d4b29d7cf # Parent a51736641843c7536b46f3028dc3c853e9bd31be# Parent 01397b6e5eb06413d1c660a27f2034e95dcded38 merged diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/HOL/Tools/Nitpick/kodkod.scala --- 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 **/ diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/HOL/Tools/etc/settings --- 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' diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/ML/ml_statistics.scala --- 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) } diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/PIDE/protocol.ML --- 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" diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/PIDE/protocol_handlers.scala --- 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)) diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/PIDE/session.scala --- 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)) diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/System/isabelle_system.scala --- 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 { diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/System/scala.scala --- 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) diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/Tools/build.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, diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/Tools/debugger.scala --- 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) diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/Tools/print_operation.scala --- 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) } } diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/Tools/simplifier_trace.scala --- 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) } } diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Pure/library.scala --- 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) + } } diff -r 01397b6e5eb0 -r 3afe53e8b2ba src/Tools/jEdit/src/query_dockable.scala --- 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 }