# HG changeset patch
# User wenzelm
# Date 1650528218 -7200
# Node ID 39011d0d2128e7554c5e572be993a071ab704861
# Parent  e1c9e4d599210ceb1ebfad3065df43f4533c0fe4
tuned signature;

diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -103,7 +103,8 @@
       }
     }
 
-    override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
+    override val functions: Session.Protocol_Functions =
+      List(Markup.ML_Statistics.name -> ml_statistics)
   }
 
 
diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -106,11 +106,12 @@
   /* protocol handlers */
 
   type Protocol_Function = Prover.Protocol_Output => Boolean
+  type Protocol_Functions = List[(String, Protocol_Function)]
 
   abstract class Protocol_Handler extends Isabelle_System.Service {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
-    def functions: List[(String, Protocol_Function)] = Nil
+    def functions: Protocol_Functions = Nil
     def prover_options(options: Options): Options = options
   }
 }
diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/System/scala.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -235,7 +235,7 @@
       }
     }
 
-    override val functions =
+    override val functions: Session.Protocol_Functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -321,7 +321,7 @@
               case _ => false
             }
 
-          override val functions =
+          override val functions: Session.Protocol_Functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/Tools/debugger.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -133,7 +133,7 @@
       }
     }
 
-    override val functions =
+    override val functions: Session.Protocol_Functions =
       List(
         Markup.DEBUGGER_STATE -> debugger_state,
         Markup.DEBUGGER_OUTPUT -> debugger_output)
diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/Tools/print_operation.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -34,6 +34,7 @@
       true
     }
 
-    override val functions = List(Markup.PRINT_OPERATIONS -> put)
+    override val functions: Session.Protocol_Functions =
+      List(Markup.PRINT_OPERATIONS -> put)
   }
 }
diff -r e1c9e4d59921 -r 39011d0d2128 src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Sat Apr 09 15:40:29 2022 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Thu Apr 21 10:03:38 2022 +0200
@@ -313,6 +313,7 @@
           false
       }
 
-    override val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel)
+    override val functions: Session.Protocol_Functions =
+      List(Markup.SIMP_TRACE_CANCEL -> cancel)
   }
 }