src/Pure/System/isabelle_tool.scala
author wenzelm
Thu, 04 Mar 2021 22:01:53 +0100
changeset 73616 ffdb22a155b4
parent 73614 77ef8bef0593
child 73651 48569c862eb8
permissions -rw-r--r--
tuned --- avoid compiler warnings;
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
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
     3
    Author:     Lars Hupel
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
     4
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
     5
Isabelle system tools: external executables or internal Scala functions.
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
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
     8
package isabelle
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
     9
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    10
import java.net.URLClassLoader
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    11
import scala.reflect.runtime.universe
73000
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
    12
import scala.tools.reflect.{ToolBox, ToolBoxError}
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    13
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    14
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    15
object Isabelle_Tool
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    16
{
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    17
  /* Scala source tools */
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    18
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    19
  abstract class Body extends Function[List[String], Unit]
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    20
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    21
  private def compile(path: Path): Body =
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    22
  {
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    23
    def err(msg: String): Nothing =
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    24
      cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    25
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    26
    val source = File.read(path)
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    27
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    28
    val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    29
    val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    30
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    31
    try {
73616
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    32
      val tree = tool_box.parse(source)
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    33
      val module =
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    34
        try { tree.asInstanceOf[universe.ModuleDef] }
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    35
        catch {
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    36
          case _: java.lang.ClassCastException =>
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    37
            err("Source does not describe a module (Scala object)")
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    38
        }
ffdb22a155b4 tuned --- avoid compiler warnings;
wenzelm
parents: 73614
diff changeset
    39
      tool_box.compile(universe.Ident(tool_box.define(module)))() match {
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    40
        case body: Body => body
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    41
        case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    42
      }
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    43
    }
63519
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    44
    catch {
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    45
      case e: ToolBoxError =>
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    46
        if (tool_box.frontEnd.hasErrors) {
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    47
          val infos = tool_box.frontEnd.infos.toList
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    48
          val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    49
          err(msgs.mkString("\n"))
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    50
        }
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    51
        else
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    52
          err(e.toString)
78401d628718 more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents: 63226
diff changeset
    53
    }
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    54
  }
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    55
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    56
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    57
  /* external tools */
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    58
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    59
  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
    60
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    61
  private def is_external(dir: Path, file_name: String): Boolean =
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    62
  {
65450
b0a73039ddaa more robust: user could provide name with "/" etc.;
wenzelm
parents: 65138
diff changeset
    63
    val file = (dir + Path.explode(file_name)).file
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    64
    try {
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    65
      file.isFile && file.canRead &&
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    66
        (file_name.endsWith(".scala") || file.canExecute) &&
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    67
        !file_name.endsWith("~") && !file_name.endsWith(".orig")
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    68
    }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    69
    catch { case _: SecurityException => false }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    70
  }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    71
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    72
  private def find_external(name: String): Option[List[String] => Unit] =
71592
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 71587
diff changeset
    73
    dirs().collectFirst({
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    74
      case dir if is_external(dir, name + ".scala") =>
65450
b0a73039ddaa more robust: user could provide name with "/" etc.;
wenzelm
parents: 65138
diff changeset
    75
        compile(dir + Path.explode(name + ".scala"))
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    76
      case dir if is_external(dir, name) =>
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    77
        (args: List[String]) =>
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    78
          {
65450
b0a73039ddaa more robust: user could provide name with "/" etc.;
wenzelm
parents: 65138
diff changeset
    79
            val tool = dir + Path.explode(name)
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64161
diff changeset
    80
            val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
63226
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    81
            sys.exit(result.print_stdout.rc)
d8884c111bca support for .scala tools;
wenzelm
parents: 62960
diff changeset
    82
          }
62830
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    83
    })
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    84
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    85
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    86
  /* internal tools */
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    87
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
    88
  private lazy val internal_tools: List[Isabelle_Tool] =
72389
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72024
diff changeset
    89
    Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools)
62830
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    90
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
    91
  private def find_internal(name: String): Option[List[String] => Unit] =
