--- a/src/Pure/GUI/system_dialog.scala Tue Sep 29 23:43:35 2015 +0200
+++ /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
-}
--- a/src/Pure/build-jars Tue Sep 29 23:43:35 2015 +0200
+++ b/src/Pure/build-jars Wed Sep 30 14:32:26 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
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Sep 29 23:43:35 2015 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Sep 30 14:32:26 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"
--- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Sep 29 23:43:35 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Sep 30 14:32:26 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(_))))
}
}
-
--- a/src/Tools/jEdit/src/plugin.scala Tue Sep 29 23:43:35 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Sep 30 14:32:26 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 ||
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/session_build.scala Wed Sep 30 14:32:26 2015 +0200
@@ -0,0 +1,185 @@
+/* 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 "Exit") {
+ 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()
+
+ return_code(rc)
+ }
+ }
+}