# HG changeset patch
# User wenzelm
# Date 1597491925 -7200
# Node ID d1ca82e27cbca59d21e6b4445fc9a85aceaffd18
# Parent  065dcd80293e1c39f272ba1ec557813ab641d3e2
clarified names;

diff -r 065dcd80293e -r d1ca82e27cbc etc/settings
--- a/etc/settings	Sat Aug 15 13:37:34 2020 +0200
+++ b/etc/settings	Sat Aug 15 13:45:25 2020 +0200
@@ -27,8 +27,8 @@
 
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
-isabelle_scala_service 'isabelle.ML_Statistics$Protocol_Handler'
-isabelle_scala_service 'isabelle.Scala'
+isabelle_scala_service 'isabelle.ML_Statistics$Handler'
+isabelle_scala_service 'isabelle.Scala$Handler'
 isabelle_scala_service 'isabelle.Print_Operation$Handler'
 isabelle_scala_service 'isabelle.Simplifier_Trace$Handler'
 
diff -r 065dcd80293e -r d1ca82e27cbc src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Aug 15 13:37:34 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Sat Aug 15 13:45:25 2020 +0200
@@ -80,7 +80,7 @@
 
   /* protocol handler */
 
-  class Protocol_Handler extends Session.Protocol_Handler
+  class Handler extends Session.Protocol_Handler
   {
     private var session: Session = null
     private var monitoring: Future[Unit] = Future.value(())
diff -r 065dcd80293e -r d1ca82e27cbc src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Aug 15 13:37:34 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat Aug 15 13:45:25 2020 +0200
@@ -138,71 +138,71 @@
         }
       case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
     }
-}
 
 
-/* protocol handler */
+  /* protocol handler */
+
+  class Handler extends Session.Protocol_Handler
+  {
+    private var session: Session = null
+    private var futures = Map.empty[String, Future[Unit]]
 
-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 init(init_session: Session): Unit =
-    synchronized { session = init_session }
+    override def exit(): Unit = synchronized
+    {
+      for ((id, future) <- futures) cancel(id, future)
+      futures = Map.empty
+    }
 
-  override def exit(): Unit = synchronized
-  {
-    for ((id, future) <- futures) cancel(id, future)
-    futures = Map.empty
-  }
+    private def result(id: String, tag: Scala.Tag.Value, res: String): Unit =
+      synchronized
+      {
+        if (futures.isDefinedAt(id)) {
+          session.protocol_command("Scala.result", id, tag.id.toString, res)
+          futures -= id
+        }
+      }
 
-  private def result(id: String, tag: Scala.Tag.Value, res: String): Unit =
-    synchronized
+    private def cancel(id: String, future: Future[Unit])
+    {
+      future.cancel
+      result(id, Scala.Tag.INTERRUPT, "")
+    }
+
+    private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
     {
-      if (futures.isDefinedAt(id)) {
-        session.protocol_command("Scala.result", id, tag.id.toString, res)
-        futures -= id
+      msg.properties match {
+        case Markup.Invoke_Scala(name, id) =>
+          futures += (id ->
+            Future.fork {
+              val (tag, res) = Scala.function(name, msg.text)
+              result(id, tag, res)
+            })
+          true
+        case _ => false
       }
     }
 
-  private def cancel(id: String, future: Future[Unit])
-  {
-    future.cancel
-    result(id, Scala.Tag.INTERRUPT, "")
-  }
+    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
+      }
+    }
 
-  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, res) = Scala.function(name, msg.text)
-            result(id, tag, res)
-          })
-        true
-      case _ => false
-    }
+    val functions =
+      List(
+        Markup.Invoke_Scala.name -> invoke_scala,
+        Markup.Cancel_Scala.name -> cancel_scala)
   }
-
-  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)
 }