src/Pure/System/isabelle_tool.scala
changeset 62830 85024c0e953d
parent 62829 4141c2a8458b
child 62831 5560905a32ae
     1.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 21:32:57 2016 +0200
     1.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:15:40 2016 +0200
     1.3 @@ -23,41 +23,62 @@
     1.4      catch { case _: SecurityException => false }
     1.5    }
     1.6  
     1.7 -  private def run_external(dir: Path, name: String)(args: List[String]): Nothing =
     1.8 +  private def list_external(): List[(String, String)] =
     1.9    {
    1.10 -    val tool = dir + Path.basic(name)
    1.11 -    val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    1.12 -    sys.exit(result.print_stdout.rc)
    1.13 +    val Description = """.*\bDESCRIPTION: *(.*)""".r
    1.14 +    for {
    1.15 +      dir <- dirs() if dir.is_dir
    1.16 +      name <- File.read_dir(dir) if is_external(dir, name)
    1.17 +    } yield {
    1.18 +      val source = File.read(dir + Path.basic(name))
    1.19 +      val description =
    1.20 +        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
    1.21 +      (name, description)
    1.22 +    }
    1.23    }
    1.24  
    1.25    private def find_external(name: String): Option[List[String] => Unit] =
    1.26 -    dirs.collectFirst({ case dir if is_external(dir, name) => run_external(dir, name) })
    1.27 +    dirs.collectFirst({ case dir if is_external(dir, name) =>
    1.28 +      (args: List[String]) =>
    1.29 +        {
    1.30 +          val tool = dir + Path.basic(name)
    1.31 +          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    1.32 +          sys.exit(result.print_stdout.rc)
    1.33 +        }
    1.34 +    })
    1.35 +
    1.36 +
    1.37 +  /* internal tools */
    1.38 +
    1.39 +  private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
    1.40 +
    1.41 +  private def list_internal(): List[(String, String)] =
    1.42 +    synchronized {
    1.43 +      for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
    1.44 +    }
    1.45 +
    1.46 +  private def find_internal(name: String): Option[List[String] => Unit] =
    1.47 +    synchronized { internal_tools.get(name).map(_._2) }
    1.48 +
    1.49 +  private def register(isabelle_tool: Isabelle_Tool): Unit =
    1.50 +    synchronized {
    1.51 +      internal_tools +=
    1.52 +        (isabelle_tool.name ->
    1.53 +          (isabelle_tool.description,
    1.54 +            args => Command_Line.tool0 { isabelle_tool.body(args) }))
    1.55 +    }
    1.56  
    1.57  
    1.58    /* command line entry point */
    1.59  
    1.60 -  private def tool_descriptions(): List[String] =
    1.61 -  {
    1.62 -    val Description = """.*\bDESCRIPTION: *(.*)""".r
    1.63 -    val entries =
    1.64 -      for {
    1.65 -        dir <- dirs() if dir.is_dir
    1.66 -        name <- File.read_dir(dir) if is_external(dir, name)
    1.67 -      } yield {
    1.68 -        val source = File.read(dir + Path.basic(name))
    1.69 -        split_lines(source).collectFirst({ case Description(s) => s }) match {
    1.70 -          case None => (name, "")
    1.71 -          case Some(description) => (name, " - " + description)
    1.72 -        }
    1.73 -      }
    1.74 -    entries.sortBy(_._1).map({ case (a, b) => a + b })
    1.75 -  }
    1.76 -
    1.77    def main(args: Array[String])
    1.78    {
    1.79      Command_Line.tool0 {
    1.80        args.toList match {
    1.81          case Nil | List("-?") =>
    1.82 +          val tool_descriptions =
    1.83 +            (list_external() ::: list_internal()).sortBy(_._1).
    1.84 +              map({ case (a, "") => a case (a, b) => a + " - " + b })
    1.85            Getopts("""
    1.86  Usage: isabelle TOOL [ARGS ...]
    1.87  
    1.88 @@ -65,11 +86,13 @@
    1.89  
    1.90  Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
    1.91          case tool_name :: tool_args =>
    1.92 -          find_external(tool_name) match {
    1.93 -            case Some(run) => run(tool_args)
    1.94 +          find_external(tool_name) orElse find_internal(tool_name) match {
    1.95 +            case Some(tool) => tool(tool_args)
    1.96              case None => error("Unknown Isabelle tool: " + quote(tool_name))
    1.97            }
    1.98        }
    1.99      }
   1.100    }
   1.101  }
   1.102 +
   1.103 +sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)