src/Pure/System/scala.scala
author wenzelm
Wed, 22 Jun 2022 13:42:30 +0200
changeset 75588 3349e360b71d
parent 75586 b2b097624e4c
child 75620 44815dc2b8f9
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71849
265bbad3d6af clarified modules;
wenzelm
parents: 71673
diff changeset
     1
/*  Title:      Pure/System/scala.scala
43744
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     3
71849
265bbad3d6af clarified modules;
wenzelm
parents: 71673
diff changeset
     4
Support for Scala at runtime.
43744
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     5
*/
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     6
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     7
package isabelle
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     8
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     9
71864
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
    10
import java.io.{File => JFile, StringWriter, PrintWriter}
56730
e723f041b6d0 tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents: 56667
diff changeset
    11
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
    12
import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
72294
25c6423ec538 clarified signature: proper eval/print via interpret;
wenzelm
parents: 72213
diff changeset
    13
import scala.tools.nsc.interpreter.{IMain, Results}
73136
ca17e9ebfdf1 updated to scala-2.13.4;
wenzelm
parents: 72763
diff changeset
    14
import scala.tools.nsc.interpreter.shell.ReplReporterImpl
43744
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    15
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    16
object Scala {
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    17
  /** registered functions **/
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    19
  abstract class Fun(val name: String, val thread: Boolean = false) {
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    20
    override def toString: String = name
75586
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    21
    def single: Boolean = false
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    22
    def bytes: Boolean = false
72756
72ac27ea12b2 more positions;
wenzelm
parents: 72332
diff changeset
    23
    def position: Properties.T = here.position
72ac27ea12b2 more positions;
wenzelm
parents: 72332
diff changeset
    24
    def here: Scala_Project.Here
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    25
    def invoke(args: List[Bytes]): List[Bytes]
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    26
  }
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    27
75588
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    28
  trait Single_Fun extends Fun { override def single: Boolean = true }
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    29
  trait Bytes_Fun extends Fun { override def bytes: Boolean = true }
75586
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    30
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    31
  abstract class Fun_Strings(name: String, thread: Boolean = false)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    32
  extends Fun(name, thread = thread) {
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    33
    override def invoke(args: List[Bytes]): List[Bytes] =
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    34
      apply(args.map(_.text)).map(Bytes.apply)
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    35
    def apply(args: List[String]): List[String]
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    36
  }
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    37
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    38
  abstract class Fun_String(name: String, thread: Boolean = false)
75588
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    39
  extends Fun_Strings(name, thread = thread) with Single_Fun {
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
    40
    override def apply(args: List[String]): List[String] =
73571
f86661e32bed clarified signature;
wenzelm
parents: 73565
diff changeset
    41
      List(apply(Library.the_single(args)))
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    42
    def apply(arg: String): String
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    43
  }
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    44
75588
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    45
  abstract class Fun_Bytes(name: String, thread: Boolean = false)
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    46
    extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun {
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    47
    override def invoke(args: List[Bytes]): List[Bytes] =
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    48
      List(apply(Library.the_single(args)))
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    49
    def apply(arg: Bytes): Bytes
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    50
  }
3349e360b71d clarified signature;
wenzelm
parents: 75586
diff changeset
    51
75586
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    52
  val encode_fun: XML.Encode.T[Fun] = { fun =>
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    53
    import XML.Encode._
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    54
    pair(string, pair(pair(bool, bool), properties))(
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    55
      fun.name, ((fun.single, fun.bytes), fun.position))
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    56
  }
b2b097624e4c clarified types and defaults;
wenzelm
parents: 75579
diff changeset
    57
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    58
  class Functions(val functions: Fun*) extends Isabelle_System.Service
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    59
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    60
  lazy val functions: List[Fun] =
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    61
    Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    62
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    63
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    64
72152
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    65
  /** demo functions **/
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    66
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    67
  object Echo extends Fun_String("echo") {
72756
72ac27ea12b2 more positions;
wenzelm
parents: 72332
diff changeset
    68
    val here = Scala_Project.here
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    69
    def apply(arg: String): String = arg
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    70
  }
72152
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    71
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    72
  object Sleep extends Fun_String("sleep") {
72756
72ac27ea12b2 more positions;
wenzelm
parents: 72332
diff changeset
    73
    val here = Scala_Project.here
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    74
    def apply(seconds: String): String = {
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    75
      val t =
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    76
        seconds match {
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    77
          case Value.Double(s) => Time.seconds(s)
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    78
          case _ => error("Malformed argument: " + quote(seconds))
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    79
        }
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    80
      val t0 = Time.now()
73702
7202e12cb324 tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents: 73576
diff changeset
    81
      t.sleep()
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    82
      val t1 = Time.now()
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    83
      (t1 - t0).toString
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
    84
    }
72152
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    85
  }
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    86
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    87
3fa75db844f5 clarified demo functions;
wenzelm
parents: 72151
diff changeset
    88
71870
82abfda58667 init default context;
wenzelm
parents: 71869
diff changeset
    89
  /** compiler **/
71850
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
    90
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73702
diff changeset
    91
  def class_path(): List[String] =
73988
678e1c9eb009 more robust: avoid duplicate classpath entries;
wenzelm
parents: 73987
diff changeset
    92
    for {
678e1c9eb009 more robust: avoid duplicate classpath entries;
wenzelm
parents: 73987
diff changeset
    93
      prop <- List("isabelle.scala.classpath", "java.class.path")
678e1c9eb009 more robust: avoid duplicate classpath entries;
wenzelm
parents: 73987
diff changeset
    94
      elems = System.getProperty(prop, "") if elems.nonEmpty
678e1c9eb009 more robust: avoid duplicate classpath entries;
wenzelm
parents: 73987
diff changeset
    95
      elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty
678e1c9eb009 more robust: avoid duplicate classpath entries;
wenzelm
parents: 73987
diff changeset
    96
    } yield elem
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73702
diff changeset
    97
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
    98
  object Compiler {
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
    99
    def default_print_writer: PrintWriter =
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   100
      new NewLinePrintWriter(new ConsoleWriter, true)
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   101
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   102
    def context(
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   103
      print_writer: PrintWriter = default_print_writer,
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   104
      error: String => Unit = Exn.error,
75442
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   105
      jar_dirs: List[JFile] = Nil,
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   106
      class_loader: Option[ClassLoader] = None
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
   107
    ): Context = {
71864
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   108
      def find_jars(dir: JFile): List[String] =
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   109
        File.find_files(dir, file => file.getName.endsWith(".jar")).
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   110
          map(File.absolute_name)
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   111
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   112
      val settings = new GenericRunnerSettings(error)
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   113
      settings.classpath.value =
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73702
diff changeset
   114
        (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
71850
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
   115
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   116
      new Context(settings, print_writer, class_loader)
71864
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   117
    }
71850
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
   118
75442
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   119
    class Context private [Compiler](
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   120
      val settings: GenericRunnerSettings,
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   121
      val print_writer: PrintWriter,
75442
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   122
      val class_loader: Option[ClassLoader]
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   123
    ) {
71869
2b7840fb2f90 tuned message;
wenzelm
parents: 71868
diff changeset
   124
      override def toString: String = settings.toString
2b7840fb2f90 tuned message;
wenzelm
parents: 71868
diff changeset
   125
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   126
      val interp: IMain =
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
   127
        new IMain(settings, new ReplReporterImpl(settings, print_writer)) {
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   128
          override def parentClassLoader: ClassLoader =
75442
d5041b68a237 clarified signature;
wenzelm
parents: 75441
diff changeset
   129
            class_loader getOrElse super.parentClassLoader
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   130
        }
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   131
    }
71850
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
   132
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   133
    def toplevel(interpret: Boolean, source: String): List[String] = {
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   134
      val out = new StringWriter
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   135
      val interp = Compiler.context(print_writer = new PrintWriter(out)).interp
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   136
      val marker = '\u000b'
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   137
      val ok =
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   138
        interp.withLabel(marker.toString) {
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   139
          if (interpret) interp.interpret(source) == Results.Success
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   140
          else (new interp.ReadEvalPrint).compile(source)
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   141
        }
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   142
      out.close()
71864
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   143
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   144
      val Error = """(?s)^\S* error: (.*)$""".r
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   145
      val errors =
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   146
        space_explode(marker, Library.strip_ansi_color(out.toString)).
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   147
          collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
71868
06ec50d9fc0a clarified signature;
wenzelm
parents: 71865
diff changeset
   148
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   149
      if (!ok && errors.isEmpty) List("Error") else errors
71864
bfc120aa737a clarified signature;
wenzelm
parents: 71862
diff changeset
   150
    }
72194
eef421b724c0 clarified names;
wenzelm
parents: 72193
diff changeset
   151
  }
71850
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
   152
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
   153
  object Toplevel extends Fun_String("scala_toplevel") {
72756
72ac27ea12b2 more positions;
wenzelm
parents: 72332
diff changeset
   154
    val here = Scala_Project.here
75429
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   155
    def apply(arg: String): String = {
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   156
      val (interpret, source) =
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   157
        YXML.parse_body(arg) match {
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   158
          case Nil => (false, "")
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   159
          case List(XML.Text(source)) => (false, source)
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   160
          case body => import XML.Decode._; pair(bool, string)(body)
436747f1f632 revert 2c861b196d52: still required in HOL/Library/Code_Test.thy;
wenzelm
parents: 75417
diff changeset
   161
        }
72194
eef421b724c0 clarified names;
wenzelm
parents: 72193
diff changeset
   162
      val errors =
75443
d6f2fbdc6322 clarified signature;
wenzelm
parents: 75442
diff changeset
   163
        try { Compiler.toplevel(interpret, source) }
72194
eef421b724c0 clarified names;
wenzelm
parents: 72193
diff changeset
   164
        catch { case ERROR(msg) => List(msg) }
eef421b724c0 clarified names;
wenzelm
parents: 72193
diff changeset
   165
      locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
   166
    }
71872
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
   167
  }
b5191ededb6c check Scala source snippets from ML;
wenzelm
parents: 71871
diff changeset
   168
71850
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
   169
f640380aaf86 clarified signature;
wenzelm
parents: 71849
diff changeset
   170
75444
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   171
  /** interpreter thread **/
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   172
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   173
  object Interpreter {
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   174
    /* requests */
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   175
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   176
    sealed abstract class Request
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   177
    case class Execute(command: Compiler.Context => Unit) extends Request
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   178
    case object Shutdown extends Request
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   179
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   180
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   181
    /* known interpreters */
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   182
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   183
    private val known = Synchronized(Set.empty[Interpreter])
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   184
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   185
    def add(interpreter: Interpreter): Unit = known.change(_ + interpreter)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   186
    def del(interpreter: Interpreter): Unit = known.change(_ - interpreter)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   187
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   188
    def get[A](which: PartialFunction[Interpreter, A]): Option[A] =
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   189
      known.value.collectFirst(which)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   190
  }
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   191
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   192
  class Interpreter(context: Compiler.Context) {
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   193
    interpreter =>
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   194
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   195
    private val running = Synchronized[Option[Thread]](None)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   196
    def running_thread(thread: Thread): Boolean = running.value.contains(thread)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   197
    def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt })
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   198
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   199
    private lazy val thread: Consumer_Thread[Interpreter.Request] =
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   200
      Consumer_Thread.fork("Scala.Interpreter") {
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   201
        case Interpreter.Execute(command) =>
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   202
          try {
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   203
            running.change(_ => Some(Thread.currentThread()))
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   204
            command(context)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   205
          }
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   206
          finally {
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   207
            running.change(_ => None)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   208
            Exn.Interrupt.dispose()
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   209
          }
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   210
          true
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   211
        case Interpreter.Shutdown =>
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   212
          Interpreter.del(interpreter)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   213
          false
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   214
      }
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   215
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   216
    def shutdown(): Unit = {
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   217
      thread.send(Interpreter.Shutdown)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   218
      interrupt_thread()
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   219
      thread.shutdown()
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   220
    }
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   221
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   222
    def execute(command: Compiler.Context => Unit): Unit =
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   223
      thread.send(Interpreter.Execute(command))
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   224
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   225
    Interpreter.add(interpreter)
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   226
    thread
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   227
  }
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   228
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   229
331f96a67924 clarified management of interpreter threads: more generic;
wenzelm
parents: 75443
diff changeset
   230
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71870
diff changeset
   231
  /** invoke Scala functions from ML **/
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71870
diff changeset
   232
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71870
diff changeset
   233
  /* invoke function */
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43744
diff changeset
   234
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
   235
  object Tag extends Enumeration {
65638
wenzelm
parents: 65220
diff changeset
   236
    val NULL, OK, ERROR, FAIL, INTERRUPT = Value
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43744
diff changeset
   237
  }
