--- a/src/Pure/General/properties.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Pure/General/properties.scala Tue May 29 22:44:02 2012 +0200
@@ -52,7 +52,7 @@
props.find(_._1 == name).map(_._2)
}
- class Int(name: java.lang.String)
+ class Int(val name: java.lang.String)
{
def apply(value: scala.Int): T = List((name, Value.Int(value)))
def unapply(props: T): Option[scala.Int] =
@@ -62,7 +62,7 @@
}
}
- class Long(name: java.lang.String)
+ class Long(val name: java.lang.String)
{
def apply(value: scala.Long): T = List((name, Value.Long(value)))
def unapply(props: T): Option[scala.Long] =
@@ -72,7 +72,7 @@
}
}
- class Double(name: java.lang.String)
+ class Double(val name: java.lang.String)
{
def apply(value: scala.Double): T = List((name, Value.Double(value)))
def unapply(props: T): Option[scala.Double] =
--- a/src/Pure/PIDE/isabelle_markup.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Tue May 29 22:44:02 2012 +0200
@@ -236,6 +236,8 @@
val STDERR = "stderr"
val EXIT = "exit"
+ val Return_Code = new Properties.Int("return_code")
+
val LEGACY = "legacy"
val NO_REPORT = "no_report"
--- a/src/Pure/System/gui_setup.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Pure/System/gui_setup.scala Tue May 29 22:44:02 2012 +0200
@@ -55,7 +55,7 @@
val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
if (isabelle_home_windows != "")
text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
- text.append("Isabelle jdk home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
+ text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
}
catch { case ERROR(msg) => text.append(msg + "\n") }
--- a/src/Pure/System/isabelle_process.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue May 29 22:44:02 2012 +0200
@@ -77,7 +77,6 @@
class Isabelle_Process(
- timeout: Time = Time.seconds(25),
receiver: Isabelle_Process.Message => Unit = Console.println(_),
args: List[String] = Nil)
{
@@ -104,9 +103,10 @@
}
}
- private def output_message(kind: String, text: String)
+ private def exit_message(rc: Int)
{
- output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
+ output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
+ List(XML.Text("Return code: " + rc.toString)))
}
@@ -154,25 +154,25 @@
{
val (startup_failed, startup_errors) =
{
- val expired = System.currentTimeMillis() + timeout.ms
+ var finished: Option[Boolean] = None
val result = new StringBuilder(100)
-
- var finished: Option[Boolean] = None
- while (finished.isEmpty && System.currentTimeMillis() <= expired) {
+ while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
while (finished.isEmpty && process.stderr.ready) {
- val c = process.stderr.read
- if (c == 2) finished = Some(true)
- else result += c.toChar
+ try {
+ val c = process.stderr.read
+ if (c == 2) finished = Some(true)
+ else result += c.toChar
+ }
+ catch { case _: IOException => finished = Some(false) }
}
- if (process_result.is_finished) finished = Some(false)
- else Thread.sleep(10)
+ Thread.sleep(10)
}
(finished.isEmpty || !finished.get, result.toString.trim)
}
if (startup_errors != "") system_output(startup_errors)
if (startup_failed) {
- output_message(Isabelle_Markup.EXIT, "Return code: 127")
+ exit_message(127)
process.stdin.close
Thread.sleep(300)
terminate_process()
@@ -189,10 +189,11 @@
val rc = process_result.join
system_output("process terminated")
+ close_input()
for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
thread.join
system_output("process_manager terminated")
- output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
+ exit_message(rc)
}
system_channel.accepted()
}
@@ -204,7 +205,7 @@
def terminate()
{
- close()
+ close_input()
system_output("Terminating Isabelle process")
terminate_process()
}
@@ -263,7 +264,7 @@
else done = true
}
if (result.length > 0) {
- output_message(markup, result.toString)
+ output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
result.length = 0
}
else {
@@ -399,5 +400,5 @@
input_bytes(name, args.map(Standard_System.string_bytes): _*)
}
- def close(): Unit = { close(command_input); close(standard_input) }
+ def close_input(): Unit = { close(command_input); close(standard_input) }
}
--- a/src/Pure/System/session.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Pure/System/session.scala Tue May 29 22:44:02 2012 +0200
@@ -174,7 +174,7 @@
/* actor messages */
- private case class Start(timeout: Time, args: List[String])
+ private case class Start(args: List[String])
private case object Cancel_Execution
private case class Edit(edits: List[Document.Edit_Text])
private case class Change(
@@ -369,10 +369,12 @@
case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
prover_syntax += name
+ case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
+ if (rc == 0) phase = Session.Inactive
+ else phase = Session.Failed
+
case _ =>
- if (output.is_exit && phase == Session.Startup) phase = Session.Failed
- else if (output.is_exit) phase = Session.Inactive
- else if (output.is_init || output.is_stdout) { }
+ if (output.is_init || output.is_stdout) { }
else bad_output(output)
}
}
@@ -387,10 +389,10 @@
receiveWithin(delay_commands_changed.flush_timeout) {
case TIMEOUT => delay_commands_changed.flush()
- case Start(timeout, args) if prover.isEmpty =>
+ case Start(args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
+ prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
}
case Stop =>
@@ -444,10 +446,7 @@
/* actions */
- def start(timeout: Time, args: List[String])
- { session_actor ! Start(timeout, args) }
-
- def start(args: List[String]) { start (Time.seconds(25), args) }
+ def start(args: List[String]) { session_actor ! Start(args) }
def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
--- a/src/Tools/jEdit/lib/Tools/jedit Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue May 29 22:44:02 2012 +0200
@@ -22,8 +22,10 @@
"src/plugin.scala"
"src/protocol_dockable.scala"
"src/raw_output_dockable.scala"
+ "src/readme_dockable.scala"
"src/scala_console.scala"
"src/session_dockable.scala"
+ "src/syslog_dockable.scala"
"src/text_area_painter.scala"
"src/text_overview.scala"
"src/token_markup.scala"
@@ -260,7 +262,7 @@
if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
-<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
+<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
<?xml version="1.0" encoding="UTF-8" ?>
--- a/src/Tools/jEdit/src/Isabelle.props Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Tue May 29 22:44:02 2012 +0200
@@ -33,7 +33,6 @@
options.isabelle.tooltip-margin=60
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8.0
-options.isabelle.startup-timeout=25.0
options.isabelle.auto-start.title=Auto Start
options.isabelle.auto-start=true
@@ -51,17 +50,21 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
+isabelle.readme-panel.label=README panel
+isabelle.syslog-panel.label=Syslog panel
#dockables
isabelle-session.title=Prover Session
isabelle-output.title=Output
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
+isabelle-readme.title=README
+isabelle-syslog.title=Syslog
#SideKick
sidekick.parser.isabelle.label=Isabelle
--- a/src/Tools/jEdit/src/actions.xml Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/src/actions.xml Tue May 29 22:44:02 2012 +0200
@@ -7,6 +7,16 @@
wm.addDockableWindow("isabelle-session");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.syslog-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-syslog");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.readme-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-readme");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.output-panel">
<CODE>
wm.addDockableWindow("isabelle-output");
--- a/src/Tools/jEdit/src/dockables.xml Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Tue May 29 22:44:02 2012 +0200
@@ -5,6 +5,12 @@
<DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
new isabelle.jedit.Session_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
+ new isabelle.jedit.Syslog_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-readme" MOVABLE="TRUE">
+ new isabelle.jedit.README_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/jEdit.props Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Tue May 29 22:44:02 2012 +0200
@@ -181,6 +181,7 @@
isabelle-output.height=174
isabelle-output.width=412
isabelle-session.dock-position=bottom
+isabelle-readme.dock-position=bottom
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
--- a/src/Tools/jEdit/src/plugin.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue May 29 22:44:02 2012 +0200
@@ -295,14 +295,13 @@
def start_session()
{
- val timeout = Time_Property("startup-timeout", Time.seconds(25)) max Time.seconds(5)
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic = {
val logic = Property("logic")
if (logic != null && logic != "") logic
else Isabelle.default_logic()
}
- session.start(timeout, modes ::: List(logic))
+ session.start(modes ::: List(logic))
}
@@ -388,9 +387,8 @@
phase match {
case Session.Failed =>
Swing_Thread.later {
- Library.error_dialog(jEdit.getActiveView,
- "Failed to start Isabelle process",
- Library.scrollable_text(Isabelle.session.current_syslog()))
+ Library.error_dialog(jEdit.getActiveView, "Prover process failure",
+ "Isabelle Syslog", Library.scrollable_text(Isabelle.session.current_syslog()))
}
case Session.Ready =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/readme_dockable.scala Tue May 29 22:44:02 2012 +0200
@@ -0,0 +1,24 @@
+/* Title: Tools/jEdit/src/readme_dockable.scala
+ Author: Makarius
+
+Dockable window for README.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.View
+
+
+class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+ private val readme = new HTML_Panel("SansSerif", 14)
+ private val readme_path = Path.explode("$JEDIT_HOME/README.html")
+ readme.render_document(
+ Isabelle_System.platform_file_url(readme_path),
+ Isabelle_System.try_read(List(readme_path)))
+
+ set_content(readme)
+}
--- a/src/Tools/jEdit/src/session_dockable.scala Tue May 29 19:13:02 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue May 29 22:44:02 2012 +0200
@@ -10,8 +10,7 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
- ScrollPane, TabbedPane, Component, Swing}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, Component}
import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
import java.lang.System
@@ -24,15 +23,9 @@
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
{
- /* main tabs */
+ /* status */
- private val readme = new HTML_Panel("SansSerif", 14)
- private val readme_path = Path.explode("$JEDIT_HOME/README.html")
- readme.render_document(
- Isabelle_System.platform_file_url(readme_path),
- Isabelle_System.try_read(List(readme_path)))
-
- val status = new ListView(Nil: List[Document.Node.Name]) {
+ private val status = new ListView(Nil: List[Document.Node.Name]) {
listenTo(mouse.clicks)
reactions += {
case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
@@ -43,34 +36,20 @@
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
status.selection.intervalMode = ListView.IntervalMode.Single
- private val syslog = new TextArea(Isabelle.session.current_syslog())
-
- private val tabs = new TabbedPane {
- pages += new TabbedPane.Page("README", Component.wrap(readme))
- pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
- pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
-
- selection.index =
- {
- val index = Isabelle.Int_Property("session-panel.selection", 0)
- if (index >= pages.length) 0 else index
- }
- listenTo(selection)
- reactions += {
- case SelectionChanged(_) =>
- Isabelle.Int_Property("session-panel.selection") = selection.index
- }
- }
-
- set_content(tabs)
+ set_content(status)
/* controls */
- val session_phase = new Label(Isabelle.session.phase.toString)
+ private val session_phase = new Label(Isabelle.session.phase.toString)
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"
+ private def handle_phase(phase: Session.Phase)
+ {
+ Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
+ }
+
private val cancel = new Button("Cancel") {
reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
}
@@ -173,15 +152,7 @@
private val main_actor = actor {
loop {
react {
- case output: Isabelle_Process.Output =>
- if (output.is_syslog)
- Swing_Thread.later {
- val text = Isabelle.session.current_syslog()
- if (text != syslog.text) syslog.text = text
- }
-
- case phase: Session.Phase =>
- Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
+ case phase: Session.Phase => handle_phase(phase)
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
@@ -190,17 +161,15 @@
}
}
- override def init() {
- Isabelle.session.syslog_messages += main_actor
- Isabelle.session.phase_changed += main_actor
- Isabelle.session.commands_changed += main_actor
+ override def init()
+ {
+ Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
+ Isabelle.session.commands_changed += main_actor; handle_update()
}
- override def exit() {
- Isabelle.session.syslog_messages -= main_actor
+ override def exit()
+ {
Isabelle.session.phase_changed -= main_actor
Isabelle.session.commands_changed -= main_actor
}
-
- handle_update()
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Tue May 29 22:44:02 2012 +0200
@@ -0,0 +1,60 @@
+/* Title: Tools/jEdit/src/syslog_dockable.scala
+ Author: Makarius
+
+Dockable window for syslog.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.TextArea
+
+import java.lang.System
+
+import org.gjt.sp.jedit.View
+
+
+class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+ /* GUI components */
+
+ private val syslog = new TextArea()
+
+ private def update_syslog()
+ {
+ Swing_Thread.later {
+ val text = Isabelle.session.current_syslog()
+ if (text != syslog.text) syslog.text = text
+ }
+ }
+
+ set_content(syslog)
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case output: Isabelle_Process.Output =>
+ if (output.is_syslog) update_syslog()
+
+ case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Isabelle.session.syslog_messages += main_actor
+ update_syslog()
+ }
+
+ override def exit()
+ {
+ Isabelle.session.syslog_messages -= main_actor
+ }
+}