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