# HG changeset patch
# User wenzelm
# Date 1443648147 -7200
# Node ID d6e51df4e7f00ea8c81330157a0cd7345d32287f
# Parent 2f61e05ec124ec7facba98f1589c4688703efed0# Parent 371c117c2feabe54a29ba58a3b4560929f60c50c
merged
diff -r 2f61e05ec124 -r d6e51df4e7f0 Admin/PLATFORMS
--- a/Admin/PLATFORMS Wed Sep 30 17:17:53 2015 +0100
+++ b/Admin/PLATFORMS Wed Sep 30 23:22:27 2015 +0200
@@ -11,10 +11,10 @@
The basic Isabelle system infrastructure provides some facilities to
make this work, e.g. see the ML and Scala modules File and Path, or
functions like Isabelle_System.bash. The settings environment also
-provides some means for portability, e.g. the bash function "jvmpath"
-to keep the impression that Java on Windows/Cygwin adheres to
-Isabelle/POSIX standards, although inside the JVM itself there are
-many Windows-specific things.
+provides some means for portability, e.g. the bash function
+"platform_path" to keep the impression that Windows/Cygwin adheres to
+Isabelle/POSIX standards, although Poly/ML and the JVM are
+Windows-specific things.
When producing add-on tools, it is important to stay within this clean
room of Isabelle, and refrain from overly ambitious system hacking.
@@ -97,7 +97,7 @@
* Perl as largely portable system programming language, with its
fairly robust support for processes, signals, sockets etc.
-* Scala with Java 1.7. Isabelle/Scala irons out many oddities and
+* Scala with Java 1.8. Isabelle/Scala irons out many oddities and
portability issues of the Java platform.
diff -r 2f61e05ec124 -r d6e51df4e7f0 Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml Wed Sep 30 17:17:53 2015 +0100
+++ b/Admin/Windows/launch4j/isabelle.xml Wed Sep 30 23:22:27 2015 +0200
@@ -30,7 +30,7 @@
jdkOnly
{PLATFORM_BITS}
- -Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin"
+ -Disabelle.root="%EXEDIR%" -Dcygwin.root="%EXEDIR%\contrib\cygwin"
{SPLASH}
diff -r 2f61e05ec124 -r d6e51df4e7f0 NEWS
--- a/NEWS Wed Sep 30 17:17:53 2015 +0100
+++ b/NEWS Wed Sep 30 23:22:27 2015 +0200
@@ -408,6 +408,9 @@
- isabelle build: settings
ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64
+* Bash shell function "jvmpath" has been renamed to "platform_path": it
+is relevant both for Poly/ML and JVM processes.
+
New in Isabelle2015 (May 2015)
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/Tools/browser
--- a/lib/Tools/browser Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/Tools/browser Wed Sep 30 23:22:27 2015 +0200
@@ -86,9 +86,9 @@
esac
if [ -z "$OUTFILE" ]; then
- "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
+ "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
else
- "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
+ "$ISABELLE_TOOL" java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
fi
RC="$?"
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/Tools/getenv
--- a/lib/Tools/getenv Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/Tools/getenv Wed Sep 30 23:22:27 2015 +0200
@@ -76,7 +76,7 @@
fi
if [ -n "$DUMP" ]; then
- export PATH_JVM="$(jvmpath "$PATH")"
+ export PATH_JVM="$(platform_path "$PATH")"
exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
fi
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/Tools/java
--- a/lib/Tools/java Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/Tools/java Wed Sep 30 23:22:27 2015 +0200
@@ -10,5 +10,5 @@
unset CLASSPATH
isabelle_java java "${JAVA_ARGS[@]}" \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/Tools/scala
--- a/lib/Tools/scala Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/Tools/scala Wed Sep 30 23:22:27 2015 +0200
@@ -14,4 +14,4 @@
done
isabelle_scala scala "${SCALA_ARGS[@]}" \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/Tools/scalac
--- a/lib/Tools/scalac Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/Tools/scalac Wed Sep 30 23:22:27 2015 +0200
@@ -7,5 +7,5 @@
isabelle_admin_build jars || exit $?
isabelle_scala scalac -Dfile.encoding=UTF-8 \
- -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/browser/build
--- a/lib/browser/build Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/browser/build Wed Sep 30 23:22:27 2015 +0200
@@ -65,7 +65,7 @@
isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \
fail "Failed to compile sources"
- isabelle_jdk jar cf "$(jvmpath "$TARGET")" -C classes . ||
+ isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . ||
fail "Failed to produce $TARGET"
rm -rf classes
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/scripts/getsettings
--- a/lib/scripts/getsettings Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/scripts/getsettings Wed Sep 30 23:22:27 2015 +0200
@@ -36,8 +36,9 @@
USER_HOME="$(cygpath -u "$USERPROFILE")"
fi
- function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
- CYGWIN_ROOT="$(jvmpath "/")"
+ function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
+ CYGWIN_ROOT="$(platform_path "/")"
+ ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
unset CLASSPATH
@@ -46,7 +47,9 @@
USER_HOME="$HOME"
fi
- function jvmpath() { echo "$@"; }
+ ISABELLE_ROOT="$ISABELLE_HOME"
+
+ function platform_path() { echo "$@"; }
ISABELLE_CLASSPATH="$CLASSPATH"
unset CLASSPATH
diff -r 2f61e05ec124 -r d6e51df4e7f0 lib/scripts/run-polyml-5.5.3
--- a/lib/scripts/run-polyml-5.5.3 Wed Sep 30 17:17:53 2015 +0100
+++ b/lib/scripts/run-polyml-5.5.3 Wed Sep 30 23:22:27 2015 +0200
@@ -42,8 +42,8 @@
case "$ML_PLATFORM" in
*-windows)
- PLATFORM_INFILE="$(jvmpath -m "$INFILE")"
- PLATFORM_OUTFILE="$(jvmpath -m "$OUTFILE")"
+ PLATFORM_INFILE="$(platform_path -m "$INFILE")"
+ PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
;;
*)
PLATFORM_INFILE="$INFILE"
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala Wed Sep 30 17:17:53 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,188 +0,0 @@
-/* Title: Pure/GUI/system_dialog.scala
- Author: Makarius
-
-Dialog for system processes, with optional output window.
-*/
-
-package isabelle
-
-
-import java.awt.event.{WindowEvent, WindowAdapter}
-import javax.swing.{WindowConstants, JFrame, JDialog}
-
-import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
- BorderPanel, Frame, TextArea, Component, Label}
-import scala.swing.event.ButtonClicked
-
-
-class System_Dialog(owner: JFrame = null) extends Progress
-{
- /* component state -- owned by GUI thread */
-
- private var _title = "Isabelle"
- private var _window: Option[Window] = None
- private var _return_code: Option[Int] = None
-
- private def check_window(): Window =
- {
- GUI_Thread.require {}
-
- _window match {
- case Some(window) => window
- case None =>
- val window = new Window
- _window = Some(window)
-
- window.pack()
- window.setLocationRelativeTo(owner)
- window.setVisible(true)
-
- window
- }
- }
-
- private val result = Future.promise[Int]
-
- private def conclude()
- {
- GUI_Thread.require {}
- require(_return_code.isDefined)
-
- _window match {
- case None =>
- case Some(window) =>
- window.setVisible(false)
- window.dispose
- _window = None
- }
-
- try { result.fulfill(_return_code.get) }
- catch { case ERROR(_) => }
- }
-
- def join(): Int = result.join
- def join_exit(): Nothing = sys.exit(join)
-
-
- /* window */
-
- private class Window extends JDialog(owner, _title)
- {
- setIconImages(GUI.isabelle_images())
-
-
- /* text */
-
- val text = new TextArea {
- editable = false
- columns = 65
- rows = 24
- }
- text.font = (new Label).font
-
- val scroll_text = new ScrollPane(text)
-
-
- /* layout panel with dynamic actions */
-
- val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
- val layout_panel = new BorderPanel
- layout_panel.layout(scroll_text) = BorderPanel.Position.Center
- layout_panel.layout(action_panel) = BorderPanel.Position.South
-
- setContentPane(layout_panel.peer)
-
- def set_actions(cs: Component*)
- {
- action_panel.contents.clear
- action_panel.contents ++= cs
- layout_panel.revalidate
- layout_panel.repaint
- }
-
-
- /* close */
-
- setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
-
- addWindowListener(new WindowAdapter {
- override def windowClosing(e: WindowEvent) {
- if (_return_code.isDefined) conclude()
- else stopping()
- }
- })
-
- def stopping()
- {
- is_stopped = true
- set_actions(new Label("Stopping ..."))
- }
-
- val stop_button = new Button("Stop") {
- reactions += { case ButtonClicked(_) => stopping() }
- }
-
- var do_auto_close = true
- def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
-
- val auto_close = new CheckBox("Auto close") {
- reactions += {
- case ButtonClicked(_) => do_auto_close = this.selected
- if (can_auto_close) conclude()
- }
- }
- auto_close.selected = do_auto_close
- auto_close.tooltip = "Automatically close dialog when finished"
-
- set_actions(stop_button, auto_close)
-
-
- /* exit */
-
- val delay_exit =
- GUI_Thread.delay_first(Time.seconds(1.0))
- {
- if (can_auto_close) conclude()
- else {
- val button =
- new Button(if (_return_code == Some(0)) "OK" else "Exit") {
- reactions += { case ButtonClicked(_) => conclude() }
- }
- set_actions(button)
- button.peer.getRootPane.setDefaultButton(button.peer)
- }
- }
- }
-
-
- /* progress operations */
-
- def title(txt: String): Unit =
- GUI_Thread.later {
- _title = txt
- _window.foreach(window => window.setTitle(txt))
- }
-
- def return_code(rc: Int): Unit =
- GUI_Thread.later {
- _return_code = Some(rc)
- _window match {
- case None => conclude()
- case Some(window) => window.delay_exit.invoke
- }
- }
-
- override def echo(txt: String): Unit =
- GUI_Thread.later {
- val window = check_window()
- window.text.append(txt + "\n")
- val vertical = window.scroll_text.peer.getVerticalScrollBar
- vertical.setValue(vertical.getMaximum)
- }
-
- override def theory(session: String, theory: String): Unit =
- echo(session + ": theory " + theory)
-
- @volatile private var is_stopped = false
- override def stopped: Boolean = is_stopped
-}
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Pure/General/file.scala Wed Sep 30 23:22:27 2015 +0200
@@ -27,7 +27,7 @@
def standard_path(platform_path: String): String =
if (Platform.is_windows) {
val Platform_Root = new Regex("(?i)" +
- Pattern.quote(Isabelle_System.get_cygwin_root()) + """(?:\\+|\z)(.*)""")
+ Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
platform_path.replace('/', '\\') match {
@@ -71,7 +71,7 @@
result_path ++= root
rest
case path if path.startsWith("/") =>
- result_path ++= Isabelle_System.get_cygwin_root()
+ result_path ++= Isabelle_System.cygwin_root()
path
case path => path
}
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Pure/System/cygwin.scala Wed Sep 30 23:22:27 2015 +0200
@@ -15,73 +15,51 @@
object Cygwin
{
- /** Cygwin init (e.g. after extraction via 7zip) **/
-
- def init()
- {
- val isabelle_home0 = System.getenv("ISABELLE_HOME")
- if (isabelle_home0 == null || isabelle_home0 == "") {
+ /* init (e.g. after extraction via 7zip) */
- /* isabelle_home */
-
- val isabelle_home = System.getProperty("isabelle.home", "")
-
- if (isabelle_home == "")
- error("Unknown Isabelle home directory")
-
- if (!(new JFile(isabelle_home)).isDirectory)
- error("Bad Isabelle home directory: " + quote(isabelle_home))
+ def init(isabelle_root: String, cygwin_root: String)
+ {
+ require(Platform.is_windows)
- def execute(args: String*)
- {
- val cwd = new JFile(isabelle_home)
- val env = Map("CYGWIN" -> "nodosfilewarning")
- val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
- val (output, rc) = Isabelle_System.process_output(proc)
- if (rc != 0) error(output)
- }
+ def execute(args: String*)
+ {
+ val cwd = new JFile(isabelle_root)
+ val env = Map("CYGWIN" -> "nodosfilewarning")
+ val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+ val (output, rc) = Isabelle_System.process_output(proc)
+ if (rc != 0) error(output)
+ }
-
- /* cygwin_root */
-
- val cygwin_root = isabelle_home + "\\contrib\\cygwin"
- if ((new JFile(cygwin_root)).isDirectory)
- System.setProperty("cygwin.root", cygwin_root)
-
+ val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
+ val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
- /* init */
-
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+ if (uninitialized) {
+ val symlinks =
+ {
+ val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
+ Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+ }
+ @tailrec def recover_symlinks(list: List[String]): Unit =
+ {
+ list match {
+ case Nil | List("") =>
+ case link :: content :: rest =>
+ val path = (new JFile(isabelle_root, link)).toPath
- if (uninitialized) {
- val symlinks =
- {
- val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
- Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+ val writer = Files.newBufferedWriter(path, UTF8.charset)
+ try { writer.write("!" + content + "\u0000") }
+ finally { writer.close }
+
+ Files.setAttribute(path, "dos:system", true)
+
+ recover_symlinks(rest)
+ case _ => error("Unbalanced symlinks list")
}
- @tailrec def recover_symlinks(list: List[String]): Unit =
- {
- list match {
- case Nil | List("") =>
- case link :: content :: rest =>
- val path = (new JFile(isabelle_home, link)).toPath
-
- val writer = Files.newBufferedWriter(path, UTF8.charset)
- try { writer.write("!" + content + "\u0000") }
- finally { writer.close }
+ }
+ recover_symlinks(symlinks)
- Files.setAttribute(path, "dos:system", true)
-
- recover_symlinks(rest)
- case _ => error("Unbalanced symlinks list")
- }
- }
- recover_symlinks(symlinks)
-
- execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
- execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
- }
+ execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+ execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
}
}
}
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Sep 30 23:22:27 2015 +0200
@@ -29,17 +29,20 @@
else java_home
}
- private def find_cygwin_root(cygwin_root0: String = ""): String =
+ def bootstrap_directory(
+ preference: String, envar: String, property: String, description: String): String =
{
- require(Platform.is_windows)
+ def check(s: String): Option[String] =
+ if (s != null && s != "") Some(s) else None
- val cygwin_root1 = System.getenv("CYGWIN_ROOT")
- val cygwin_root2 = System.getProperty("cygwin.root")
+ val value =
+ check(preference) orElse // explicit argument
+ check(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
+ check(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
+ error("Unknown " + description + " directory")
- if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0
- else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
- else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
- else error("Cannot determine Cygwin root directory")
+ if ((new JFile(value)).isDirectory) value
+ else error("Bad " + description + " directory " + quote(value))
}
@@ -54,21 +57,24 @@
_settings.get
}
- /*
- Isabelle home precedence:
- (1) isabelle_home as explicit argument
- (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
- (3) isabelle.home system property (e.g. via JVM application boot process)
- */
- def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
+ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
if (_settings.isEmpty) {
import scala.collection.JavaConversions._
+ val isabelle_root1 =
+ bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
+
+ val cygwin_root1 =
+ if (Platform.is_windows)
+ bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
+ else ""
+
+ if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
+
def set_cygwin_root()
{
if (Platform.is_windows)
- _settings = Some(_settings.getOrElse(Map.empty) +
- ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
+ _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
}
set_cygwin_root()
@@ -81,7 +87,7 @@
{
val temp_windows =
{
- val temp = System.getenv("TEMP")
+ val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
}
val user_home = System.getProperty("user.home", "")
@@ -95,28 +101,18 @@
"ISABELLE_APP" -> "true")
}
- val system_home =
- if (isabelle_home != null && isabelle_home != "") isabelle_home
- else
- env.get("ISABELLE_HOME") match {
- case None | Some("") =>
- val path = System.getProperty("isabelle.home", "")
- if (path == "") error("Unknown Isabelle home directory")
- else path
- case Some(path) => path
- }
-
val settings =
{
val dump = JFile.createTempFile("settings", null)
dump.deleteOnExit
try {
- val shell_prefix =
- if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
- else Nil
- val cmdline =
- shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
- val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
+ val cmd1 =
+ if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
+ val cmd2 =
+ List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle",
+ "getenv", "-d", dump.toString)
+
+ val (output, rc) = process_output(raw_execute(null, env, true, (cmd1 ::: cmd2): _*))
if (rc != 0) error(output)
val entries =
@@ -146,7 +142,7 @@
else error("Undefined Isabelle environment variable: " + quote(name))
}
- def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+ def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
@@ -218,7 +214,7 @@
def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: args.toList
else args
val env1 = if (env == null) settings else settings ++ env
raw_execute(cwd, env1, redirect, cmdline: _*)
@@ -298,7 +294,7 @@
def kill(signal: String, group_pid: String): (String, Int) =
{
val bash =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\bash.exe")
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
process_output(raw_execute(null, null, true, cmdline: _*))
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Pure/Tools/main.scala Wed Sep 30 23:22:27 2015 +0200
@@ -19,10 +19,6 @@
val start =
{
try {
- /* system init */
-
- if (Platform.is_windows) Cygwin.init()
-
Isabelle_System.init()
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Pure/build-jars
--- a/src/Pure/build-jars Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Pure/build-jars Wed Sep 30 23:22:27 2015 +0200
@@ -24,7 +24,6 @@
GUI/html5_panel.scala
GUI/jfx_gui.scala
GUI/popup.scala
- GUI/system_dialog.scala
GUI/wrap_panel.scala
General/antiquote.scala
General/bytes.scala
@@ -239,7 +238,7 @@
(
classpath "$JAVA_HOME/lib/jfxrt.jar"
classpath classes
- export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
+ export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
if [ "$TEST_PIDE" = true ]; then
isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
@@ -263,7 +262,7 @@
cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/.
cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/.
- isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.Main META-INF isabelle || \
+ isabelle_jdk jar cfe "$(platform_path "$TARGET")" isabelle.Main META-INF isabelle || \
fail "Failed to produce $TARGET"
popd >/dev/null
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Sep 30 23:22:27 2015 +0200
@@ -55,6 +55,7 @@
"src/rendering.scala"
"src/rich_text_area.scala"
"src/scala_console.scala"
+ "src/session_build.scala"
"src/simplifier_trace_dockable.scala"
"src/simplifier_trace_window.scala"
"src/sledgehammer_dockable.scala"
@@ -196,10 +197,10 @@
# args
if [ "$#" -eq 0 ]; then
- ARGS["${#ARGS[@]}"]="$(jvmpath "$USER_HOME/Scratch.thy")"
+ ARGS["${#ARGS[@]}"]="$(platform_path "$USER_HOME/Scratch.thy")"
else
while [ "$#" -gt 0 ]; do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
shift
done
fi
@@ -331,7 +332,7 @@
do
classpath "$JAR"
done
- export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
+ export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
) || fail "Failed to compile sources"
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Tools/jEdit/lib/Tools/jedit_client
--- a/src/Tools/jEdit/lib/Tools/jedit_client Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit_client Wed Sep 30 23:22:27 2015 +0200
@@ -85,7 +85,7 @@
while [ "$#" -gt 0 ]
do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
shift
done
@@ -109,7 +109,7 @@
if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
then
exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" -jar "$JEDIT_HOME/dist/jedit.jar" \
- "-settings=$(jvmpath "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
+ "-settings=$(platform_path "$JEDIT_SETTINGS")" -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
else
fail "Isabelle/jEdit server \"$SERVER_NAME\" not active"
fi
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Sep 30 23:22:27 2015 +0200
@@ -1,7 +1,7 @@
/* Title: Tools/jEdit/src/isabelle_logic.scala
Author: Makarius
-Isabellel logic session.
+Isabelle logic session.
*/
package isabelle.jedit
@@ -17,7 +17,7 @@
{
private val option_name = "jedit_logic"
- private def jedit_logic(): String =
+ def session_name(): String =
Isabelle_System.default_logic(
Isabelle_System.getenv("JEDIT_LOGIC"),
PIDE.options.string(option_name))
@@ -32,7 +32,7 @@
GUI_Thread.require {}
val entries =
- new Logic_Entry("", "default (" + jedit_logic() + ")") ::
+ new Logic_Entry("", "default (" + session_name() + ")") ::
Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
val component = new ComboBox(entries) with Option_Component {
@@ -58,13 +58,23 @@
component
}
- def session_args(): List[String] =
+ def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+
+ def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
{
- val modes =
+ val mode = session_build_mode()
+
+ Build.build(options = PIDE.options.value, progress = progress,
+ build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
+ dirs = session_dirs(), sessions = List(session_name()))
+ }
+
+ def session_start()
+ {
+ val print_modes =
space_explode(',', PIDE.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))
-
- modes.map("-m" + _) ::: List("-r", "-q", jedit_logic())
+ PIDE.session.start("Isabelle", print_modes.map("-m" + _) ::: List("-r", "-q", session_name()))
}
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
@@ -79,11 +89,9 @@
def session_content(inlined_files: Boolean): Build.Session_Content =
{
- val dirs = session_dirs()
- val name = session_args().last
- val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name)
+ val content =
+ Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
content.copy(known_theories =
content.known_theories.mapValues(name => name.map(File.platform_path(_))))
}
}
-
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala Wed Sep 30 17:17:53 2015 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Sep 30 23:22:27 2015 +0200
@@ -262,59 +262,6 @@
}
- /* session build */
-
- def session_build(): Int =
- {
- val system_dialog = new System_Dialog(jEdit.getActiveView())
-
- try {
- val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
- if (mode == "none")
- system_dialog.return_code(0)
- else {
- val system_mode = mode == "" || mode == "system"
- val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
- val session = Isabelle_System.default_logic(
- Isabelle_System.getenv("JEDIT_LOGIC"),
- PIDE.options.string("jedit_logic"))
-
- if (Build.build(options = PIDE.options.value, build_heap = true, no_build = true,
- dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0)
- system_dialog.return_code(0)
- else {
- system_dialog.title("Isabelle build (" +
- Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
- "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
- system_dialog.echo("Build started for Isabelle/" + session + " ...")
-
- val (out, rc) =
- try {
- ("",
- Build.build(options = PIDE.options.value, progress = system_dialog,
- build_heap = true, dirs = dirs, system_mode = system_mode,
- sessions = List(session)))
- }
- catch {
- case exn: Throwable =>
- (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
- }
-
- system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
- system_dialog.return_code(rc)
- }
- }
- }
- catch {
- case exn: Throwable =>
- GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
- system_dialog.return_code(Exn.return_code(exn, 2))
- }
-
- system_dialog.join()
- }
-
-
/* session phase */
private val session_phase =
@@ -379,10 +326,7 @@
"It is for testing only, not for production use.")
}
- Simple_Thread.fork("session_build") {
- val rc = session_build()
- if (rc == 0) PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
- }
+ Session_Build.session_build(jEdit.getActiveView())
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED ||
@@ -440,6 +384,7 @@
Debug.DISABLE_SEARCH_DIALOG_POOL = true
PIDE.plugin = this
+ Isabelle_System.init()
GUI.install_fonts()
PIDE.options.update(Options.init())
diff -r 2f61e05ec124 -r d6e51df4e7f0 src/Tools/jEdit/src/session_build.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/session_build.scala Wed Sep 30 23:22:27 2015 +0200
@@ -0,0 +1,187 @@
+/* Title: Tools/jEdit/src/session_build.scala
+ Author: Makarius
+
+Session build management.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.event.{WindowEvent, WindowAdapter}
+import javax.swing.{WindowConstants, JDialog}
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+ BorderPanel, TextArea, Component, Label}
+import scala.swing.event.ButtonClicked
+
+import org.gjt.sp.jedit.View
+
+
+object Session_Build
+{
+ def session_build(view: View)
+ {
+ GUI_Thread.require {}
+
+ try {
+ if (Isabelle_Logic.session_build_mode() == "none" ||
+ Isabelle_Logic.session_build(no_build = true) == 0) Isabelle_Logic.session_start()
+ else new Dialog(view)
+ }
+ catch {
+ case exn: Throwable =>
+ GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ }
+ }
+
+ private class Dialog(view: View) extends JDialog(view)
+ {
+ /* text */
+
+ private val text = new TextArea {
+ editable = false
+ columns = 65
+ rows = 24
+ }
+ text.font = (new Label).font
+
+ private val scroll_text = new ScrollPane(text)
+
+
+ /* progress */
+
+ @volatile private var is_stopped = false
+
+ private val progress = new Progress {
+ override def echo(txt: String): Unit =
+ GUI_Thread.later {
+ text.append(txt + "\n")
+ val vertical = scroll_text.peer.getVerticalScrollBar
+ vertical.setValue(vertical.getMaximum)
+ }
+
+ override def theory(session: String, theory: String): Unit =
+ echo(session + ": theory " + theory)
+
+ override def stopped: Boolean = is_stopped
+ }
+
+
+ /* layout panel with dynamic actions */
+
+ private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
+ private val layout_panel = new BorderPanel
+ layout_panel.layout(scroll_text) = BorderPanel.Position.Center
+ layout_panel.layout(action_panel) = BorderPanel.Position.South
+
+ setContentPane(layout_panel.peer)
+
+ private def set_actions(cs: Component*)
+ {
+ action_panel.contents.clear
+ action_panel.contents ++= cs
+ layout_panel.revalidate
+ layout_panel.repaint
+ }
+
+
+ /* return code and exit */
+
+ private var _return_code: Option[Int] = None
+
+ private def return_code(rc: Int): Unit =
+ GUI_Thread.later {
+ _return_code = Some(rc)
+ delay_exit.invoke
+ }
+
+ private val delay_exit =
+ GUI_Thread.delay_first(Time.seconds(1.0))
+ {
+ if (can_auto_close) conclude()
+ else {
+ val button =
+ new Button(if (_return_code == Some(0)) "OK" else "Close") {
+ reactions += { case ButtonClicked(_) => conclude() }
+ }
+ set_actions(button)
+ button.peer.getRootPane.setDefaultButton(button.peer)
+ }
+ }
+
+ private def conclude()
+ {
+ setVisible(false)
+ dispose()
+ }
+
+
+ /* close */
+
+ setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
+
+ addWindowListener(new WindowAdapter {
+ override def windowClosing(e: WindowEvent) {
+ if (_return_code.isDefined) conclude()
+ else stopping()
+ }
+ })
+
+ private def stopping()
+ {
+ is_stopped = true
+ set_actions(new Label("Stopping ..."))
+ }
+
+ private val stop_button = new Button("Stop") {
+ reactions += { case ButtonClicked(_) => stopping() }
+ }
+
+ private var do_auto_close = true
+ private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
+
+ private val auto_close = new CheckBox("Auto close") {
+ reactions += {
+ case ButtonClicked(_) => do_auto_close = this.selected
+ if (can_auto_close) conclude()
+ }
+ }
+ auto_close.selected = do_auto_close
+ auto_close.tooltip = "Automatically close dialog when finished"
+
+ set_actions(stop_button, auto_close)
+
+
+ /* main */
+
+ setIconImages(GUI.isabelle_images())
+
+ setTitle("Isabelle build (" +
+ Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
+ "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
+
+ pack()
+ setLocationRelativeTo(view)
+ setVisible(true)
+
+ Simple_Thread.fork("session_build") {
+ progress.echo("Build started for Isabelle/" + Isabelle_Logic.session_name() + " ...")
+
+ val (out, rc) =
+ try { ("", Isabelle_Logic.session_build(progress = progress)) }
+ catch {
+ case exn: Throwable =>
+ (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
+ }
+
+ progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+
+ if (rc == 0) Isabelle_Logic.session_start()
+ else progress.echo("Build failed -- prover remains inactive!")
+
+ return_code(rc)
+ }
+ }
+}