# HG changeset patch # User wenzelm # Date 1378822173 -7200 # Node ID 3c977c570e20bda96f82c2d85f2b40aa50c9c8e9 # Parent abec1d118bc9339706cda118c8a12d0def2f5788 discontinued obsolete command-line tool "isabelle build_dialog"; diff -r abec1d118bc9 -r 3c977c570e20 lib/Tools/build_dialog --- a/lib/Tools/build_dialog Tue Sep 10 14:02:49 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,77 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Makarius -# -# DESCRIPTION: build Isabelle session images via GUI dialog - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS]" - echo - echo " Options are:" - echo " -L OPTION default logic via system option" - echo " -d DIR include session directory" - echo " -l NAME logic session name" - echo " -s system build mode: produce output in ISABELLE_HOME" - echo - echo " Build Isabelle logic session image via GUI dialog (default: $ISABELLE_LOGIC)." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -LOGIC_OPTION="" -declare -a INCLUDE_DIRS=() -LOGIC="" -SYSTEM_MODE=false - -while getopts "L:d:l:s" OPT -do - case "$OPT" in - L) - LOGIC_OPTION="$OPTARG" - ;; - d) - INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" - ;; - l) - LOGIC="$OPTARG" - ;; - s) - SYSTEM_MODE="true" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -# args - -[ "$#" -ne 0 ] && usage - - -## main - -isabelle_admin_build jars || exit $? - -"$ISABELLE_TOOL" java isabelle.Build_Dialog \ - "$LOGIC_OPTION" "$LOGIC" "$SYSTEM_MODE" "${INCLUDE_DIRS[@]}" - diff -r abec1d118bc9 -r 3c977c570e20 src/Doc/System/Interfaces.thy --- a/src/Doc/System/Interfaces.thy Tue Sep 10 14:02:49 2013 +0200 +++ b/src/Doc/System/Interfaces.thy Tue Sep 10 16:09:33 2013 +0200 @@ -32,10 +32,10 @@ directories may be included via option @{verbatim "-d"} to augment that name space (see also \secref{sec:tool-build}). - By default, the specified image is checked and built on demand, see - also @{tool build_dialog}. The @{verbatim "-s"} determines where to - store the result session image (see also \secref{sec:tool-build}). - The @{verbatim "-n"} option bypasses the session build dialog. + By default, the specified image is checked and built on demand. The + @{verbatim "-s"} option determines where to store the result session + image (see also \secref{sec:tool-build}). The @{verbatim "-n"} + option bypasses the session build dialog. The @{verbatim "-m"} option specifies additional print modes for the prover process. diff -r abec1d118bc9 -r 3c977c570e20 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue Sep 10 14:02:49 2013 +0200 +++ b/src/Doc/System/Sessions.thy Tue Sep 10 16:09:33 2013 +0200 @@ -419,31 +419,4 @@ \end{ttbox} *} - -section {* Build dialog *} - -text {* The @{tool_def build_dialog} provides a simple GUI wrapper to - the tool Isabelle @{tool build} tool. This enables user interfaces - like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made - logic image on startup. Its command-line usage is: -\begin{ttbox} -Usage: isabelle build_dialog [OPTIONS] LOGIC - - Options are: - -L OPTION default logic via system option - -d DIR include session directory - -l NAME logic session name - -s system build mode: produce output in ISABELLE_HOME - - Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC). -\end{ttbox} - - \medskip Option @{verbatim "-l"} specifies an explicit logic session - name. Option @{verbatim "-L"} specifies a system option name as - fall-back to determine the logic session name. If both are omitted - or have empty value, @{setting ISABELLE_LOGIC} is used as default. - - \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same - meaning as for the command-line @{tool build} tool itself. *} - end diff -r abec1d118bc9 -r 3c977c570e20 src/Pure/Tools/build_dialog.scala --- a/src/Pure/Tools/build_dialog.scala Tue Sep 10 14:02:49 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -/* Title: Pure/Tools/build_dialog.scala - Author: Makarius - -Dialog for session build process. -*/ - -package isabelle - - -import java.awt.{GraphicsEnvironment, Point, Font} - -import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, - BorderPanel, MainFrame, TextArea, SwingApplication, Component, Label} -import scala.swing.event.ButtonClicked - - -object Build_Dialog -{ - /* command line entry point */ - - def main(args: Array[String]) - { - GUI.init_laf() - try { - args.toList match { - case - logic_option :: - logic :: - Properties.Value.Boolean(system_mode) :: - include_dirs => - val options = Options.init() - val dirs = include_dirs.map(Path.explode(_)) - val session = - Isabelle_System.default_logic(logic, - if (logic_option != "") options.string(logic_option) else "") - - val system_dialog = new System_Dialog - dialog(options, system_dialog, system_mode, dirs, session) - system_dialog.join_exit - - case _ => error("Bad arguments:\n" + cat_lines(args)) - } - } - catch { - case exn: Throwable => - GUI.error_dialog(null, "Isabelle build failure", GUI.scrollable_text(Exn.message(exn))) - sys.exit(2) - } - } - - - /* dialog */ - - def dialog( - options: Options, - system_dialog: System_Dialog, - system_mode: Boolean, - dirs: List[Path], - session: String) - { - val more_dirs = dirs.map((false, _)) - - if (Build.build(options = options, build_heap = true, no_build = true, - more_dirs = more_dirs, sessions = List(session)) == 0) - system_dialog.return_code(0) - else { - system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") - system_dialog.echo("Build started for Isabelle/" + session + " ...") - - val (out, rc) = - try { - ("", - Build.build(options = options, progress = system_dialog, - build_heap = true, more_dirs = more_dirs, - system_mode = system_mode, sessions = List(session))) - } - catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } - - system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) - system_dialog.return_code(rc) - } - } -} - diff -r abec1d118bc9 -r 3c977c570e20 src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Tue Sep 10 14:02:49 2013 +0200 +++ b/src/Pure/Tools/main.scala Tue Sep 10 16:09:33 2013 +0200 @@ -7,7 +7,6 @@ package isabelle -import javax.swing.SwingUtilities import java.lang.{System, ClassLoader} import java.io.{File => JFile, BufferedReader, InputStreamReader} import java.nio.file.Files @@ -40,13 +39,32 @@ if (mode == "none") system_dialog.return_code(0) else { + val options = Options.init() val system_mode = mode == "" || mode == "system" - val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) - val options = Options.init() + val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _)) val session = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string("jedit_logic")) - Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session) + + if (Build.build(options = options, build_heap = true, no_build = true, + more_dirs = more_dirs, sessions = List(session)) == 0) + system_dialog.return_code(0) + else { + system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") + system_dialog.echo("Build started for Isabelle/" + session + " ...") + + val (out, rc) = + try { + ("", + Build.build(options = options, progress = system_dialog, + build_heap = true, more_dirs = more_dirs, + system_mode = system_mode, sessions = List(session))) + } + catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } + + system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) + system_dialog.return_code(rc) + } } } catch { case exn: Throwable => exit_error(exn) } diff -r abec1d118bc9 -r 3c977c570e20 src/Pure/build-jars --- a/src/Pure/build-jars Tue Sep 10 14:02:49 2013 +0200 +++ b/src/Pure/build-jars Tue Sep 10 16:09:33 2013 +0200 @@ -72,7 +72,6 @@ Thy/thy_load.scala Thy/thy_syntax.scala Tools/build.scala - Tools/build_dialog.scala Tools/doc.scala Tools/keywords.scala Tools/main.scala