62960
cfbb6a5b427c simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents: 62838
diff changeset
    92
    internal_tools.collectFirst({
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
    93
      case tool if tool.name == name =>
71848
c1bc38327bc2 clarified signature;
wenzelm
parents: 71592
diff changeset
    94
        args => Command_Line.tool { tool.body(args) }
62960
cfbb6a5b427c simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents: 62838
diff changeset
    95
      })
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62830
diff changeset
    96
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
    97
73000
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
    98
  /* list tools */
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
    99
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   100
  abstract class Entry
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   101
  {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   102
    def name: String
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   103
    def position: Properties.T
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   104
    def description: String
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   105
    def print: String =
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   106
      description match {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   107
        case "" => name
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   108
        case descr => name + " - " + descr
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   109
      }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   110
  }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   111
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   112
  sealed case class External(name: String, path: Path) extends Entry
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   113
  {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   114
    def position: Properties.T = Position.File(path.absolute.implode)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   115
    def description: String =
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   116
    {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   117
      val Pattern = """.*\bDESCRIPTION: *(.*)""".r
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   118
      split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse ""
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   119
    }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   120
  }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   121
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   122
  def external_tools(): List[External] =
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   123
  {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   124
    for {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   125
      dir <- dirs() if dir.is_dir
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   126
      file_name <- File.read_dir(dir) if is_external(dir, file_name)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   127
    } yield {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   128
      val path = dir + Path.explode(file_name)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   129
      val name = Library.perhaps_unsuffix(".scala", file_name)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   130
      External(name, path)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   131
    }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   132
  }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   133
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   134
  def isabelle_tools(): List[Entry] =
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   135
    (external_tools() ::: internal_tools).sortBy(_.name)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   136
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   137
  object Isabelle_Tools extends Scala.Fun("isabelle_tools")
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   138
  {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   139
    val here = Scala_Project.here
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   140
    def apply(arg: String): String =
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   141
      if (arg.nonEmpty) error("Bad argument: " + quote(arg))
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   142
      else {
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   143
        val result = isabelle_tools().map(entry => (entry.name, entry.position))
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   144
        val body = { import XML.Encode._; list(pair(string, properties))(result) }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   145
        YXML.string_of_body(body)
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   146
      }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   147
  }
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   148
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   149
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   150
  /* command line entry point */
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   151
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73123
diff changeset
   152
  def main(args: Array[String]): Unit =
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   153
  {
71848
c1bc38327bc2 clarified signature;
wenzelm
parents: 71592
diff changeset
   154
    Command_Line.tool {
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   155
      args.toList match {
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   156
        case Nil | List("-?") =>
73000
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   157
          val tool_descriptions = isabelle_tools().map(_.print)
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   158
          Getopts("""
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   159
Usage: isabelle TOOL [ARGS ...]
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   160
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   161
  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
   162
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   163
Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage()
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   164
        case tool_name :: tool_args =>
62830
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
   165
          find_external(tool_name) orElse find_internal(tool_name) match {
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
   166
            case Some(tool) => tool(tool_args)
62829
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   167
            case None => error("Unknown Isabelle tool: " + quote(tool_name))
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   168
          }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   169
      }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   170
    }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   171
  }
4141c2a8458b clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff changeset
   172
}
62830
85024c0e953d support for internal tools;
wenzelm
parents: 62829
diff changeset
   173
73000
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   174
sealed case class Isabelle_Tool(
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   175
  name: String,
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   176
  description: String,
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   177
  here: Scala_Project.Here,
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   178
  body: List[String] => Unit) extends Isabelle_Tool.Entry
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   179
{
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   180
  def position: Position.T = here.position
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72998
diff changeset
   181
}
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   182
71952
a2afc7ed2c68 another isabelle_scala_service;
wenzelm
parents: 71848
diff changeset
   183
class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   184
69989
a23d6ff31f79 clarified name;
wenzelm
parents: 69571
diff changeset
   185
class Tools extends Isabelle_Scala_Tools(
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   186
  Build.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   187
  Build_Docker.isabelle_tool,
73095
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 73004
diff changeset
   188
  Build_Job.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   189
  Doc.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   190
  Dump.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   191
  Export.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   192
  ML_Process.isabelle_tool,
71521
937328d61436 added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents: 71308
diff changeset
   193
  Mercurial.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   194
  Mkroot.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   195
  Options.isabelle_tool,
71164
79736ffe77c3 some support for Phabricator server;
wenzelm
parents: 70876
diff changeset
   196
  Phabricator.isabelle_tool1,
79736ffe77c3 some support for Phabricator server;
wenzelm
parents: 70876
diff changeset
   197
  Phabricator.isabelle_tool2,
71296
d3ededaa77b3 added "isabelle phabricator";
wenzelm
parents: 71164
diff changeset
   198
  Phabricator.isabelle_tool3,
71308
8c1c717a830b configure SSH hosting via "isabelle phabricator_setup_ssh";
wenzelm
parents: 71296
diff changeset
   199
  Phabricator.isabelle_tool4,
72888
07edf1952ab1 clarified modules;
wenzelm
parents: 72699
diff changeset
   200
  Presentation.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   201
  Profiling_Report.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   202
  Server.isabelle_tool,
72024
e2ad50885887 added "isabelle sessions" tool;
wenzelm
parents: 71956
diff changeset
   203
  Sessions.isabelle_tool,
71587
820cf124dced added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents: 71521
diff changeset
   204
  Scala_Project.isabelle_tool,
69571
e72360fef69a update theory sources based on PIDE markup;
wenzelm
parents: 69439
diff changeset
   205
  Update.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   206
  Update_Cartouches.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   207
  Update_Comments.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   208
  Update_Header.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   209
  Update_Then.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   210
  Update_Theorems.isabelle_tool,
73004
f6bf65554764 clarified files;
wenzelm
parents: 73000
diff changeset
   211
  isabelle.vscode.TextMate_Grammar.isabelle_tool,
72998
4519eeefe3b5 avoid conflicting base names;
wenzelm
parents: 72888
diff changeset
   212
  isabelle.vscode.Language_Server.isabelle_tool)
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   213
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   214
class Admin_Tools extends Isabelle_Scala_Tools(
72647
af24c0dd6975 build Isabelle CSDP component from official downloads;
wenzelm
parents: 72644
diff changeset
   215
  Build_CSDP.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   216
  Build_Cygwin.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   217
  Build_Doc.isabelle_tool,
72596
fc5f10691147 build Isabelle E prover component from official downloads;
wenzelm
parents: 72579
diff changeset
   218
  Build_E.isabelle_tool,
69349
6baa37cbf70b clarified module name (again);
wenzelm
parents: 69347
diff changeset
   219
  Build_Fonts.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   220
  Build_JDK.isabelle_tool,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   221
  Build_PolyML.isabelle_tool1,
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   222
  Build_PolyML.isabelle_tool2,
72644
b8cc129ece05 build Isabelle SPASS component from unofficial download;
wenzelm
parents: 72596
diff changeset
   223
  Build_SPASS.isabelle_tool,
72579
93e533198bf6 build Isabelle sqlite-jdbc component from official download;
wenzelm
parents: 72389
diff changeset
   224
  Build_SQLite.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   225
  Build_Status.isabelle_tool,
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents: 73095
diff changeset
   226
  Build_Vampire.isabelle_tool,
72672
7f6800b2e8c2 build Isabelle veriT component from official download;
wenzelm
parents: 72647
diff changeset
   227
  Build_VeriT.isabelle_tool,
72699
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents: 72672
diff changeset
   228
  Build_Zipperposition.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   229
  Check_Sources.isabelle_tool,
69439
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 69411
diff changeset
   230
  Components.isabelle_tool,
69282
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 69169
diff changeset
   231
  isabelle.vscode.Build_VSCode.isabelle_tool)