diff --git a/etc/build.props b/etc/build.props
new file mode 100644
--- /dev/null
+++ b/etc/build.props
@@ -0,0 +1,9 @@
+title = AFP/Tools
+module = $ISABELLE_HOME/lib/classes/afp_tools.jar
+requirements = \
+  env:ISABELLE_SCALA_JAR
+sources = \
+  tools/afp_check_roots.scala \
+  tools/afp_dependencies.scala \
+  tools/afp_tool.scala
+services = afp.Tools
diff --git a/etc/settings b/etc/settings
--- a/etc/settings
+++ b/etc/settings
@@ -1,11 +1,11 @@
 # -*- shell-script -*- :mode=shellscript:
 
 AFP_BASE="$COMPONENT"
 AFP="$AFP_BASE/thys"
 
 isabelle_directory '$AFP_BASE'
 isabelle_directory '$AFP'
 
 AFP_BUILD_OPTIONS='-v -o browser_info -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"'
 
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$AFP_BASE/tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$AFP_BASE/tools/lib"
diff --git a/tools/afp_check_roots.scala b/tools/afp_check_roots.scala
--- a/tools/afp_check_roots.scala
+++ b/tools/afp_check_roots.scala
@@ -1,134 +1,171 @@
-// DESCRIPTION: check ROOT files of AFP sessions
-
-object AFP_Check_Roots extends isabelle.Isabelle_Tool.Body {
+package afp
 
-  import isabelle._
 
-  val afp_dir = Path.explode("$AFP").expand
-  val excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc")
+import isabelle._
 
+
+object AFP_Check_Roots
+{
   def print_good(string: String): Unit =
     println(Console.BOLD + Console.GREEN + string + Console.RESET)
 
   def print_bad(string: String): Unit =
     println(Console.BOLD + Console.RED + string + Console.RESET)
 
   class Check[T](
     run: (Sessions.Structure, List[String]) => List[T],
     failure_msg: String,
     failure_format: T => String)
   {
     def apply(tree: Sessions.Structure, selected: List[String]): Boolean =
       run(tree, selected) match {
         case Nil =>
           true
         case offenders =>
           print_bad(failure_msg)
           offenders.foreach(offender => println("  " + failure_format(offender)))
           false
       }
   }
 
-  val check_timeout = new Check[(String, List[String])](
-    run = { (tree, selected) =>
-      selected.flatMap { name =>
-        val info = tree(name)
-        val entry = info.dir.base.implode
-        val timeout = info.options.real("timeout")
-        if (timeout == 0 || timeout % 300 != 0)
-          Some((entry, name))
-        else
-          None
-      }.groupBy(_._1).view.mapValues(_.map(_._2)).toList
-    },
-    failure_msg = "The following entries contain sessions without timeouts or with timeouts not divisible by 300:",
-    failure_format = { case (entry, sessions) => s"""$entry ${sessions.mkString("(", ", ", ")")}""" }
-  )
-
-  val check_paths = new Check[(String, Path)](
-    run = { (tree, selected) =>
-      selected.flatMap { name =>
-        val info = tree(name)
-        val dir = info.dir
-        if (dir.dir.expand.file != afp_dir.file)
-          Some((name, dir))
-        else
-          None
+  def afp_checks(afp_dir: Path, excludes: List[String]): List[Check[_]] =
+  {
+    val check_timeout = new Check[(String, List[String])](
+      run = { (tree, selected) =>
+        selected.flatMap { name =>
+          val info = tree(name)
+          val entry = info.dir.base.implode
+          val timeout = info.options.real("timeout")
+          if (timeout == 0 || timeout % 300 != 0)
+            Some((entry, name))
+          else
+            None
+        }.groupBy(_._1).view.mapValues(_.map(_._2)).toList
+      },
+      failure_msg = "The following entries contain sessions without timeouts or with timeouts not divisible by 300:",
+      failure_format = {
+        case (entry, sessions) => s"""$entry ${sessions.mkString("(", ", ", ")")}"""
       }
-    },
-    failure_msg = "The following sessions are in the wrong directory:",
-    failure_format = { case (session, dir) => s"""$session ($dir)""" }
-  )
+    )
 
-  val check_chapter = new Check[String](
-    run = { (tree, selected) =>
-      selected.flatMap { name =>
-        val info = tree(name)
-        val entry = info.dir.base.implode
-        if (info.chapter != "AFP")
-          Some(entry)
-        else
-          None
-      }.distinct
-    },
-    failure_msg = "The following entries are not in the AFP chapter:",
-    failure_format = identity
-  )
-
-  val check_groups = new Check[(String, List[String])](
-    run = { (tree, selected) =>
-      selected.flatMap { name =>
-        val info = tree(name)
-        if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") ||
-            !info.groups.contains("AFP"))
-          Some((name, info.groups))
-        else
-          None
+    val check_paths = new Check[(String, Path)](
+      run = { (tree, selected) =>
+        selected.flatMap { name =>
+          val info = tree(name)
+          val dir = info.dir
+          if (dir.dir.expand.file != afp_dir.file)
+            Some((name, dir))
+          else
+            None
+        }
+      },
+      failure_msg = "The following sessions are in the wrong directory:",
+      failure_format = {
+        case (session, dir) => s"""$session ($dir)"""
       }
-    },
-    failure_msg = "The following sessions have wrong groups:",
-    failure_format = { case (session, groups) => s"""$session ${groups.mkString("{", ", ", "}")}""" }
-  )
-
-  val check_presence = new Check[String](
-    run = { (tree, selected) =>
-      val fs_entries = File.read_dir(afp_dir).filterNot(excludes.contains)
+    )
 
-      fs_entries.flatMap { name =>
-        if (!selected.contains(name) || tree(name).dir.base.implode != name)
-          Some(name)
-        else
-          None
+    val check_chapter = new Check[String](
+      run = { (tree, selected) =>
+        selected.flatMap { name =>
+          val info = tree(name)
+          val entry = info.dir.base.implode
+          if (info.chapter != "AFP")
+            Some(entry)
+          else
+            None
+        }.distinct
+      },
+      failure_msg = "The following entries are not in the AFP chapter:",
+      failure_format = identity
+    )
+
+    val check_groups = new Check[(String, List[String])](
+      run = { (tree, selected) =>
+        selected.flatMap { name =>
+          val info = tree(name)
+          if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") ||
+            !info.groups.contains("AFP"))
+            Some((name, info.groups))
+          else
+            None
+        }
+      },
+      failure_msg = "The following sessions have wrong groups:",
+      failure_format = {
+        case (session, groups) => s"""$session ${groups.mkString("{", ", ", "}")}"""
       }
-    },
-    failure_msg = "The following entries (according to the file system) are not registered in ROOTS, or registered in the wrong ROOT:",
-    failure_format = identity
-  )
+    )
 
-  def apply(args: List[String]): Unit =
-  {
-    val full_tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
-    val selected = full_tree.build_selection(Sessions.Selection.empty)
+    val check_presence = new Check[String](
+      run = { (tree, selected) =>
+        val fs_entries = File.read_dir(afp_dir).filterNot(excludes.contains)
 
-    val checks = List(
+        fs_entries.flatMap { name =>
+          if (!selected.contains(name) || tree(name).dir.base.implode != name)
+            Some(name)
+          else
+            None
+        }
+      },
+      failure_msg = "The following entries (according to the file system) are not registered in ROOTS, or registered in the wrong ROOT:",
+      failure_format = identity
+    )
+
+    List(
       check_timeout,
       // check_paths,
       check_chapter,
       check_groups,
       check_presence)
+  }
+
+  def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit =
+  {
+    val full_tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
+    val selected = full_tree.build_selection(Sessions.Selection.empty)
+    val checks = afp_checks(afp_dir, excludes)
 
     val bad = checks.exists(check => !check(full_tree, selected))
 
     if (bad)
     {
       print_bad("Errors found.")
       System.exit(1)
     }
     else
     {
       print_good(s"${selected.length} sessions have been checked")
       print_good(s"${checks.length} checks have found no errors")
     }
   }
 
+  val isabelle_tool =
+    Isabelle_Tool(
+      "afp_check_roots",
+      "check ROOT files of AFP sessions",
+      Scala_Project.here,
+      args => {
+        var excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc")
+
+        val getopts = Getopts(
+          """
+Usage: isabelle afp_check_roots [OPTIONS]
+
+  Options are:
+    -x NAME      exclude directories with name
+                 (default """ + excludes.map(quote).mkString(", ") + """)
+
+  Check ROOT files of AFP sessions.
+""",
+          "x:" -> (arg => excludes ::= arg)
+        )
+
+        getopts(args)
+
+        val afp_dir = Path.explode("$AFP").expand
+
+        afp_check_roots(afp_dir, excludes)
+      }
+    )
 }
diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala
--- a/tools/afp_dependencies.scala
+++ b/tools/afp_dependencies.scala
@@ -1,44 +1,78 @@
-// DESCRIPTION: extract dependencies between AFP entries
-
-object AFP_Dependencies extends isabelle.Isabelle_Tool.Body {
-
-  import isabelle._
-
-  val afp_dir = Path.explode("$AFP").expand
-
-  val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
-  val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil)).build_graph.keys
+package afp
 
-  def get_entry(name: String): Option[String] =
-  {
-    val info = tree(name)
-    val dir = info.dir
 
-    if (dir.dir.expand.file != afp_dir.file)
-      None
-    else
-      Some(dir.base.implode)
-  }
+import isabelle._
 
+
+object AFP_Dependencies
+{
   def as_json(entry: String, distrib_deps: List[String], afp_deps: List[String]): String =
     s"""
       {"$entry":
         {"distrib_deps": [${commas_quote(distrib_deps)}],
          "afp_deps": [${commas_quote(afp_deps)}]
         }
       }"""
 
-  def apply(args: List[String]): Unit =
+  def afp_dependencies(afp_dir: Path): String =
   {
+    val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
+    val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil))
+      .build_graph.keys
+
+    def get_entry(name: String): Option[String] =
+    {
+      val info = tree(name)
+      val dir = info.dir
+
+      if (selected.contains(dir.dir.expand))
+        None
+      else
+        Some(dir.base.implode)
+    }
+
     val result = selected.groupBy(get_entry).collect {
       case (Some(e), sessions) =>
-        val dependencies = sessions.flatMap(tree.imports_graph.imm_preds).map(d => (d, get_entry(d)))
+        val dependencies = sessions.flatMap(tree.imports_graph.imm_preds)
+          .map(d => (d, get_entry(d)))
         val distrib_deps = dependencies.collect { case (d, None) => d }.distinct
         val afp_deps = dependencies.collect { case (_, Some(d)) if d != e => d }.distinct
         as_json(e, distrib_deps, afp_deps)
     }
 
-    println("[" + commas(result) + "]")
+    "[" + commas(result) + "]"
   }
 
+  val isabelle_tool =
+    Isabelle_Tool(
+      "afp_dependencies",
+      "extract dependencies between AFP entries",
+      Scala_Project.here,
+      args => {
+        var output_file: Option[Path] = None
+
+        val getopts = Getopts(
+          """
+Usage: isabelle afp_dependencies [OPTIONS]
+
+  Options are:
+    -o FILE      output file name
+
+  Extract dependencies between AFP entries.
+""",
+          "o:" -> (arg => output_file = Some(Path.explode(arg)))
+        )
+
+        getopts(args)
+        val afp_dir = Path.explode("$AFP").expand
+
+        val progress = new Console_Progress()
+
+        val res = afp_dependencies(afp_dir)
+        output_file match {
+          case Some(file) => File.write(file, res)
+          case None => progress.echo(res)
+        }
+      }
+    )
 }
diff --git a/tools/afp_tool.scala b/tools/afp_tool.scala
new file mode 100644
--- /dev/null
+++ b/tools/afp_tool.scala
@@ -0,0 +1,10 @@
+package afp
+
+
+import isabelle.Isabelle_Scala_Tools
+
+
+class Tools extends Isabelle_Scala_Tools(
+  AFP_Check_Roots.isabelle_tool,
+  AFP_Dependencies.isabelle_tool,
+)
diff --git a/tools/afp_build b/tools/lib/afp_build
rename from tools/afp_build
rename to tools/lib/afp_build
diff --git a/tools/afp_churn_pie b/tools/lib/afp_churn_pie
rename from tools/afp_churn_pie
rename to tools/lib/afp_churn_pie