clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
authorwenzelm
Sun Apr 03 21:32:57 2016 +0200 (2016-04-03)
changeset 628294141c2a8458b
parent 62828 3fee575c9dce
child 62830 85024c0e953d
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
bin/isabelle
lib/scripts/tools.pl
src/Doc/System/Environment.thy
src/Doc/antiquote_setup.ML
src/Pure/General/file.scala
src/Pure/System/isabelle_system.ML
src/Pure/System/isabelle_tool.scala
src/Pure/Thy/present.ML
src/Pure/build-jars
     1.1 --- a/bin/isabelle	Sun Apr 03 19:47:29 2016 +0200
     1.2 +++ b/bin/isabelle	Sun Apr 03 21:32:57 2016 +0200
     1.3 @@ -18,46 +18,40 @@
     1.4  source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
     1.5  
     1.6  
     1.7 -## diagnostics
     1.8 +## external tool (shell script)
     1.9 +
    1.10 +if [ "$#" -ge 1 -a "$1" != "-?" ]
    1.11 +then
    1.12 +  TOOL_NAME="$1"
    1.13  
    1.14 -function usage()
    1.15 -{
    1.16 -  echo
    1.17 -  echo "Usage: $PRG NAME [ARGS ...]"
    1.18 -  echo
    1.19 -  echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
    1.20 -  echo
    1.21 -  echo "Available tools:"
    1.22 -  perl -w "$ISABELLE_HOME/lib/scripts/tools.pl"
    1.23 -  exit 1
    1.24 -}
    1.25 -
    1.26 -function fail()
    1.27 -{
    1.28 -  echo "$1" >&2
    1.29 -  exit 2
    1.30 -}
    1.31 +  splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
    1.32 +  for DIR in "${TOOLS[@]}"
    1.33 +  do
    1.34 +    TOOL="$DIR/$TOOL_NAME"
    1.35 +    case "$TOOL" in
    1.36 +      *~ | *.orig) ;;
    1.37 +      *)
    1.38 +        if [ -f "$TOOL" -a -x "$TOOL" ]; then
    1.39 +          shift
    1.40 +          exec "$TOOL" "$@"
    1.41 +        fi
    1.42 +        ;;
    1.43 +    esac
    1.44 +  done
    1.45 +fi
    1.46  
    1.47  
    1.48 -## args
    1.49 -
    1.50 -[ "$#" -lt 1 -o "$1" = "-?" ] && usage
    1.51 +## internal tool or usage (Scala)
    1.52  
    1.53 -TOOLNAME="$1"
    1.54 -shift
    1.55 -
    1.56 -
    1.57 -## main
    1.58 +isabelle_admin_build jars || exit $?
    1.59  
    1.60 -splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
    1.61 +case "$ISABELLE_JAVA_PLATFORM" in
    1.62 +  x86-*)
    1.63 +    eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS32)"
    1.64 +    ;;
    1.65 +  x86_64-*)
    1.66 +    eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS64)"
    1.67 +    ;;
    1.68 +esac
    1.69  
    1.70 -for DIR in "${TOOLS[@]}"
    1.71 -do
    1.72 -  TOOL="$DIR/$TOOLNAME"
    1.73 -  case "$TOOL" in
    1.74 -    *~ | *.orig) ;;
    1.75 -    *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;;
    1.76 -  esac
    1.77 -done
    1.78 -
    1.79 -fail "Unknown Isabelle tool: $TOOLNAME"
    1.80 +exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
     2.1 --- a/lib/scripts/tools.pl	Sun Apr 03 19:47:29 2016 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,37 +0,0 @@
     2.4 -#
     2.5 -# Author: Makarius
     2.6 -#
     2.7 -# tools.pl - list Isabelle tools with description
     2.8 -#
     2.9 -
    2.10 -use strict;
    2.11 -use warnings;
    2.12 -
    2.13 -my @tools = ();
    2.14 -
    2.15 -for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) {
    2.16 -  if (-d $dir) {
    2.17 -    if (opendir DIR, $dir) {
    2.18 -      for my $name (readdir DIR) {
    2.19 -        my $file = "$dir/$name";
    2.20 -        if (-f $file and -x $file and !($file =~ /~$/ or $file =~ /\.orig$/)) {
    2.21 -          if (open FILE, $file) {
    2.22 -            my $description;
    2.23 -            while (<FILE>) {
    2.24 -              if (!defined($description) and m/DESCRIPTION: *(.*)$/) {
    2.25 -                $description = $1;
    2.26 -              }
    2.27 -            }
    2.28 -            close FILE;
    2.29 -            if (defined($description)) {
    2.30 -              push(@tools, "  $name - $description\n");
    2.31 -            }
    2.32 -          }
    2.33 -        }
    2.34 -      }
    2.35 -      closedir DIR;
    2.36 -    }
    2.37 -  }
    2.38 -}
    2.39 -
    2.40 -for (sort @tools) { print };
     3.1 --- a/src/Doc/System/Environment.thy	Sun Apr 03 19:47:29 2016 +0200
     3.2 +++ b/src/Doc/System/Environment.thy	Sun Apr 03 21:32:57 2016 +0200
     3.3 @@ -267,7 +267,7 @@
     3.4    @{verbatim [display]
     3.5  \<open>Usage: isabelle TOOL [ARGS ...]
     3.6  
     3.7 -  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
     3.8 +  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
     3.9  
    3.10  Available tools:
    3.11    ...\<close>}
     4.1 --- a/src/Doc/antiquote_setup.ML	Sun Apr 03 19:47:29 2016 +0200
     4.2 +++ b/src/Doc/antiquote_setup.ML	Sun Apr 03 21:32:57 2016 +0200
     4.3 @@ -157,17 +157,6 @@
     4.4    (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
     4.5      handle ERROR _ => false;
     4.6  
     4.7 -fun check_tool ctxt (name, pos) =
     4.8 -  let
     4.9 -    fun tool dir =
    4.10 -      let val path = Path.append dir (Path.basic name)
    4.11 -      in if File.exists path then SOME path else NONE end;
    4.12 -  in
    4.13 -    (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
    4.14 -      NONE => false
    4.15 -    | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
    4.16 -  end;
    4.17 -
    4.18  val arg = enclose "{" "}" o clean_string;
    4.19  
    4.20  fun entity check markup binding index =
    4.21 @@ -220,7 +209,7 @@
    4.22      entity_antiqs check_system_option "isasystem" @{binding system_option} #>
    4.23      entity_antiqs no_check "" @{binding inference} #>
    4.24      entity_antiqs no_check "isasystem" @{binding executable} #>
    4.25 -    entity_antiqs check_tool "isatool" @{binding tool} #>
    4.26 +    entity_antiqs no_check "isatool" @{binding tool} #>
    4.27      entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
    4.28      entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
    4.29  
     5.1 --- a/src/Pure/General/file.scala	Sun Apr 03 19:47:29 2016 +0200
     5.2 +++ b/src/Pure/General/file.scala	Sun Apr 03 21:32:57 2016 +0200
     5.3 @@ -141,7 +141,15 @@
     5.4      if (path.is_file) path else error("No such file: " + path)
     5.5  
     5.6  
     5.7 -  /* find files */
     5.8 +  /* directory content */
     5.9 +
    5.10 +  def read_dir(dir: Path): List[String] =
    5.11 +  {
    5.12 +    if (!dir.is_dir) error("Bad directory: " + dir.toString)
    5.13 +    val files = dir.file.listFiles
    5.14 +    if (files == null) Nil
    5.15 +    else files.toList.map(_.getName)
    5.16 +  }
    5.17  
    5.18    def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
    5.19    {
     6.1 --- a/src/Pure/System/isabelle_system.ML	Sun Apr 03 19:47:29 2016 +0200
     6.2 +++ b/src/Pure/System/isabelle_system.ML	Sun Apr 03 21:32:57 2016 +0200
     6.3 @@ -6,7 +6,6 @@
     6.4  
     6.5  signature ISABELLE_SYSTEM =
     6.6  sig
     6.7 -  val isabelle_tool: string -> string -> int
     6.8    val mkdirs: Path.T -> unit
     6.9    val mkdir: Path.T -> unit
    6.10    val copy_dir: Path.T -> Path.T -> unit
    6.11 @@ -37,29 +36,12 @@
    6.12    in rc end;
    6.13  
    6.14  
    6.15 -(* system commands *)
    6.16 -
    6.17 -fun isabelle_tool name args =
    6.18 -  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
    6.19 -      let
    6.20 -        val path = Path.append (Path.explode dir) (Path.basic name);
    6.21 -        val platform_path = File.platform_path path;
    6.22 -      in
    6.23 -        if can OS.FileSys.modTime platform_path andalso
    6.24 -          not (OS.FileSys.isDir platform_path) andalso
    6.25 -          OS.FileSys.access (platform_path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
    6.26 -        then SOME path
    6.27 -        else NONE
    6.28 -      end handle OS.SysErr _ => NONE) of
    6.29 -    SOME path => bash (File.bash_path path ^ " " ^ args)
    6.30 -  | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
    6.31 +(* directory operations *)
    6.32  
    6.33  fun system_command cmd =
    6.34 -  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
    6.35 -  else ();
    6.36 +  if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
    6.37  
    6.38 -
    6.39 -(* directory operations *)
    6.40 +fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
    6.41  
    6.42  fun mkdirs path =
    6.43    if File.is_dir path then ()
    6.44 @@ -112,8 +94,6 @@
    6.45  
    6.46  (* tmp dirs *)
    6.47  
    6.48 -fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
    6.49 -
    6.50  fun with_tmp_dir name f =
    6.51    let
    6.52      val path = create_tmp_path name "";
    6.53 @@ -121,4 +101,3 @@
    6.54    in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
    6.55  
    6.56  end;
    6.57 -
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 21:32:57 2016 +0200
     7.3 @@ -0,0 +1,75 @@
     7.4 +/*  Title:      Pure/System/isabelle_tool.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Isabelle system tools: external executables or internal Scala functions.
     7.8 +*/
     7.9 +
    7.10 +package isabelle
    7.11 +
    7.12 +
    7.13 +object Isabelle_Tool
    7.14 +{
    7.15 +  /* external tools */
    7.16 +
    7.17 +  private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
    7.18 +
    7.19 +  private def is_external(dir: Path, name: String): Boolean =
    7.20 +  {
    7.21 +    val file = (dir + Path.basic(name)).file
    7.22 +    try {
    7.23 +      file.isFile && file.canRead && file.canExecute &&
    7.24 +        !name.endsWith("~") && !name.endsWith(".orig")
    7.25 +    }
    7.26 +    catch { case _: SecurityException => false }
    7.27 +  }
    7.28 +
    7.29 +  private def run_external(dir: Path, name: String)(args: List[String]): Nothing =
    7.30 +  {
    7.31 +    val tool = dir + Path.basic(name)
    7.32 +    val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    7.33 +    sys.exit(result.print_stdout.rc)
    7.34 +  }
    7.35 +
    7.36 +  private def find_external(name: String): Option[List[String] => Unit] =
    7.37 +    dirs.collectFirst({ case dir if is_external(dir, name) => run_external(dir, name) })
    7.38 +
    7.39 +
    7.40 +  /* command line entry point */
    7.41 +
    7.42 +  private def tool_descriptions(): List[String] =
    7.43 +  {
    7.44 +    val Description = """.*\bDESCRIPTION: *(.*)""".r
    7.45 +    val entries =
    7.46 +      for {
    7.47 +        dir <- dirs() if dir.is_dir
    7.48 +        name <- File.read_dir(dir) if is_external(dir, name)
    7.49 +      } yield {
    7.50 +        val source = File.read(dir + Path.basic(name))
    7.51 +        split_lines(source).collectFirst({ case Description(s) => s }) match {
    7.52 +          case None => (name, "")
    7.53 +          case Some(description) => (name, " - " + description)
    7.54 +        }
    7.55 +      }
    7.56 +    entries.sortBy(_._1).map({ case (a, b) => a + b })
    7.57 +  }
    7.58 +
    7.59 +  def main(args: Array[String])
    7.60 +  {
    7.61 +    Command_Line.tool0 {
    7.62 +      args.toList match {
    7.63 +        case Nil | List("-?") =>
    7.64 +          Getopts("""
    7.65 +Usage: isabelle TOOL [ARGS ...]
    7.66 +
    7.67 +  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
    7.68 +
    7.69 +Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
    7.70 +        case tool_name :: tool_args =>
    7.71 +          find_external(tool_name) match {
    7.72 +            case Some(run) => run(tool_args)
    7.73 +            case None => error("Unknown Isabelle tool: " + quote(tool_name))
    7.74 +          }
    7.75 +      }
    7.76 +    }
    7.77 +  }
    7.78 +}
     8.1 --- a/src/Pure/Thy/present.ML	Sun Apr 03 19:47:29 2016 +0200
     8.2 +++ b/src/Pure/Thy/present.ML	Sun Apr 03 21:32:57 2016 +0200
     8.3 @@ -269,8 +269,8 @@
     8.4          val doc_dir = Path.append doc_prefix (Path.basic doc_name);
     8.5          val _ = Isabelle_System.mkdirs doc_dir;
     8.6          val _ =
     8.7 -          Isabelle_System.isabelle_tool "latex"
     8.8 -            ("-o sty " ^ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
     8.9 +          Isabelle_System.bash ("isabelle latex -o sty " ^
    8.10 +            File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
    8.11          val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
    8.12          val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
    8.13          val _ = write_tex_index tex_index doc_dir;
    8.14 @@ -360,8 +360,8 @@
    8.15      val _ = Isabelle_System.mkdirs doc_path;
    8.16      val root_path = Path.append doc_path (Path.basic "root.tex");
    8.17      val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
    8.18 -    val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.bash_path root_path);
    8.19 -    val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.bash_path root_path);
    8.20 +    val _ = Isabelle_System.bash ("isabelle latex -o sty " ^ File.bash_path root_path);
    8.21 +    val _ = Isabelle_System.bash ("isabelle latex -o syms " ^ File.bash_path root_path);
    8.22  
    8.23      fun known name =
    8.24        let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
    8.25 @@ -382,8 +382,6 @@
    8.26      val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
    8.27      val _ = Isabelle_System.mkdirs target_dir;
    8.28      val _ = Isabelle_System.copy_file result target;
    8.29 -  in
    8.30 -    Isabelle_System.isabelle_tool "display" (File.bash_path target ^ " &")
    8.31 -  end);
    8.32 +  in Isabelle_System.bash ("isabelle display " ^ File.bash_path target ^ " &") end);
    8.33  
    8.34  end;
     9.1 --- a/src/Pure/build-jars	Sun Apr 03 19:47:29 2016 +0200
     9.2 +++ b/src/Pure/build-jars	Sun Apr 03 21:32:57 2016 +0200
     9.3 @@ -81,6 +81,7 @@
     9.4    System/isabelle_charset.scala
     9.5    System/isabelle_process.scala
     9.6    System/isabelle_system.scala
     9.7 +  System/isabelle_tool.scala
     9.8    System/options.scala
     9.9    System/platform.scala
    9.10    System/posix_interrupt.scala