--- 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[@]}"
-
--- 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.
--- 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
--- 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)
- }
- }
-}
-
--- 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) }
--- 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