43744
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
   238
73419
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   239
  def function_thread(name: String): Boolean =
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   240
    functions.find(fun => fun.name == name) match {
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   241
      case Some(fun) => fun.thread
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   242
      case None => false
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   243
    }
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   244
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   245
  def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
71873
a7b81dd9954e tuned signature;
wenzelm
parents: 71872
diff changeset
   246
    functions.find(fun => fun.name == name) match {
a7b81dd9954e tuned signature;
wenzelm
parents: 71872
diff changeset
   247
      case Some(fun) =>
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   248
        Exn.capture { fun.invoke(args) } match {
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   249
          case Exn.Res(null) => (Tag.NULL, Nil)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43744
diff changeset
   250
          case Exn.Res(res) => (Tag.OK, res)
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   251
          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   252
          case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43744
diff changeset
   253
        }
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   254
      case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43744
diff changeset
   255
    }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   256
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   257
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   258
  /* protocol handler */
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   259
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
   260
  class Handler extends Session.Protocol_Handler {
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   261
    private var session: Session = null
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   262
    private var futures = Map.empty[String, Future[Unit]]
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   263
72213
wenzelm
parents: 72212
diff changeset
   264
    override def init(session: Session): Unit =
wenzelm
parents: 72212
diff changeset
   265
      synchronized { this.session = session }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   266
75380
2cb2606ce075 tuned: avoid problems with scala3;
wenzelm
parents: 74147
diff changeset
   267
    override def exit(): Unit = synchronized {
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   268
      for ((id, future) <- futures) cancel(id, future)
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   269
      futures = Map.empty
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   270
    }
65219
ed4b47b8c7dc misc tuning and simplification;
wenzelm
parents: 64442
diff changeset
   271
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   272
    private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
75380
2cb2606ce075 tuned: avoid problems with scala3;
wenzelm
parents: 74147
diff changeset
   273
      synchronized {
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   274
        if (futures.isDefinedAt(id)) {
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   275
          session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   276
          futures -= id
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   277
        }
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   278
      }
65220
wenzelm
parents: 65219
diff changeset
   279
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75380
diff changeset
   280
    private def cancel(id: String, future: Future[Unit]): Unit = {
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73356
diff changeset
   281
      future.cancel()
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   282
      result(id, Scala.Tag.INTERRUPT, Nil)
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   283
    }
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   284
75380
2cb2606ce075 tuned: avoid problems with scala3;
wenzelm
parents: 74147
diff changeset
   285
    private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   286
      msg.properties match {
73419
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   287
        case Markup.Invoke_Scala(name, id) =>
75441
400e325a5416 clarified signature, based on hints by IntelliJ IDEA;
wenzelm
parents: 75440
diff changeset
   288
          def body(): Unit = {
73565
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73523
diff changeset
   289
            val (tag, res) = Scala.function_body(name, msg.chunks)
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72294
diff changeset
   290
            result(id, tag, res)
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72294
diff changeset
   291
          }
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72294
diff changeset
   292
          val future =
73419
22f3f2117ed7 clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents: 73418
diff changeset
   293
            if (Scala.function_thread(name)) {
75441
400e325a5416 clarified signature, based on hints by IntelliJ IDEA;
wenzelm
parents: 75440
diff changeset
   294
              Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body())
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72294
diff changeset
   295
            }
75441
400e325a5416 clarified signature, based on hints by IntelliJ IDEA;
wenzelm
parents: 75440
diff changeset
   296
            else Future.fork(body())
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 72294
diff changeset
   297
          futures += (id -> future)
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   298
          true
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   299
        case _ => false
56387
d92eb5c3960d more general prover operations;
wenzelm
parents: 56385
diff changeset
   300
      }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   301
    }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   302
