--- a/src/Pure/ROOT.ML Wed May 20 15:00:25 2020 +0100
+++ b/src/Pure/ROOT.ML Wed May 20 20:45:43 2020 +0200
@@ -327,7 +327,7 @@
ML_file "System/command_line.ML";
ML_file "System/message_channel.ML";
ML_file "System/isabelle_process.ML";
-ML_file "System/invoke_scala.ML";
+ML_file "System/scala.ML";
ML_file "Thy/bibtex.ML";
ML_file "PIDE/protocol.ML";
ML_file "General/output_primitives_virtual.ML";
--- a/src/Pure/System/invoke_scala.ML Wed May 20 15:00:25 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: Pure/System/invoke_scala.ML
- Author: Makarius
-
-JVM method invocation service via Isabelle/Scala.
-*)
-
-signature INVOKE_SCALA =
-sig
- val method: string -> string -> string
- val promise_method: string -> string -> string future
- exception Null
-end;
-
-structure Invoke_Scala: INVOKE_SCALA =
-struct
-
-val _ = Session.protocol_handler "isabelle.Invoke_Scala";
-
-
-(* pending promises *)
-
-val new_id = string_of_int o Counter.make ();
-
-val promises =
- Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
-
-
-(* method invocation *)
-
-fun promise_method name arg =
- let
- val id = new_id ();
- fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
- val promise = Future.promise_name "invoke_scala" abort : string future;
- val _ = Synchronized.change promises (Symtab.update (id, promise));
- val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
- in promise end;
-
-fun method name arg = Future.join (promise_method name arg);
-
-
-(* fulfill *)
-
-exception Null;
-
-fun fulfill id tag res =
- let
- val result =
- (case tag of
- "0" => Exn.Exn Null
- | "1" => Exn.Res res
- | "2" => Exn.Exn (ERROR res)
- | "3" => Exn.Exn (Fail res)
- | "4" => Exn.Exn Exn.Interrupt
- | _ => raise Fail "Bad tag");
- val promise =
- Synchronized.change_result promises
- (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
- val _ = Future.fulfill_result promise result;
- in () end;
-
-val _ =
- Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
- (fn [id, tag, res] =>
- fulfill id tag res
- handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
-
-end;
-
--- a/src/Pure/System/invoke_scala.scala Wed May 20 15:00:25 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-/* Title: Pure/System/invoke_scala.scala
- Author: Makarius
-
-JVM method invocation service via Isabelle/Scala.
-*/
-
-package isabelle
-
-
-import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-
-import scala.util.matching.Regex
-
-
-object Invoke_Scala
-{
- /* method reflection */
-
- private val Ext = new Regex("(.*)\\.([^.]*)")
- private val STRING = Class.forName("java.lang.String")
-
- private def get_method(name: String): String => String =
- name match {
- case Ext(class_name, method_name) =>
- val m =
- try { Class.forName(class_name).getMethod(method_name, STRING) }
- catch {
- case _: ClassNotFoundException | _: NoSuchMethodException =>
- error("No such method: " + quote(name))
- }
- if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
- if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
-
- (arg: String) => {
- try { m.invoke(null, arg).asInstanceOf[String] }
- catch {
- case e: InvocationTargetException if e.getCause != null =>
- throw e.getCause
- }
- }
- case _ => error("Malformed method name: " + quote(name))
- }
-
-
- /* method invocation */
-
- object Tag extends Enumeration
- {
- val NULL, OK, ERROR, FAIL, INTERRUPT = Value
- }
-
- def method(name: String, arg: String): (Tag.Value, String) =
- Exn.capture { get_method(name) } match {
- case Exn.Res(f) =>
- Exn.capture { f(arg) } match {
- case Exn.Res(null) => (Tag.NULL, "")
- case Exn.Res(res) => (Tag.OK, res)
- case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
- case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
- }
- case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
- }
-}
-
-
-/* protocol handler */
-
-class Invoke_Scala extends Session.Protocol_Handler
-{
- 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 exit(): Unit = synchronized
- {
- for ((id, future) <- futures) cancel(id, future)
- futures = Map.empty
- }
-
- private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
- synchronized
- {
- if (futures.isDefinedAt(id)) {
- session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
- futures -= id
- }
- }
-
- private def cancel(id: String, future: Future[Unit])
- {
- future.cancel
- fulfill(id, Invoke_Scala.Tag.INTERRUPT, "")
- }
-
- private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
- {
- msg.properties match {
- case Markup.Invoke_Scala(name, id) =>
- futures += (id ->
- Future.fork {
- val (tag, result) = Invoke_Scala.method(name, msg.text)
- fulfill(id, tag, result)
- })
- true
- case _ => false
- }
- }
-
- private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
- {
- msg.properties match {
- case Markup.Cancel_Scala(id) =>
- futures.get(id) match {
- case Some(future) => cancel(id, future)
- case None =>
- }
- true
- case _ => false
- }
- }
-
- val functions =
- List(
- Markup.Invoke_Scala.name -> invoke_scala,
- Markup.Cancel_Scala.name -> cancel_scala)
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala.ML Wed May 20 20:45:43 2020 +0200
@@ -0,0 +1,70 @@
+(* Title: Pure/System/scala.ML
+ Author: Makarius
+
+Support for Scala at runtime.
+*)
+
+signature SCALA =
+sig
+ val method: string -> string -> string
+ val promise_method: string -> string -> string future
+ exception Null
+end;
+
+structure Scala: SCALA =
+struct
+
+(** invoke JVM method via Isabelle/Scala **)
+
+val _ = Session.protocol_handler "isabelle.Scala";
+
+
+(* pending promises *)
+
+val new_id = string_of_int o Counter.make ();
+
+val promises =
+ Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
+
+
+(* method invocation *)
+
+fun promise_method name arg =
+ let
+ val id = new_id ();
+ fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
+ val promise = Future.promise_name "invoke_scala" abort : string future;
+ val _ = Synchronized.change promises (Symtab.update (id, promise));
+ val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
+ in promise end;
+
+fun method name arg = Future.join (promise_method name arg);
+
+
+(* fulfill *)
+
+exception Null;
+
+fun fulfill id tag res =
+ let
+ val result =
+ (case tag of
+ "0" => Exn.Exn Null
+ | "1" => Exn.Res res
+ | "2" => Exn.Exn (ERROR res)
+ | "3" => Exn.Exn (Fail res)
+ | "4" => Exn.Exn Exn.Interrupt
+ | _ => raise Fail "Bad tag");
+ val promise =
+ Synchronized.change_result promises
+ (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
+ val _ = Future.fulfill_result promise result;
+ in () end;
+
+val _ =
+ Isabelle_Process.protocol_command "Scala.fulfill"
+ (fn [id, tag, res] =>
+ fulfill id tag res
+ handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala.scala Wed May 20 20:45:43 2020 +0200
@@ -0,0 +1,130 @@
+/* Title: Pure/System/scala.scala
+ Author: Makarius
+
+Support for Scala at runtime.
+*/
+
+package isabelle
+
+
+import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+
+import scala.util.matching.Regex
+
+
+object Scala
+{
+ /** invoke JVM method via Isabelle/Scala **/
+
+ /* method reflection */
+
+ private val Ext = new Regex("(.*)\\.([^.]*)")
+ private val STRING = Class.forName("java.lang.String")
+
+ private def get_method(name: String): String => String =
+ name match {
+ case Ext(class_name, method_name) =>
+ val m =
+ try { Class.forName(class_name).getMethod(method_name, STRING) }
+ catch {
+ case _: ClassNotFoundException | _: NoSuchMethodException =>
+ error("No such method: " + quote(name))
+ }
+ if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
+ if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
+
+ (arg: String) => {
+ try { m.invoke(null, arg).asInstanceOf[String] }
+ catch {
+ case e: InvocationTargetException if e.getCause != null =>
+ throw e.getCause
+ }
+ }
+ case _ => error("Malformed method name: " + quote(name))
+ }
+
+
+ /* method invocation */
+
+ object Tag extends Enumeration
+ {
+ val NULL, OK, ERROR, FAIL, INTERRUPT = Value
+ }
+
+ def method(name: String, arg: String): (Tag.Value, String) =
+ Exn.capture { get_method(name) } match {
+ case Exn.Res(f) =>
+ Exn.capture { f(arg) } match {
+ case Exn.Res(null) => (Tag.NULL, "")
+ case Exn.Res(res) => (Tag.OK, res)
+ case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
+ case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
+ }
+ case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
+ }
+}
+
+
+/* protocol handler */
+
+class Scala extends Session.Protocol_Handler
+{
+ 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 exit(): Unit = synchronized
+ {
+ for ((id, future) <- futures) cancel(id, future)
+ futures = Map.empty
+ }
+
+ private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit =
+ synchronized
+ {
+ if (futures.isDefinedAt(id)) {
+ session.protocol_command("Scala.fulfill", id, tag.id.toString, res)
+ futures -= id
+ }
+ }
+
+ private def cancel(id: String, future: Future[Unit])
+ {
+ future.cancel
+ fulfill(id, Scala.Tag.INTERRUPT, "")
+ }
+
+ private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
+ {
+ msg.properties match {
+ case Markup.Invoke_Scala(name, id) =>
+ futures += (id ->
+ Future.fork {
+ val (tag, result) = Scala.method(name, msg.text)
+ fulfill(id, tag, result)
+ })
+ true
+ case _ => false
+ }
+ }
+
+ private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
+ {
+ msg.properties match {
+ case Markup.Cancel_Scala(id) =>
+ futures.get(id) match {
+ case Some(future) => cancel(id, future)
+ case None =>
+ }
+ true
+ case _ => false
+ }
+ }
+
+ val functions =
+ List(
+ Markup.Invoke_Scala.name -> invoke_scala,
+ Markup.Cancel_Scala.name -> cancel_scala)
+}
--- a/src/Pure/Thy/bibtex.ML Wed May 20 15:00:25 2020 +0100
+++ b/src/Pure/Thy/bibtex.ML Wed May 20 20:45:43 2020 +0200
@@ -20,7 +20,7 @@
type message = string * Position.T;
fun check_database pos0 database =
- Invoke_Scala.method "isabelle.Bibtex.check_database_yxml" database
+ Scala.method "isabelle.Bibtex.check_database_yxml" database
|> YXML.parse_body
|> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
|> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
--- a/src/Pure/build-jars Wed May 20 15:00:25 2020 +0100
+++ b/src/Pure/build-jars Wed May 20 20:45:43 2020 +0200
@@ -120,7 +120,6 @@
src/Pure/System/cygwin.scala
src/Pure/System/distribution.scala
src/Pure/System/getopts.scala
- src/Pure/System/invoke_scala.scala
src/Pure/System/isabelle_charset.scala
src/Pure/System/isabelle_fonts.scala
src/Pure/System/isabelle_process.scala
@@ -133,6 +132,7 @@
src/Pure/System/posix_interrupt.scala
src/Pure/System/process_result.scala
src/Pure/System/progress.scala
+ src/Pure/System/scala.scala
src/Pure/System/system_channel.scala
src/Pure/System/tty_loop.scala
src/Pure/Thy/bibtex.scala