clarified modules;
authorwenzelm
Wed May 20 20:45:43 2020 +0200 (11 days ago)
changeset 71849265bbad3d6af
parent 71848 3c7852327787
child 71850 f640380aaf86
clarified modules;
src/Pure/ROOT.ML
src/Pure/System/invoke_scala.ML
src/Pure/System/invoke_scala.scala
src/Pure/System/scala.ML
src/Pure/System/scala.scala
src/Pure/Thy/bibtex.ML
src/Pure/build-jars
     1.1 --- a/src/Pure/ROOT.ML	Wed May 20 15:00:25 2020 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed May 20 20:45:43 2020 +0200
     1.3 @@ -327,7 +327,7 @@
     1.4  ML_file "System/command_line.ML";
     1.5  ML_file "System/message_channel.ML";
     1.6  ML_file "System/isabelle_process.ML";
     1.7 -ML_file "System/invoke_scala.ML";
     1.8 +ML_file "System/scala.ML";
     1.9  ML_file "Thy/bibtex.ML";
    1.10  ML_file "PIDE/protocol.ML";
    1.11  ML_file "General/output_primitives_virtual.ML";
     2.1 --- a/src/Pure/System/invoke_scala.ML	Wed May 20 15:00:25 2020 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,69 +0,0 @@
     2.4 -(*  Title:      Pure/System/invoke_scala.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -JVM method invocation service via Isabelle/Scala.
     2.8 -*)
     2.9 -
    2.10 -signature INVOKE_SCALA =
    2.11 -sig
    2.12 -  val method: string -> string -> string
    2.13 -  val promise_method: string -> string -> string future
    2.14 -  exception Null
    2.15 -end;
    2.16 -
    2.17 -structure Invoke_Scala: INVOKE_SCALA =
    2.18 -struct
    2.19 -
    2.20 -val _ = Session.protocol_handler "isabelle.Invoke_Scala";
    2.21 -
    2.22 -
    2.23 -(* pending promises *)
    2.24 -
    2.25 -val new_id = string_of_int o Counter.make ();
    2.26 -
    2.27 -val promises =
    2.28 -  Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
    2.29 -
    2.30 -
    2.31 -(* method invocation *)
    2.32 -
    2.33 -fun promise_method name arg =
    2.34 -  let
    2.35 -    val id = new_id ();
    2.36 -    fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    2.37 -    val promise = Future.promise_name "invoke_scala" abort : string future;
    2.38 -    val _ = Synchronized.change promises (Symtab.update (id, promise));
    2.39 -    val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
    2.40 -  in promise end;
    2.41 -
    2.42 -fun method name arg = Future.join (promise_method name arg);
    2.43 -
    2.44 -
    2.45 -(* fulfill *)
    2.46 -
    2.47 -exception Null;
    2.48 -
    2.49 -fun fulfill id tag res =
    2.50 -  let
    2.51 -    val result =
    2.52 -      (case tag of
    2.53 -        "0" => Exn.Exn Null
    2.54 -      | "1" => Exn.Res res
    2.55 -      | "2" => Exn.Exn (ERROR res)
    2.56 -      | "3" => Exn.Exn (Fail res)
    2.57 -      | "4" => Exn.Exn Exn.Interrupt
    2.58 -      | _ => raise Fail "Bad tag");
    2.59 -    val promise =
    2.60 -      Synchronized.change_result promises
    2.61 -        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
    2.62 -    val _ = Future.fulfill_result promise result;
    2.63 -  in () end;
    2.64 -
    2.65 -val _ =
    2.66 -  Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
    2.67 -    (fn [id, tag, res] =>
    2.68 -      fulfill id tag res
    2.69 -        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
    2.70 -
    2.71 -end;
    2.72 -
     3.1 --- a/src/Pure/System/invoke_scala.scala	Wed May 20 15:00:25 2020 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,128 +0,0 @@
     3.4 -/*  Title:      Pure/System/invoke_scala.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -JVM method invocation service via Isabelle/Scala.
     3.8 -*/
     3.9 -
    3.10 -package isabelle
    3.11 -
    3.12 -
    3.13 -import java.lang.reflect.{Method, Modifier, InvocationTargetException}
    3.14 -
    3.15 -import scala.util.matching.Regex
    3.16 -
    3.17 -
    3.18 -object Invoke_Scala
    3.19 -{
    3.20 -  /* method reflection */
    3.21 -
    3.22 -  private val Ext = new Regex("(.*)\\.([^.]*)")
    3.23 -  private val STRING = Class.forName("java.lang.String")
    3.24 -
    3.25 -  private def get_method(name: String): String => String =
    3.26 -    name match {
    3.27 -      case Ext(class_name, method_name) =>
    3.28 -        val m =
    3.29 -          try { Class.forName(class_name).getMethod(method_name, STRING) }
    3.30 -          catch {
    3.31 -            case _: ClassNotFoundException | _: NoSuchMethodException =>
    3.32 -              error("No such method: " + quote(name))
    3.33 -          }
    3.34 -        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    3.35 -        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
    3.36 -
    3.37 -        (arg: String) => {
    3.38 -          try { m.invoke(null, arg).asInstanceOf[String] }
    3.39 -          catch {
    3.40 -            case e: InvocationTargetException if e.getCause != null =>
    3.41 -              throw e.getCause
    3.42 -          }
    3.43 -        }
    3.44 -      case _ => error("Malformed method name: " + quote(name))
    3.45 -    }
    3.46 -
    3.47 -
    3.48 -  /* method invocation */
    3.49 -
    3.50 -  object Tag extends Enumeration
    3.51 -  {
    3.52 -    val NULL, OK, ERROR, FAIL, INTERRUPT = Value
    3.53 -  }
    3.54 -
    3.55 -  def method(name: String, arg: String): (Tag.Value, String) =
    3.56 -    Exn.capture { get_method(name) } match {
    3.57 -      case Exn.Res(f) =>
    3.58 -        Exn.capture { f(arg) } match {
    3.59 -          case Exn.Res(null) => (Tag.NULL, "")
    3.60 -          case Exn.Res(res) => (Tag.OK, res)
    3.61 -          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
    3.62 -          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    3.63 -        }
    3.64 -      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    3.65 -    }
    3.66 -}
    3.67 -
    3.68 -
    3.69 -/* protocol handler */
    3.70 -
    3.71 -class Invoke_Scala extends Session.Protocol_Handler
    3.72 -{
    3.73 -  private var session: Session = null
    3.74 -  private var futures = Map.empty[String, Future[Unit]]
    3.75 -
    3.76 -  override def init(init_session: Session): Unit =
    3.77 -    synchronized { session = init_session }
    3.78 -
    3.79 -  override def exit(): Unit = synchronized
    3.80 -  {
    3.81 -    for ((id, future) <- futures) cancel(id, future)
    3.82 -    futures = Map.empty
    3.83 -  }
    3.84 -
    3.85 -  private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    3.86 -    synchronized
    3.87 -    {
    3.88 -      if (futures.isDefinedAt(id)) {
    3.89 -        session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
    3.90 -        futures -= id
    3.91 -      }
    3.92 -    }
    3.93 -
    3.94 -  private def cancel(id: String, future: Future[Unit])
    3.95 -  {
    3.96 -    future.cancel
    3.97 -    fulfill(id, Invoke_Scala.Tag.INTERRUPT, "")
    3.98 -  }
    3.99 -
   3.100 -  private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   3.101 -  {
   3.102 -    msg.properties match {
   3.103 -      case Markup.Invoke_Scala(name, id) =>
   3.104 -        futures += (id ->
   3.105 -          Future.fork {
   3.106 -            val (tag, result) = Invoke_Scala.method(name, msg.text)
   3.107 -            fulfill(id, tag, result)
   3.108 -          })
   3.109 -        true
   3.110 -      case _ => false
   3.111 -    }
   3.112 -  }
   3.113 -
   3.114 -  private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   3.115 -  {
   3.116 -    msg.properties match {
   3.117 -      case Markup.Cancel_Scala(id) =>
   3.118 -        futures.get(id) match {
   3.119 -          case Some(future) => cancel(id, future)
   3.120 -          case None =>
   3.121 -        }
   3.122 -        true
   3.123 -      case _ => false
   3.124 -    }
   3.125 -  }
   3.126 -
   3.127 -  val functions =
   3.128 -    List(
   3.129 -      Markup.Invoke_Scala.name -> invoke_scala,
   3.130 -      Markup.Cancel_Scala.name -> cancel_scala)
   3.131 -}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/System/scala.ML	Wed May 20 20:45:43 2020 +0200
     4.3 @@ -0,0 +1,70 @@
     4.4 +(*  Title:      Pure/System/scala.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Support for Scala at runtime.
     4.8 +*)
     4.9 +
    4.10 +signature SCALA =
    4.11 +sig
    4.12 +  val method: string -> string -> string
    4.13 +  val promise_method: string -> string -> string future
    4.14 +  exception Null
    4.15 +end;
    4.16 +
    4.17 +structure Scala: SCALA =
    4.18 +struct
    4.19 +
    4.20 +(** invoke JVM method via Isabelle/Scala **)
    4.21 +
    4.22 +val _ = Session.protocol_handler "isabelle.Scala";
    4.23 +
    4.24 +
    4.25 +(* pending promises *)
    4.26 +
    4.27 +val new_id = string_of_int o Counter.make ();
    4.28 +
    4.29 +val promises =
    4.30 +  Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
    4.31 +
    4.32 +
    4.33 +(* method invocation *)
    4.34 +
    4.35 +fun promise_method name arg =
    4.36 +  let
    4.37 +    val id = new_id ();
    4.38 +    fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
    4.39 +    val promise = Future.promise_name "invoke_scala" abort : string future;
    4.40 +    val _ = Synchronized.change promises (Symtab.update (id, promise));
    4.41 +    val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
    4.42 +  in promise end;
    4.43 +
    4.44 +fun method name arg = Future.join (promise_method name arg);
    4.45 +
    4.46 +
    4.47 +(* fulfill *)
    4.48 +
    4.49 +exception Null;
    4.50 +
    4.51 +fun fulfill id tag res =
    4.52 +  let
    4.53 +    val result =
    4.54 +      (case tag of
    4.55 +        "0" => Exn.Exn Null
    4.56 +      | "1" => Exn.Res res
    4.57 +      | "2" => Exn.Exn (ERROR res)
    4.58 +      | "3" => Exn.Exn (Fail res)
    4.59 +      | "4" => Exn.Exn Exn.Interrupt
    4.60 +      | _ => raise Fail "Bad tag");
    4.61 +    val promise =
    4.62 +      Synchronized.change_result promises
    4.63 +        (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab));
    4.64 +    val _ = Future.fulfill_result promise result;
    4.65 +  in () end;
    4.66 +
    4.67 +val _ =
    4.68 +  Isabelle_Process.protocol_command "Scala.fulfill"
    4.69 +    (fn [id, tag, res] =>
    4.70 +      fulfill id tag res
    4.71 +        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
    4.72 +
    4.73 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/System/scala.scala	Wed May 20 20:45:43 2020 +0200
     5.3 @@ -0,0 +1,130 @@
     5.4 +/*  Title:      Pure/System/scala.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Support for Scala at runtime.
     5.8 +*/
     5.9 +
    5.10 +package isabelle
    5.11 +
    5.12 +
    5.13 +import java.lang.reflect.{Method, Modifier, InvocationTargetException}
    5.14 +
    5.15 +import scala.util.matching.Regex
    5.16 +
    5.17 +
    5.18 +object Scala
    5.19 +{
    5.20 +  /** invoke JVM method via Isabelle/Scala **/
    5.21 +
    5.22 +  /* method reflection */
    5.23 +
    5.24 +  private val Ext = new Regex("(.*)\\.([^.]*)")
    5.25 +  private val STRING = Class.forName("java.lang.String")
    5.26 +
    5.27 +  private def get_method(name: String): String => String =
    5.28 +    name match {
    5.29 +      case Ext(class_name, method_name) =>
    5.30 +        val m =
    5.31 +          try { Class.forName(class_name).getMethod(method_name, STRING) }
    5.32 +          catch {
    5.33 +            case _: ClassNotFoundException | _: NoSuchMethodException =>
    5.34 +              error("No such method: " + quote(name))
    5.35 +          }
    5.36 +        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    5.37 +        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
    5.38 +
    5.39 +        (arg: String) => {
    5.40 +          try { m.invoke(null, arg).asInstanceOf[String] }
    5.41 +          catch {
    5.42 +            case e: InvocationTargetException if e.getCause != null =>
    5.43 +              throw e.getCause
    5.44 +          }
    5.45 +        }
    5.46 +      case _ => error("Malformed method name: " + quote(name))
    5.47 +    }
    5.48 +
    5.49 +
    5.50 +  /* method invocation */
    5.51 +
    5.52 +  object Tag extends Enumeration
    5.53 +  {
    5.54 +    val NULL, OK, ERROR, FAIL, INTERRUPT = Value
    5.55 +  }
    5.56 +
    5.57 +  def method(name: String, arg: String): (Tag.Value, String) =
    5.58 +    Exn.capture { get_method(name) } match {
    5.59 +      case Exn.Res(f) =>
    5.60 +        Exn.capture { f(arg) } match {
    5.61 +          case Exn.Res(null) => (Tag.NULL, "")
    5.62 +          case Exn.Res(res) => (Tag.OK, res)
    5.63 +          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
    5.64 +          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    5.65 +        }
    5.66 +      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    5.67 +    }
    5.68 +}
    5.69 +
    5.70 +
    5.71 +/* protocol handler */
    5.72 +
    5.73 +class Scala extends Session.Protocol_Handler
    5.74 +{
    5.75 +  private var session: Session = null
    5.76 +  private var futures = Map.empty[String, Future[Unit]]
    5.77 +
    5.78 +  override def init(init_session: Session): Unit =
    5.79 +    synchronized { session = init_session }
    5.80 +
    5.81 +  override def exit(): Unit = synchronized
    5.82 +  {
    5.83 +    for ((id, future) <- futures) cancel(id, future)
    5.84 +    futures = Map.empty
    5.85 +  }
    5.86 +
    5.87 +  private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit =
    5.88 +    synchronized
    5.89 +    {
    5.90 +      if (futures.isDefinedAt(id)) {
    5.91 +        session.protocol_command("Scala.fulfill", id, tag.id.toString, res)
    5.92 +        futures -= id
    5.93 +      }
    5.94 +    }
    5.95 +
    5.96 +  private def cancel(id: String, future: Future[Unit])
    5.97 +  {
    5.98 +    future.cancel
    5.99 +    fulfill(id, Scala.Tag.INTERRUPT, "")
   5.100 +  }
   5.101 +
   5.102 +  private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   5.103 +  {
   5.104 +    msg.properties match {
   5.105 +      case Markup.Invoke_Scala(name, id) =>
   5.106 +        futures += (id ->
   5.107 +          Future.fork {
   5.108 +            val (tag, result) = Scala.method(name, msg.text)
   5.109 +            fulfill(id, tag, result)
   5.110 +          })
   5.111 +        true
   5.112 +      case _ => false
   5.113 +    }
   5.114 +  }
   5.115 +
   5.116 +  private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   5.117 +  {
   5.118 +    msg.properties match {
   5.119 +      case Markup.Cancel_Scala(id) =>
   5.120 +        futures.get(id) match {
   5.121 +          case Some(future) => cancel(id, future)
   5.122 +          case None =>
   5.123 +        }
   5.124 +        true
   5.125 +      case _ => false
   5.126 +    }
   5.127 +  }
   5.128 +
   5.129 +  val functions =
   5.130 +    List(
   5.131 +      Markup.Invoke_Scala.name -> invoke_scala,
   5.132 +      Markup.Cancel_Scala.name -> cancel_scala)
   5.133 +}
     6.1 --- a/src/Pure/Thy/bibtex.ML	Wed May 20 15:00:25 2020 +0100
     6.2 +++ b/src/Pure/Thy/bibtex.ML	Wed May 20 20:45:43 2020 +0200
     6.3 @@ -20,7 +20,7 @@
     6.4  type message = string * Position.T;
     6.5  
     6.6  fun check_database pos0 database =
     6.7 -  Invoke_Scala.method "isabelle.Bibtex.check_database_yxml" database
     6.8 +  Scala.method "isabelle.Bibtex.check_database_yxml" database
     6.9    |> YXML.parse_body
    6.10    |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
    6.11    |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
     7.1 --- a/src/Pure/build-jars	Wed May 20 15:00:25 2020 +0100
     7.2 +++ b/src/Pure/build-jars	Wed May 20 20:45:43 2020 +0200
     7.3 @@ -120,7 +120,6 @@
     7.4    src/Pure/System/cygwin.scala
     7.5    src/Pure/System/distribution.scala
     7.6    src/Pure/System/getopts.scala
     7.7 -  src/Pure/System/invoke_scala.scala
     7.8    src/Pure/System/isabelle_charset.scala
     7.9    src/Pure/System/isabelle_fonts.scala
    7.10    src/Pure/System/isabelle_process.scala
    7.11 @@ -133,6 +132,7 @@
    7.12    src/Pure/System/posix_interrupt.scala
    7.13    src/Pure/System/process_result.scala
    7.14    src/Pure/System/progress.scala
    7.15 +  src/Pure/System/scala.scala
    7.16    src/Pure/System/system_channel.scala
    7.17    src/Pure/System/tty_loop.scala
    7.18    src/Pure/Thy/bibtex.scala