--- a/bin/isabelle Sun Apr 03 19:47:29 2016 +0200
+++ b/bin/isabelle Sun Apr 03 21:32:57 2016 +0200
@@ -18,46 +18,40 @@
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-## diagnostics
+## external tool (shell script)
+
+if [ "$#" -ge 1 -a "$1" != "-?" ]
+then
+ TOOL_NAME="$1"
-function usage()
-{
- echo
- echo "Usage: $PRG NAME [ARGS ...]"
- echo
- echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
- echo
- echo "Available tools:"
- perl -w "$ISABELLE_HOME/lib/scripts/tools.pl"
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
+ splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+ for DIR in "${TOOLS[@]}"
+ do
+ TOOL="$DIR/$TOOL_NAME"
+ case "$TOOL" in
+ *~ | *.orig) ;;
+ *)
+ if [ -f "$TOOL" -a -x "$TOOL" ]; then
+ shift
+ exec "$TOOL" "$@"
+ fi
+ ;;
+ esac
+ done
+fi
-## args
-
-[ "$#" -lt 1 -o "$1" = "-?" ] && usage
+## internal tool or usage (Scala)
-TOOLNAME="$1"
-shift
-
-
-## main
+isabelle_admin_build jars || exit $?
-splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+case "$ISABELLE_JAVA_PLATFORM" in
+ x86-*)
+ eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS32)"
+ ;;
+ x86_64-*)
+ eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS64)"
+ ;;
+esac
-for DIR in "${TOOLS[@]}"
-do
- TOOL="$DIR/$TOOLNAME"
- case "$TOOL" in
- *~ | *.orig) ;;
- *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;;
- esac
-done
-
-fail "Unknown Isabelle tool: $TOOLNAME"
+exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
--- a/lib/scripts/tools.pl Sun Apr 03 19:47:29 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-#
-# Author: Makarius
-#
-# tools.pl - list Isabelle tools with description
-#
-
-use strict;
-use warnings;
-
-my @tools = ();
-
-for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) {
- if (-d $dir) {
- if (opendir DIR, $dir) {
- for my $name (readdir DIR) {
- my $file = "$dir/$name";
- if (-f $file and -x $file and !($file =~ /~$/ or $file =~ /\.orig$/)) {
- if (open FILE, $file) {
- my $description;
- while (<FILE>) {
- if (!defined($description) and m/DESCRIPTION: *(.*)$/) {
- $description = $1;
- }
- }
- close FILE;
- if (defined($description)) {
- push(@tools, " $name - $description\n");
- }
- }
- }
- }
- closedir DIR;
- }
- }
-}
-
-for (sort @tools) { print };
--- a/src/Doc/System/Environment.thy Sun Apr 03 19:47:29 2016 +0200
+++ b/src/Doc/System/Environment.thy Sun Apr 03 21:32:57 2016 +0200
@@ -267,7 +267,7 @@
@{verbatim [display]
\<open>Usage: isabelle TOOL [ARGS ...]
- Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+ Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
Available tools:
...\<close>}
--- a/src/Doc/antiquote_setup.ML Sun Apr 03 19:47:29 2016 +0200
+++ b/src/Doc/antiquote_setup.ML Sun Apr 03 21:32:57 2016 +0200
@@ -157,17 +157,6 @@
(Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
handle ERROR _ => false;
-fun check_tool ctxt (name, pos) =
- let
- fun tool dir =
- let val path = Path.append dir (Path.basic name)
- in if File.exists path then SOME path else NONE end;
- in
- (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
- NONE => false
- | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
- end;
-
val arg = enclose "{" "}" o clean_string;
fun entity check markup binding index =
@@ -220,7 +209,7 @@
entity_antiqs check_system_option "isasystem" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
entity_antiqs no_check "isasystem" @{binding executable} #>
- entity_antiqs check_tool "isatool" @{binding tool} #>
+ entity_antiqs no_check "isatool" @{binding tool} #>
entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
--- a/src/Pure/General/file.scala Sun Apr 03 19:47:29 2016 +0200
+++ b/src/Pure/General/file.scala Sun Apr 03 21:32:57 2016 +0200
@@ -141,7 +141,15 @@
if (path.is_file) path else error("No such file: " + path)
- /* find files */
+ /* directory content */
+
+ def read_dir(dir: Path): List[String] =
+ {
+ if (!dir.is_dir) error("Bad directory: " + dir.toString)
+ val files = dir.file.listFiles
+ if (files == null) Nil
+ else files.toList.map(_.getName)
+ }
def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
{
--- a/src/Pure/System/isabelle_system.ML Sun Apr 03 19:47:29 2016 +0200
+++ b/src/Pure/System/isabelle_system.ML Sun Apr 03 21:32:57 2016 +0200
@@ -6,7 +6,6 @@
signature ISABELLE_SYSTEM =
sig
- val isabelle_tool: string -> string -> int
val mkdirs: Path.T -> unit
val mkdir: Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
@@ -37,29 +36,12 @@
in rc end;
-(* system commands *)
-
-fun isabelle_tool name args =
- (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
- let
- val path = Path.append (Path.explode dir) (Path.basic name);
- val platform_path = File.platform_path path;
- in
- if can OS.FileSys.modTime platform_path andalso
- not (OS.FileSys.isDir platform_path) andalso
- OS.FileSys.access (platform_path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
- then SOME path
- else NONE
- end handle OS.SysErr _ => NONE) of
- SOME path => bash (File.bash_path path ^ " " ^ args)
- | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
+(* directory operations *)
fun system_command cmd =
- if bash cmd <> 0 then error ("System command failed: " ^ cmd)
- else ();
+ if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
-
-(* directory operations *)
+fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
fun mkdirs path =
if File.is_dir path then ()
@@ -112,8 +94,6 @@
(* tmp dirs *)
-fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
-
fun with_tmp_dir name f =
let
val path = create_tmp_path name "";
@@ -121,4 +101,3 @@
in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_tool.scala Sun Apr 03 21:32:57 2016 +0200
@@ -0,0 +1,75 @@
+/* Title: Pure/System/isabelle_tool.scala
+ Author: Makarius
+
+Isabelle system tools: external executables or internal Scala functions.
+*/
+
+package isabelle
+
+
+object Isabelle_Tool
+{
+ /* external tools */
+
+ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
+
+ private def is_external(dir: Path, name: String): Boolean =
+ {
+ val file = (dir + Path.basic(name)).file
+ try {
+ file.isFile && file.canRead && file.canExecute &&
+ !name.endsWith("~") && !name.endsWith(".orig")
+ }
+ catch { case _: SecurityException => false }
+ }
+
+ private def run_external(dir: Path, name: String)(args: List[String]): Nothing =
+ {
+ val tool = dir + Path.basic(name)
+ val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
+ sys.exit(result.print_stdout.rc)
+ }
+
+ private def find_external(name: String): Option[List[String] => Unit] =
+ dirs.collectFirst({ case dir if is_external(dir, name) => run_external(dir, name) })
+
+
+ /* command line entry point */
+
+ private def tool_descriptions(): List[String] =
+ {
+ val Description = """.*\bDESCRIPTION: *(.*)""".r
+ val entries =
+ for {
+ dir <- dirs() if dir.is_dir
+ name <- File.read_dir(dir) if is_external(dir, name)
+ } yield {
+ val source = File.read(dir + Path.basic(name))
+ split_lines(source).collectFirst({ case Description(s) => s }) match {
+ case None => (name, "")
+ case Some(description) => (name, " - " + description)
+ }
+ }
+ entries.sortBy(_._1).map({ case (a, b) => a + b })
+ }
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ args.toList match {
+ case Nil | List("-?") =>
+ Getopts("""
+Usage: isabelle TOOL [ARGS ...]
+
+ Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
+
+Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage
+ case tool_name :: tool_args =>
+ find_external(tool_name) match {
+ case Some(run) => run(tool_args)
+ case None => error("Unknown Isabelle tool: " + quote(tool_name))
+ }
+ }
+ }
+ }
+}
--- a/src/Pure/Thy/present.ML Sun Apr 03 19:47:29 2016 +0200
+++ b/src/Pure/Thy/present.ML Sun Apr 03 21:32:57 2016 +0200
@@ -269,8 +269,8 @@
val doc_dir = Path.append doc_prefix (Path.basic doc_name);
val _ = Isabelle_System.mkdirs doc_dir;
val _ =
- Isabelle_System.isabelle_tool "latex"
- ("-o sty " ^ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
+ Isabelle_System.bash ("isabelle latex -o sty " ^
+ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
val _ = write_tex_index tex_index doc_dir;
@@ -360,8 +360,8 @@
val _ = Isabelle_System.mkdirs doc_path;
val root_path = Path.append doc_path (Path.basic "root.tex");
val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
- val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.bash_path root_path);
- val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.bash_path root_path);
+ val _ = Isabelle_System.bash ("isabelle latex -o sty " ^ File.bash_path root_path);
+ val _ = Isabelle_System.bash ("isabelle latex -o syms " ^ File.bash_path root_path);
fun known name =
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
@@ -382,8 +382,6 @@
val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
val _ = Isabelle_System.mkdirs target_dir;
val _ = Isabelle_System.copy_file result target;
- in
- Isabelle_System.isabelle_tool "display" (File.bash_path target ^ " &")
- end);
+ in Isabelle_System.bash ("isabelle display " ^ File.bash_path target ^ " &") end);
end;
--- a/src/Pure/build-jars Sun Apr 03 19:47:29 2016 +0200
+++ b/src/Pure/build-jars Sun Apr 03 21:32:57 2016 +0200
@@ -81,6 +81,7 @@
System/isabelle_charset.scala
System/isabelle_process.scala
System/isabelle_system.scala
+ System/isabelle_tool.scala
System/options.scala
System/platform.scala
System/posix_interrupt.scala