src/Pure/System/isabelle_tool.scala
author wenzelm
Sun Apr 03 22:15:40 2016 +0200 (2016-04-03)
changeset 62830 85024c0e953d
parent 62829 4141c2a8458b
child 62831 5560905a32ae
permissions -rw-r--r--
support for internal tools;
wenzelm@62829
     1
/*  Title:      Pure/System/isabelle_tool.scala
wenzelm@62829
     2
    Author:     Makarius
wenzelm@62829
     3
wenzelm@62829
     4
Isabelle system tools: external executables or internal Scala functions.
wenzelm@62829
     5
*/
wenzelm@62829
     6
wenzelm@62829
     7
package isabelle
wenzelm@62829
     8
wenzelm@62829
     9
wenzelm@62829
    10
object Isabelle_Tool
wenzelm@62829
    11
{
wenzelm@62829
    12
  /* external tools */
wenzelm@62829
    13
wenzelm@62829
    14
  private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
wenzelm@62829
    15
wenzelm@62829
    16
  private def is_external(dir: Path, name: String): Boolean =
wenzelm@62829
    17
  {
wenzelm@62829
    18
    val file = (dir + Path.basic(name)).file
wenzelm@62829
    19
    try {
wenzelm@62829
    20
      file.isFile && file.canRead && file.canExecute &&
wenzelm@62829
    21
        !name.endsWith("~") && !name.endsWith(".orig")
wenzelm@62829
    22
    }
wenzelm@62829
    23
    catch { case _: SecurityException => false }
wenzelm@62829
    24
  }
wenzelm@62829
    25
wenzelm@62830
    26
  private def list_external(): List[(String, String)] =
wenzelm@62829
    27
  {
wenzelm@62830
    28
    val Description = """.*\bDESCRIPTION: *(.*)""".r
wenzelm@62830
    29
    for {
wenzelm@62830
    30
      dir <- dirs() if dir.is_dir
wenzelm@62830
    31
      name <- File.read_dir(dir) if is_external(dir, name)
wenzelm@62830
    32
    } yield {
wenzelm@62830
    33
      val source = File.read(dir + Path.basic(name))
wenzelm@62830
    34
      val description =
wenzelm@62830
    35
        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
wenzelm@62830
    36
      (name, description)
wenzelm@62830
    37
    }
wenzelm@62829
    38
  }
wenzelm@62829
    39
wenzelm@62829
    40
  private def find_external(name: String): Option[List[String] => Unit] =
wenzelm@62830
    41
    dirs.collectFirst({ case dir if is_external(dir, name) =>
wenzelm@62830
    42
      (args: List[String]) =>
wenzelm@62830
    43
        {
wenzelm@62830
    44
          val tool = dir + Path.basic(name)
wenzelm@62830
    45
          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
wenzelm@62830
    46
          sys.exit(result.print_stdout.rc)
wenzelm@62830
    47
        }
wenzelm@62830
    48
    })
wenzelm@62830
    49
wenzelm@62830
    50
wenzelm@62830
    51
  /* internal tools */
wenzelm@62830
    52
wenzelm@62830
    53
  private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
wenzelm@62830
    54
wenzelm@62830
    55
  private def list_internal(): List[(String, String)] =
wenzelm@62830
    56
    synchronized {
wenzelm@62830
    57
      for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
wenzelm@62830
    58
    }
wenzelm@62830
    59
wenzelm@62830
    60
  private def find_internal(name: String): Option[List[String] => Unit] =
wenzelm@62830
    61
    synchronized { internal_tools.get(name).map(_._2) }
wenzelm@62830
    62
wenzelm@62830
    63
  private def register(isabelle_tool: Isabelle_Tool): Unit =
wenzelm@62830
    64
    synchronized {
wenzelm@62830
    65
      internal_tools +=
wenzelm@62830
    66
        (isabelle_tool.name ->
wenzelm@62830
    67
          (isabelle_tool.description,
wenzelm@62830
    68
            args => Command_Line.tool0 { isabelle_tool.body(args) }))
wenzelm@62830
    69
    }
wenzelm@62829
    70
wenzelm@62829
    71
wenzelm@62829
    72
  /* command line entry point */
wenzelm@62829
    73
wenzelm@62829
    74
  def main(args: Array[String])
wenzelm@62829
    75
  {
wenzelm@62829
    76
    Command_Line.tool0 {
wenzelm@62829
    77
      args.toList match {
wenzelm@62829
    78
        case Nil | List("-?") =>
wenzelm@62830
    79
          val tool_descriptions =
wenzelm@62830
    80
            (list_external() ::: list_internal()).sortBy(_._1).
wenzelm@62830
    81
              map({ case (a, "") => a case (a, b) => a + " - " + b })
wenzelm@62829
    82
          Getopts("""
wenzelm@62829
    83
Usage: isabelle TOOL [ARGS ...]
wenzelm@62829
    84
wenzelm@62829
    85
  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
wenzelm@62829
    86
wenzelm@62829
    87
Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
wenzelm@62829
    88
        case tool_name :: tool_args =>
wenzelm@62830
    89
          find_external(tool_name) orElse find_internal(tool_name) match {
wenzelm@62830
    90
            case Some(tool) => tool(tool_args)
wenzelm@62829
    91
            case None => error("Unknown Isabelle tool: " + quote(tool_name))
wenzelm@62829
    92
          }
wenzelm@62829
    93
      }
wenzelm@62829
    94
    }
wenzelm@62829
    95
  }
wenzelm@62829
    96
}
wenzelm@62830
    97
wenzelm@62830
    98
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)