src/Pure/System/isabelle_tool.scala
author wenzelm
Sun Apr 03 22:54:31 2016 +0200 (2016-04-03)
changeset 62835 1a9ce1b13b20
parent 62834 970cedec9748
child 62836 98dbed6cfa44
permissions -rw-r--r--
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
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@62833
    71
  register(Build.isabelle_tool)
wenzelm@62834
    72
  register(Check_Sources.isabelle_tool)
wenzelm@62831
    73
  register(Doc.isabelle_tool)
wenzelm@62835
    74
  register(ML_Process.isabelle_tool)
wenzelm@62832
    75
  register(Options.isabelle_tool)
wenzelm@62831
    76
wenzelm@62829
    77
wenzelm@62829
    78
  /* command line entry point */
wenzelm@62829
    79
wenzelm@62829
    80
  def main(args: Array[String])
wenzelm@62829
    81
  {
wenzelm@62829
    82
    Command_Line.tool0 {
wenzelm@62829
    83
      args.toList match {
wenzelm@62829
    84
        case Nil | List("-?") =>
wenzelm@62830
    85
          val tool_descriptions =
wenzelm@62830
    86
            (list_external() ::: list_internal()).sortBy(_._1).
wenzelm@62830
    87
              map({ case (a, "") => a case (a, b) => a + " - " + b })
wenzelm@62829
    88
          Getopts("""
wenzelm@62829
    89
Usage: isabelle TOOL [ARGS ...]
wenzelm@62829
    90
wenzelm@62829
    91
  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
wenzelm@62829
    92
wenzelm@62829
    93
Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
wenzelm@62829
    94
        case tool_name :: tool_args =>
wenzelm@62830
    95
          find_external(tool_name) orElse find_internal(tool_name) match {
wenzelm@62830
    96
            case Some(tool) => tool(tool_args)
wenzelm@62829
    97
            case None => error("Unknown Isabelle tool: " + quote(tool_name))
wenzelm@62829
    98
          }
wenzelm@62829
    99
      }
wenzelm@62829
   100
    }
wenzelm@62829
   101
  }
wenzelm@62829
   102
}
wenzelm@62830
   103
wenzelm@62830
   104
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)