# HG changeset patch
# User wenzelm
# Date 1459711977 -7200
# Node ID 4141c2a8458b5c7285afebbb98995baf1396777c
# Parent  3fee575c9dce7f31068a94209fa1f2f2e2e52b9f
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;

diff -r 3fee575c9dce -r 4141c2a8458b bin/isabelle
--- 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 "$@"
diff -r 3fee575c9dce -r 4141c2a8458b lib/scripts/tools.pl
--- 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 };
diff -r 3fee575c9dce -r 4141c2a8458b src/Doc/System/Environment.thy
--- 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>}
diff -r 3fee575c9dce -r 4141c2a8458b src/Doc/antiquote_setup.ML
--- 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});
 
diff -r 3fee575c9dce -r 4141c2a8458b src/Pure/General/file.scala
--- 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] =
   {
diff -r 3fee575c9dce -r 4141c2a8458b src/Pure/System/isabelle_system.ML
--- 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;
-
diff -r 3fee575c9dce -r 4141c2a8458b src/Pure/System/isabelle_tool.scala
--- /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))
+          }
+      }
+    }
+  }
+}
diff -r 3fee575c9dce -r 4141c2a8458b src/Pure/Thy/present.ML
--- 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;
diff -r 3fee575c9dce -r 4141c2a8458b src/Pure/build-jars
--- 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