# HG changeset patch
# User wenzelm
# Date 1459714540 -7200
# Node ID 85024c0e953df333d442a45b61c2489287d17e71
# Parent  4141c2a8458b5c7285afebbb98995baf1396777c
support for internal tools;

diff -r 4141c2a8458b -r 85024c0e953d src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 21:32:57 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:15:40 2016 +0200
@@ -23,41 +23,62 @@
     catch { case _: SecurityException => false }
   }
 
-  private def run_external(dir: Path, name: String)(args: List[String]): Nothing =
+  private def list_external(): List[(String, String)] =
   {
-    val tool = dir + Path.basic(name)
-    val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
-    sys.exit(result.print_stdout.rc)
+    val Description = """.*\bDESCRIPTION: *(.*)""".r
+    for {
+      dir <- dirs() if dir.is_dir
+      name <- File.read_dir(dir) if is_external(dir, name)
+    } yield {
+      val source = File.read(dir + Path.basic(name))
+      val description =
+        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
+      (name, description)
+    }
   }
 
   private def find_external(name: String): Option[List[String] => Unit] =
-    dirs.collectFirst({ case dir if is_external(dir, name) => run_external(dir, name) })
+    dirs.collectFirst({ case dir if is_external(dir, name) =>
+      (args: List[String]) =>
+        {
+          val tool = dir + Path.basic(name)
+          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
+          sys.exit(result.print_stdout.rc)
+        }
+    })
+
+
+  /* internal tools */
+
+  private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
+
+  private def list_internal(): List[(String, String)] =
+    synchronized {
+      for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
+    }
+
+  private def find_internal(name: String): Option[List[String] => Unit] =
+    synchronized { internal_tools.get(name).map(_._2) }
+
+  private def register(isabelle_tool: Isabelle_Tool): Unit =
+    synchronized {
+      internal_tools +=
+        (isabelle_tool.name ->
+          (isabelle_tool.description,
+            args => Command_Line.tool0 { isabelle_tool.body(args) }))
+    }
 
 
   /* command line entry point */
 
-  private def tool_descriptions(): List[String] =
-  {
-    val Description = """.*\bDESCRIPTION: *(.*)""".r
-    val entries =
-      for {
-        dir <- dirs() if dir.is_dir
-        name <- File.read_dir(dir) if is_external(dir, name)
-      } yield {
-        val source = File.read(dir + Path.basic(name))
-        split_lines(source).collectFirst({ case Description(s) => s }) match {
-          case None => (name, "")
-          case Some(description) => (name, " - " + description)
-        }
-      }
-    entries.sortBy(_._1).map({ case (a, b) => a + b })
-  }
-
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       args.toList match {
         case Nil | List("-?") =>
+          val tool_descriptions =
+            (list_external() ::: list_internal()).sortBy(_._1).
+              map({ case (a, "") => a case (a, b) => a + " - " + b })
           Getopts("""
 Usage: isabelle TOOL [ARGS ...]
 
@@ -65,11 +86,13 @@
 
 Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
         case tool_name :: tool_args =>
-          find_external(tool_name) match {
-            case Some(run) => run(tool_args)
+          find_external(tool_name) orElse find_internal(tool_name) match {
+            case Some(tool) => tool(tool_args)
             case None => error("Unknown Isabelle tool: " + quote(tool_name))
           }
       }
     }
   }
 }
+
+sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)