# HG changeset patch
# User wenzelm
# Date 1598524450 -7200
# Node ID 53e8858b839fea2d249c0b9981aae67172461537
# Parent  a6cbf8ce979e5728c922a7f2a6f2c83a1e1a055a
clarified signature;

diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -117,7 +117,7 @@
       }
     }
 
-    val functions = List(Markup.ML_Statistics.name -> ml_statistics)
+    override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
   }
 
 
diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -117,7 +117,7 @@
   {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
-    val functions: List[(String, Protocol_Function)]
+    def functions: List[(String, Protocol_Function)] = Nil
   }
 }
 
diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/System/scala.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -211,7 +211,7 @@
       }
     }
 
-    val functions =
+    override val functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/Tools/build.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -308,7 +308,7 @@
                 if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
               } yield props1.filter(p => Markup.command_timing_properties(p._1))
 
-            val functions =
+            override val functions =
               List(
                 Markup.Build_Session_Finished.name -> build_session_finished,
                 Markup.Loading_Theory.name -> loading_theory,
diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/Tools/debugger.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -141,7 +141,7 @@
       }
     }
 
-    val functions =
+    override val functions =
       List(
         Markup.DEBUGGER_STATE -> debugger_state,
         Markup.DEBUGGER_OUTPUT -> debugger_output)
diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/Tools/print_operation.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -38,6 +38,6 @@
       true
     }
 
-    val functions = List(Markup.PRINT_OPERATIONS -> put)
+    override val functions = List(Markup.PRINT_OPERATIONS -> put)
   }
 }
diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -326,6 +326,6 @@
           false
       }
 
-    val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel)
+    override val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel)
   }
 }