added document antiquotation @{tool};
formal check of isabelle tools via Isabelle/Scala;
--- a/NEWS Sat Nov 28 20:18:29 2020 +0100
+++ b/NEWS Sat Nov 28 21:56:24 2020 +0100
@@ -45,6 +45,10 @@
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
document output is always PDF.
+* Antiquotation @{tool} refers to Isabelle command-line tools, with
+completion and formal reference to the source (external script or
+internal Scala function).
+
* Antiquotation @{bash_function} refers to GNU bash functions that are
checked within the Isabelle settings environment.
--- a/etc/symbols Sat Nov 28 20:18:29 2020 +0100
+++ b/etc/symbols Sat Nov 28 21:56:24 2020 +0100
@@ -432,6 +432,7 @@
\<^term> argument: cartouche
\<^theory> argument: cartouche
\<^theory_context> argument: cartouche
+\<^tool> argument: cartouche
\<^typ> argument: cartouche
\<^type_abbrev> argument: cartouche
\<^type_name> argument: cartouche
--- a/src/Doc/System/Base.thy Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Doc/System/Base.thy Sat Nov 28 21:56:24 2020 +0100
@@ -3,7 +3,7 @@
theory Base
imports Pure
begin
-
+
ML_file \<open>../antiquote_setup.ML\<close>
end
--- a/src/Doc/antiquote_setup.ML Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Doc/antiquote_setup.ML Sat Nov 28 21:56:24 2020 +0100
@@ -201,7 +201,7 @@
entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #>
- entity_antiqs no_check "isatool" \<^binding>\<open>tool\<close> #>
+ entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\<open>tool\<close> #>
entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #>
entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>);
--- a/src/Pure/Admin/build_csdp.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_csdp.scala Sat Nov 28 21:56:24 2020 +0100
@@ -171,7 +171,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_csdp", "build prover component from official download",
+ Isabelle_Tool("build_csdp", "build prover component from official download", Scala_Project.here,
args =>
{
var target_dir = Path.current
--- a/src/Pure/Admin/build_cygwin.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Sat Nov 28 21:56:24 2020 +0100
@@ -61,7 +61,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle", args =>
+ Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle",
+ Scala_Project.here, args =>
{
var mirror = default_mirror
var more_packages: List[String] = Nil
--- a/src/Pure/Admin/build_doc.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala Sat Nov 28 21:56:24 2020 +0100
@@ -72,7 +72,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
+ Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args =>
{
var all_docs = false
var max_jobs = 1
--- a/src/Pure/Admin/build_e.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_e.scala Sat Nov 28 21:56:24 2020 +0100
@@ -108,7 +108,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_e", "build prover component from source distribution",
+ Isabelle_Tool("build_e", "build prover component from source distribution", Scala_Project.here,
args =>
{
var target_dir = Path.current
--- a/src/Pure/Admin/build_fonts.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala Sat Nov 28 21:56:24 2020 +0100
@@ -335,7 +335,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_fonts", "construct Isabelle fonts", args =>
+ Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here, args =>
{
var source_dirs: List[Path] = Nil
--- a/src/Pure/Admin/build_jdk.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala Sat Nov 28 21:56:24 2020 +0100
@@ -214,7 +214,7 @@
val isabelle_tool =
Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
- args =>
+ Scala_Project.here, args =>
{
var target_dir = Path.current
--- a/src/Pure/Admin/build_polyml.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_polyml.scala Sat Nov 28 21:56:24 2020 +0100
@@ -204,7 +204,7 @@
/** Isabelle tool wrappers **/
val isabelle_tool1 =
- Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
+ Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here, args =>
{
var mingw = MinGW.none
var arch_64 = Isabelle_Platform.self.is_arm
@@ -242,7 +242,8 @@
})
val isabelle_tool2 =
- Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
+ Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component",
+ Scala_Project.here, args =>
{
var sha1_root: Option[Path] = None
--- a/src/Pure/Admin/build_spass.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_spass.scala Sat Nov 28 21:56:24 2020 +0100
@@ -147,7 +147,7 @@
val isabelle_tool =
Isabelle_Tool("build_spass", "build prover component from source distribution",
- args =>
+ Scala_Project.here, args =>
{
var target_dir = Path.current
var download_url = default_download_url
--- a/src/Pure/Admin/build_sqlite.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_sqlite.scala Sat Nov 28 21:56:24 2020 +0100
@@ -84,7 +84,7 @@
val isabelle_tool =
Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download",
- args =>
+ Scala_Project.here, args =>
{
var target_dir = Path.current
--- a/src/Pure/Admin/build_status.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Nov 28 21:56:24 2020 +0100
@@ -573,7 +573,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_status", "present recent build status information from database", args =>
+ Isabelle_Tool("build_status", "present recent build status information from database",
+ Scala_Project.here, args =>
{
var target_dir = default_target_dir
var ml_statistics = false
--- a/src/Pure/Admin/build_verit.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_verit.scala Sat Nov 28 21:56:24 2020 +0100
@@ -124,7 +124,7 @@
val isabelle_tool =
Isabelle_Tool("build_verit", "build prover component from official download",
- args =>
+ Scala_Project.here, args =>
{
var target_dir = Path.current
var mingw = MinGW.none
--- a/src/Pure/Admin/build_zipperposition.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala Sat Nov 28 21:56:24 2020 +0100
@@ -90,7 +90,7 @@
val isabelle_tool =
Isabelle_Tool("build_zipperposition", "build prover component from OPAM repository",
- args =>
+ Scala_Project.here, args =>
{
var target_dir = Path.current
var version = default_version
--- a/src/Pure/Admin/check_sources.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/check_sources.scala Sat Nov 28 21:56:24 2020 +0100
@@ -63,7 +63,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
+ Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources",
+ Scala_Project.here, args =>
{
val getopts = Getopts("""
Usage: isabelle check_sources [ROOT_DIRS...]
--- a/src/Pure/Admin/components.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Admin/components.scala Sat Nov 28 21:56:24 2020 +0100
@@ -262,7 +262,8 @@
List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
val isabelle_tool =
- Isabelle_Tool("build_components", "build and publish Isabelle components", args =>
+ Isabelle_Tool("build_components", "build and publish Isabelle components",
+ Scala_Project.here, args =>
{
var publish = false
var update_components_sha1 = false
--- a/src/Pure/General/mercurial.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/General/mercurial.scala Sat Nov 28 21:56:24 2020 +0100
@@ -298,7 +298,8 @@
}
val isabelle_tool =
- Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", args =>
+ Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
+ Scala_Project.here, args =>
{
var remote_name = ""
var path_name = default_path_name
--- a/src/Pure/ML/ml_process.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Sat Nov 28 21:56:24 2020 +0100
@@ -141,7 +141,8 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
+ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)",
+ Scala_Project.here, args =>
{
var dirs: List[Path] = Nil
var eval_args: List[String] = Nil
--- a/src/Pure/PIDE/markup.ML Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Nov 28 21:56:24 2020 +0100
@@ -68,6 +68,7 @@
val export_pathN: string val export_path: string -> T
val urlN: string val url: string -> T
val docN: string val doc: string -> T
+ val toolN: string val tool: string -> T
val markupN: string
val consistentN: string
val unbreakableN: string
@@ -403,6 +404,7 @@
val (export_pathN, export_path) = markup_string "export_path" nameN;
val (urlN, url) = markup_string "url" nameN;
val (docN, doc) = markup_string "doc" nameN;
+val (toolN, tool) = markup_string "tool" nameN;
(* pretty printing *)
--- a/src/Pure/ROOT.ML Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/ROOT.ML Sat Nov 28 21:56:24 2020 +0100
@@ -326,6 +326,7 @@
ML_file "System/isabelle_process.ML";
ML_file "System/scala.ML";
ML_file "System/scala_compiler.ML";
+ML_file "System/isabelle_tool.ML";
ML_file "Thy/bibtex.ML";
ML_file "PIDE/protocol.ML";
ML_file "General/output_primitives_virtual.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_tool.ML Sat Nov 28 21:56:24 2020 +0100
@@ -0,0 +1,44 @@
+(* Title: Pure/System/isabelle_tool.ML
+ Author: Makarius
+
+Support for Isabelle system tools.
+*)
+
+signature ISABELLE_TOOL =
+sig
+ val isabelle_tools: unit -> (string * Position.T) list
+ val check: Proof.context -> string * Position.T -> string
+end;
+
+structure Isabelle_Tool: ISABELLE_TOOL =
+struct
+
+(* list tools *)
+
+fun symbolic_file (a, b) =
+ if a = Markup.fileN
+ then (a, Path.explode b |> Path.implode_symbolic)
+ else (a, b);
+
+fun isabelle_tools () =
+ \<^scala>\<open>isabelle_tools\<close> ""
+ |> YXML.parse_body
+ |> let open XML.Decode in list (pair string properties) end
+ |> map (apsnd (map symbolic_file #> Position.of_properties));
+
+
+(* check *)
+
+fun check ctxt arg =
+ Completion.check_item Markup.toolN
+ (fn (name, pos) =>
+ Markup.entity Markup.toolN name
+ |> Markup.properties (Position.def_properties_of pos))
+ (isabelle_tools ()) ctxt arg;
+
+val _ =
+ Theory.setup
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>tool\<close>
+ (Scan.lift Parse.embedded_position) check);
+
+end;
--- a/src/Pure/System/isabelle_tool.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sat Nov 28 21:56:24 2020 +0100
@@ -9,7 +9,7 @@
import java.net.URLClassLoader
import scala.reflect.runtime.universe
-import scala.tools.reflect.{ToolBox,ToolBoxError}
+import scala.tools.reflect.{ToolBox, ToolBoxError}
object Isabelle_Tool
@@ -66,21 +66,6 @@
catch { case _: SecurityException => false }
}
- private def list_external(): List[(String, String)] =
- {
- val Description = """.*\bDESCRIPTION: *(.*)""".r
- for {
- dir <- dirs() if dir.is_dir
- file_name <- File.read_dir(dir) if is_external(dir, file_name)
- } yield {
- val source = File.read(dir + Path.explode(file_name))
- val name = Library.perhaps_unsuffix(".scala", file_name)
- val description =
- split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
- (name, description)
- }
- }
-
private def find_external(name: String): Option[List[String] => Unit] =
dirs().collectFirst({
case dir if is_external(dir, name + ".scala") =>
@@ -100,10 +85,6 @@
private lazy val internal_tools: List[Isabelle_Tool] =
Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools)
- private def list_internal(): List[(String, String)] =
- for (tool <- internal_tools.toList)
- yield (tool.name, tool.description)
-
private def find_internal(name: String): Option[List[String] => Unit] =
internal_tools.collectFirst({
case tool if tool.name == name =>
@@ -111,6 +92,58 @@
})
+ /* list tools */
+
+ abstract class Entry
+ {
+ def name: String
+ def position: Properties.T
+ def description: String
+ def print: String =
+ description match {
+ case "" => name
+ case descr => name + " - " + descr
+ }
+ }
+
+ sealed case class External(name: String, path: Path) extends Entry
+ {
+ def position: Properties.T = Position.File(path.absolute.implode)
+ def description: String =
+ {
+ val Pattern = """.*\bDESCRIPTION: *(.*)""".r
+ split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse ""
+ }
+ }
+
+ def external_tools(): List[External] =
+ {
+ for {
+ dir <- dirs() if dir.is_dir
+ file_name <- File.read_dir(dir) if is_external(dir, file_name)
+ } yield {
+ val path = dir + Path.explode(file_name)
+ val name = Library.perhaps_unsuffix(".scala", file_name)
+ External(name, path)
+ }
+ }
+
+ def isabelle_tools(): List[Entry] =
+ (external_tools() ::: internal_tools).sortBy(_.name)
+
+ object Isabelle_Tools extends Scala.Fun("isabelle_tools")
+ {
+ val here = Scala_Project.here
+ def apply(arg: String): String =
+ if (arg.nonEmpty) error("Bad argument: " + quote(arg))
+ else {
+ val result = isabelle_tools().map(entry => (entry.name, entry.position))
+ val body = { import XML.Encode._; list(pair(string, properties))(result) }
+ YXML.string_of_body(body)
+ }
+ }
+
+
/* command line entry point */
def main(args: Array[String])
@@ -118,9 +151,7 @@
Command_Line.tool {
args.toList match {
case Nil | List("-?") =>
- val tool_descriptions =
- (list_external() ::: list_internal()).sortBy(_._1).
- map({ case (a, "") => a case (a, b) => a + " - " + b })
+ val tool_descriptions = isabelle_tools().map(_.print)
Getopts("""
Usage: isabelle TOOL [ARGS ...]
@@ -137,7 +168,14 @@
}
}
-sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
+sealed case class Isabelle_Tool(
+ name: String,
+ description: String,
+ here: Scala_Project.Here,
+ body: List[String] => Unit) extends Isabelle_Tool.Entry
+{
+ def position: Position.T = here.position
+}
class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
--- a/src/Pure/System/options.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/System/options.scala Sat Nov 28 21:56:24 2020 +0100
@@ -148,7 +148,8 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", args =>
+ val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options",
+ Scala_Project.here, args =>
{
var build_options = false
var get_option = ""
--- a/src/Pure/System/scala.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/System/scala.scala Sat Nov 28 21:56:24 2020 +0100
@@ -243,4 +243,5 @@
Scala.Sleep,
Scala.Toplevel,
Doc.Doc_Names,
- Bibtex.Check_Database)
+ Bibtex.Check_Database,
+ Isabelle_Tool.Isabelle_Tools)
--- a/src/Pure/Thy/export.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Thy/export.scala Sat Nov 28 21:56:24 2020 +0100
@@ -372,7 +372,8 @@
val default_export_dir: Path = Path.explode("export")
- val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
+ val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports",
+ Scala_Project.here, args =>
{
/* arguments */
--- a/src/Pure/Thy/presentation.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Sat Nov 28 21:56:24 2020 +0100
@@ -612,7 +612,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("document", "prepare session theory document", args =>
+ Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args =>
{
var output_sources: Option[Path] = None
var output_pdf: Option[Path] = None
--- a/src/Pure/Thy/sessions.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Nov 28 21:56:24 2020 +0100
@@ -1048,7 +1048,8 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", args =>
+ val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
+ Scala_Project.here, args =>
{
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
--- a/src/Pure/Tools/build.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/build.scala Sat Nov 28 21:56:24 2020 +0100
@@ -526,7 +526,8 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
+ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
+ Scala_Project.here, args =>
{
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
--- a/src/Pure/Tools/build_docker.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/build_docker.scala Sat Nov 28 21:56:24 2020 +0100
@@ -100,7 +100,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
+ Isabelle_Tool("build_docker", "build Isabelle docker image",
+ Scala_Project.here, args =>
{
var base = default_base
var entrypoint = false
--- a/src/Pure/Tools/doc.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/doc.scala Sat Nov 28 21:56:24 2020 +0100
@@ -100,7 +100,8 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
+ val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation",
+ Scala_Project.here, args =>
{
val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
--- a/src/Pure/Tools/dump.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/dump.scala Sat Nov 28 21:56:24 2020 +0100
@@ -420,7 +420,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
+ Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here, args =>
{
var aspects: List[Aspect] = known_aspects
var base_sessions: List[String] = Nil
--- a/src/Pure/Tools/mkroot.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/mkroot.scala Sat Nov 28 21:56:24 2020 +0100
@@ -176,7 +176,8 @@
/** Isabelle tool wrapper **/
- val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
+ val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory",
+ Scala_Project.here, args =>
{
var author = ""
var init_repos = false
--- a/src/Pure/Tools/phabricator.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala Sat Nov 28 21:56:24 2020 +0100
@@ -146,7 +146,8 @@
/* Isabelle tool wrapper */
val isabelle_tool1 =
- Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", args =>
+ Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory",
+ Scala_Project.here, args =>
{
var list = false
var name = default_name
@@ -535,7 +536,8 @@
/* Isabelle tool wrapper */
val isabelle_tool2 =
- Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", args =>
+ Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux",
+ Scala_Project.here, args =>
{
var mercurial_source = ""
var repo = ""
@@ -642,8 +644,8 @@
/* Isabelle tool wrapper */
val isabelle_tool3 =
- Isabelle_Tool("phabricator_setup_mail",
- "setup mail for one Phabricator installation", args =>
+ Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation",
+ Scala_Project.here, args =>
{
var test_user = ""
var name = default_name
@@ -805,8 +807,8 @@
/* Isabelle tool wrapper */
val isabelle_tool4 =
- Isabelle_Tool("phabricator_setup_ssh",
- "setup ssh service for all Phabricator installations", args =>
+ Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations",
+ Scala_Project.here, args =>
{
var server_port = default_server_port
var system_port = default_system_port
--- a/src/Pure/Tools/profiling_report.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/profiling_report.scala Sat Nov 28 21:56:24 2020 +0100
@@ -30,7 +30,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args =>
+ Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files",
+ Scala_Project.here, args =>
{
val getopts =
Getopts("""
--- a/src/Pure/Tools/scala_project.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/scala_project.scala Sat Nov 28 21:56:24 2020 +0100
@@ -161,7 +161,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit", args =>
+ Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit",
+ Scala_Project.here, args =>
{
var symlinks = false
--- a/src/Pure/Tools/server.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/server.scala Sat Nov 28 21:56:24 2020 +0100
@@ -418,7 +418,7 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("server", "manage resident Isabelle servers", args =>
+ Isabelle_Tool("server", "manage resident Isabelle servers", Scala_Project.here, args =>
{
var console = false
var log_file: Option[Path] = None
--- a/src/Pure/Tools/update.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update.scala Sat Nov 28 21:56:24 2020 +0100
@@ -63,7 +63,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("update", "update theory sources based on PIDE markup", args =>
+ Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here,
+ args =>
{
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
--- a/src/Pure/Tools/update_cartouches.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Sat Nov 28 21:56:24 2020 +0100
@@ -84,7 +84,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
+ Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches",
+ Scala_Project.here, args =>
{
var replace_text = false
--- a/src/Pure/Tools/update_comments.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_comments.scala Sat Nov 28 21:56:24 2020 +0100
@@ -47,7 +47,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("update_comments", "update formal comments in outer syntax", args =>
+ Isabelle_Tool("update_comments", "update formal comments in outer syntax",
+ Scala_Project.here, args =>
{
val getopts = Getopts("""
Usage: isabelle update_comments [FILES|DIRS...]
--- a/src/Pure/Tools/update_header.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_header.scala Sat Nov 28 21:56:24 2020 +0100
@@ -29,7 +29,8 @@
Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
val isabelle_tool =
- Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
+ Isabelle_Tool("update_header", "replace obsolete theory header command",
+ Scala_Project.here, args =>
{
var section = "section"
--- a/src/Pure/Tools/update_then.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_then.scala Sat Nov 28 21:56:24 2020 +0100
@@ -31,7 +31,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args =>
+ Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'",
+ Scala_Project.here, args =>
{
val getopts = Getopts("""
Usage: isabelle update_then [FILES|DIRS...]
--- a/src/Pure/Tools/update_theorems.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Pure/Tools/update_theorems.scala Sat Nov 28 21:56:24 2020 +0100
@@ -31,7 +31,8 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
+ val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords",
+ Scala_Project.here, args =>
{
val getopts = Getopts("""
Usage: isabelle update_theorems [FILES|DIRS...]
--- a/src/Tools/VSCode/src/build_vscode.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala Sat Nov 28 21:56:24 2020 +0100
@@ -44,7 +44,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module", args =>
+ Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module",
+ Scala_Project.here, args =>
{
var publish = false
--- a/src/Tools/VSCode/src/grammar.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Sat Nov 28 21:56:24 2020 +0100
@@ -134,7 +134,7 @@
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("vscode_grammar",
- "generate static TextMate grammar for VSCode editor", args =>
+ "generate static TextMate grammar for VSCode editor", Scala_Project.here, args =>
{
var dirs: List[Path] = Nil
var logic = default_logic
--- a/src/Tools/VSCode/src/language_server.scala Sat Nov 28 20:18:29 2020 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Sat Nov 28 21:56:24 2020 +0100
@@ -28,20 +28,21 @@
private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
- val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
- {
- try {
- var logic_ancestor: Option[String] = None
- var log_file: Option[Path] = None
- var logic_requirements = false
- var dirs: List[Path] = Nil
- var include_sessions: List[String] = Nil
- var logic = default_logic
- var modes: List[String] = Nil
- var options = Options.init()
- var verbose = false
+ val isabelle_tool =
+ Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", Scala_Project.here, args =>
+ {
+ try {
+ var logic_ancestor: Option[String] = None
+ var log_file: Option[Path] = None
+ var logic_requirements = false
+ var dirs: List[Path] = Nil
+ var include_sessions: List[String] = Nil
+ var logic = default_logic
+ var modes: List[String] = Nil
+ var options = Options.init()
+ var verbose = false
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle vscode_server [OPTIONS]
Options are:
@@ -57,41 +58,41 @@
Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
""",
- "A:" -> (arg => logic_ancestor = Some(arg)),
- "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
- "R:" -> (arg => { logic = arg; logic_requirements = true }),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
- "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
- "l:" -> (arg => logic = arg),
- "m:" -> (arg => modes = arg :: modes),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true))
+ "A:" -> (arg => logic_ancestor = Some(arg)),
+ "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
+ "R:" -> (arg => { logic = arg; logic_requirements = true }),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))),
+ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true))
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
- val log = Logger.make(log_file)
- val channel = new Channel(System.in, System.out, log, verbose)
- val server =
- new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
- include_sessions = include_sessions, session_ancestor = logic_ancestor,
- session_requirements = logic_requirements, modes = modes, log = log)
+ val log = Logger.make(log_file)
+ val channel = new Channel(System.in, System.out, log, verbose)
+ val server =
+ new Language_Server(channel, options, session_name = logic, session_dirs = dirs,
+ include_sessions = include_sessions, session_ancestor = logic_ancestor,
+ session_requirements = logic_requirements, modes = modes, log = log)
- // prevent spurious garbage on the main protocol channel
- val orig_out = System.out
- try {
- System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
- server.start()
+ // prevent spurious garbage on the main protocol channel
+ val orig_out = System.out
+ try {
+ System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
+ server.start()
+ }
+ finally { System.setOut(orig_out) }
}
- finally { System.setOut(orig_out) }
- }
- catch {
- case exn: Throwable =>
- val channel = new Channel(System.in, System.out, No_Logger)
- channel.error_message(Exn.message(exn))
- throw(exn)
- }
- })
+ catch {
+ case exn: Throwable =>
+ val channel = new Channel(System.in, System.out, No_Logger)
+ channel.error_message(Exn.message(exn))
+ throw(exn)
+ }
+ })
}
class Language_Server(