src/Pure/Tools/dump.scala
changeset 73340 0ffcad1f6130
parent 72869 015a61936c13
child 73359 d8a0e996614b
--- a/src/Pure/Tools/dump.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -138,7 +138,7 @@
 
     def session_dirs: List[Path] = dirs ::: select_dirs
 
-    def build_logic(logic: String)
+    def build_logic(logic: String): Unit =
     {
       Build.build_logic(options, logic, build_heap = true, progress = progress,
         dirs = session_dirs, strict = true)
@@ -226,12 +226,12 @@
 
     private val errors = Synchronized(List.empty[String])
 
-    def add_errors(more_errs: List[String])
+    def add_errors(more_errs: List[String]): Unit =
     {
       errors.change(errs => errs ::: more_errs)
     }
 
-    def check_errors
+    def check_errors: Unit =
     {
       val errs = errors.value
       if (errs.nonEmpty) error(errs.mkString("\n\n"))
@@ -289,7 +289,7 @@
 
     /* process */
 
-    def process(process_theory: Args => Unit, unicode_symbols: Boolean = false)
+    def process(process_theory: Args => Unit, unicode_symbols: Boolean = false): Unit =
     {
       val session = resources.start_session(progress = progress)
 
@@ -394,7 +394,7 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
-    selection: Sessions.Selection = Sessions.Selection.empty)
+    selection: Sessions.Selection = Sessions.Selection.empty): Unit =
   {
     val context =
       Context(options, aspects = aspects, progress = progress, dirs = dirs,