75380
2cb2606ce075 tuned: avoid problems with scala3;
wenzelm
parents: 74147
diff changeset
   303
    private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   304
      msg.properties match {
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   305
        case Markup.Cancel_Scala(id) =>
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   306
          futures.get(id) match {
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   307
            case Some(future) => cancel(id, future)
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   308
            case None =>
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   309
          }
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   310
          true
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   311
        case _ => false
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   312
      }
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   313
    }
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   314
75440
39011d0d2128 tuned signature;
wenzelm
parents: 75429
diff changeset
   315
    override val functions: Session.Protocol_Functions =
72157
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   316
      List(
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   317
        Markup.Invoke_Scala.name -> invoke_scala,
d1ca82e27cbc clarified names;
wenzelm
parents: 72152
diff changeset
   318
        Markup.Cancel_Scala.name -> cancel_scala)
52111
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   319
  }
1fd184eaa310 explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents: 49470
diff changeset
   320
}
71871
28def00726ca more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
wenzelm
parents: 71870
diff changeset
   321
72193
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
   322
class Scala_Functions extends Scala.Functions(
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
   323
  Scala.Echo,
742d94015918 clarified signature;
wenzelm
parents: 72159
diff changeset
   324
  Scala.Sleep,
72194
eef421b724c0 clarified names;
wenzelm
parents: 72193
diff changeset
   325
  Scala.Toplevel,
73576
b50f8cc8c08e support for base64 via Isabelle/Scala/ML;
wenzelm
parents: 73571
diff changeset
   326
  Bytes.Decode_Base64,
b50f8cc8c08e support for base64 via Isabelle/Scala/ML;
wenzelm
parents: 73571
diff changeset
   327
  Bytes.Encode_Base64,
75579
3362b6a5d697 support XZ compression in Isabelle/ML;
wenzelm
parents: 75444
diff changeset
   328
  Bytes.Compress,
3362b6a5d697 support XZ compression in Isabelle/ML;
wenzelm
parents: 75444
diff changeset
   329
  Bytes.Uncompress,
72760
042180540068 clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents: 72756
diff changeset
   330
  Doc.Doc_Names,
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72760
diff changeset
   331
  Bibtex.Check_Database,
73314
87403fde8cc3 more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
wenzelm
parents: 73228
diff changeset
   332
  Isabelle_System.Make_Directory,
73322
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73314
diff changeset
   333
  Isabelle_System.Copy_Dir,
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73314
diff changeset
   334
  Isabelle_System.Copy_File,
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73314
diff changeset
   335
  Isabelle_System.Copy_File_Base,
73324
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73323
diff changeset
   336
  Isabelle_System.Rm_Tree,
73323
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73322
diff changeset
   337
  Isabelle_System.Download,
73523
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73431
diff changeset
   338
  Isabelle_System.Isabelle_Id,
73418
7d7d959547a1 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents: 73367
diff changeset
   339
  Isabelle_Tool.Isabelle_Tools,
73431
f27d7b12e8a4 support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents: 73419
diff changeset
   340
  isabelle.atp.SystemOnTPTP.List_Systems,
f27d7b12e8a4 support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp;
wenzelm
parents: 73419
diff changeset
   341
  isabelle.atp.SystemOnTPTP.Run_System)