--- a/src/Pure/PIDE/document.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Pure/PIDE/document.scala Mon Sep 27 14:54:10 2010 +0200
@@ -136,8 +136,8 @@
val edits: List[Node_Text_Edit],
val result: Future[(List[Edit[Command]], Version)])
{
- val current: Future[Version] = result.map(_._2)
- def is_finished: Boolean = previous.is_finished && current.is_finished
+ val version: Future[Version] = result.map(_._2)
+ def is_finished: Boolean = previous.is_finished && version.is_finished
}
@@ -279,7 +279,7 @@
def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
{
val found_stable = history.undo_list.find(change =>
- change.is_finished && is_assigned(change.current.get_finished))
+ change.is_finished && is_assigned(change.version.get_finished))
require(found_stable.isDefined)
val stable = found_stable.get
val latest = history.undo_list.head
@@ -291,7 +291,7 @@
new Snapshot
{
- val version = stable.current.get_finished
+ val version = stable.version.get_finished
val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
--- a/src/Pure/System/cygwin.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Pure/System/cygwin.scala Mon Sep 27 14:54:10 2010 +0200
@@ -111,7 +111,9 @@
val setup_exe = new File(root, "setup.exe")
- try { Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe) }
+ try {
+ Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe)
+ }
catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
val (_, rc) = Standard_System.raw_exec(root, null, true,
--- a/src/Pure/System/download.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Pure/System/download.scala Mon Sep 27 14:54:10 2010 +0200
@@ -16,11 +16,11 @@
object Download
{
- def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
+ def stream(parent: Component, title: String, url: URL): (URLConnection, BufferedInputStream) =
{
val connection = url.openConnection
- val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
+ val stream = new ProgressMonitorInputStream(parent, title, connection.getInputStream)
val monitor = stream.getProgressMonitor
monitor.setNote(connection.getURL.toString)
@@ -30,14 +30,14 @@
(connection, new BufferedInputStream(stream))
}
- def file(parent: Component, url: URL, file: File)
+ def file(parent: Component, title: String, url: URL, file: File)
{
- val (connection, instream) = stream(parent, url)
+ val (connection, instream) = stream(parent, title, url)
val mod_time = connection.getLastModified
def read() =
try { instream.read }
- catch { case _ : InterruptedIOException => error("Download canceled!") }
+ catch { case _ : InterruptedIOException => error("Canceled by user") }
try {
val outstream = new BufferedOutputStream(new FileOutputStream(file))
try {
--- a/src/Pure/System/isabelle_system.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Sep 27 14:54:10 2010 +0200
@@ -315,10 +315,10 @@
val i = next_fifo()
val script =
"FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
- "mkfifo -m 600 \"$FIFO\" || { echo \"Failed to create fifo: $FIFO\" >&2; exit 2; }\n" +
- "echo -n \"$FIFO\"\n"
+ "echo -n \"$FIFO\"\n" +
+ "mkfifo -m 600 \"$FIFO\"\n"
val (out, err, rc) = bash(script)
- if (rc == 0) out else error(err)
+ if (rc == 0) out else error(err.trim)
}
def rm_fifo(fifo: String): Boolean =
--- a/src/Pure/System/session.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Pure/System/session.scala Mon Sep 27 14:54:10 2010 +0200
@@ -24,9 +24,10 @@
sealed abstract class Phase
case object Inactive extends Phase
- case object Exit extends Phase
+ case object Startup extends Phase // transient
+ case object Failed extends Phase
case object Ready extends Phase
- case object Shutdown extends Phase
+ case object Shutdown extends Phase // transient
}
@@ -46,7 +47,7 @@
/* pervasive event buses */
- val phase_changed = new Event_Bus[(Session.Phase, Session.Phase)]
+ val phase_changed = new Event_Bus[Session.Phase]
val global_settings = new Event_Bus[Session.Global_Settings.type]
val raw_messages = new Event_Bus[Isabelle_Process.Result]
val commands_changed = new Event_Bus[Session.Commands_Changed]
@@ -126,9 +127,8 @@
def phase = _phase
private def phase_=(new_phase: Session.Phase)
{
- val old_phase = _phase
_phase = new_phase
- phase_changed.event(old_phase, new_phase)
+ phase_changed.event(new_phase)
}
private val global_state = new Volatile(Document.State.init)
@@ -149,7 +149,7 @@
//{{{
{
val previous = change.previous.get_finished
- val (node_edits, current) = change.result.get_finished
+ val (node_edits, version) = change.result.get_finished
var former_assignment = global_state.peek().the_assignment(previous).get_finished
for {
@@ -180,8 +180,8 @@
}
(name -> Some(ids))
}
- global_state.change(_.define_version(current, former_assignment))
- prover.edit_version(previous.id, current.id, id_edits)
+ global_state.change(_.define_version(version, former_assignment))
+ prover.edit_version(previous.id, version.id, id_edits)
}
//}}}
@@ -209,10 +209,8 @@
if (result.is_syslog) {
reverse_syslog ::= result.message
if (result.is_ready) phase = Session.Ready
- else if (result.is_exit) {
- phase = Session.Exit
- phase = Session.Inactive
- }
+ else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
+ else if (result.is_exit) phase = Session.Inactive
}
else if (result.is_stdout) { }
else if (result.is_status) {
@@ -244,12 +242,12 @@
if (prover != null) prover.interrupt
case Edit_Version(edits) if prover != null =>
- val previous = global_state.peek().history.tip.current
+ val previous = global_state.peek().history.tip.version
val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
val change = global_state.change_yield(_.extend_history(previous, edits, result))
val this_actor = self
- change.current.map(_ => {
+ change.version.map(_ => {
assignments.await { global_state.peek().is_assigned(previous.get_finished) }
this_actor ! change })
@@ -260,13 +258,18 @@
case result: Isabelle_Process.Result => handle_result(result)
case Start(timeout, args) if prover == null =>
- prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
+ if (phase == Session.Inactive || phase == Session.Failed) {
+ phase = Session.Startup
+ prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
+ }
- case Stop if phase == Session.Ready =>
- global_state.change(_ => Document.State.init) // FIXME event bus!?
- phase = Session.Shutdown
- prover.terminate
- phase = Session.Inactive
+ case Stop =>
+ if (phase == Session.Ready) {
+ global_state.change(_ => Document.State.init) // FIXME event bus!?
+ phase = Session.Shutdown
+ prover.terminate
+ phase = Session.Inactive
+ }
finished = true
reply(())
--- a/src/Pure/System/standard_system.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Pure/System/standard_system.scala Mon Sep 27 14:54:10 2010 +0200
@@ -8,7 +8,8 @@
import java.util.regex.Pattern
import java.util.Locale
-import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
+import java.net.URL
+import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
File, FileFilter, IOException}
@@ -154,6 +155,65 @@
def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
: (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
+
+
+ /* unpack tar archive */
+
+ def posix_untar(url: URL, root: File, gunzip: Boolean = false,
+ tar: String = "tar", gzip: String = "", progress: Int => Unit = _ => ()): String =
+ {
+ if (!root.isDirectory && !root.mkdirs)
+ error("Failed to create root directory: " + root)
+
+ val connection = url.openConnection
+
+ val length = connection.getContentLength.toLong
+ require(length >= 0L)
+
+ val stream = new BufferedInputStream(connection.getInputStream)
+ val progress_stream = new InputStream {
+ private val total = length max 1L
+ private var index = 0L
+ private var percentage = 0L
+ override def read(): Int =
+ {
+ val c = stream.read
+ if (c != -1) {
+ index += 100
+ val p = index / total
+ if (percentage != p) { percentage = p; progress(percentage.toInt) }
+ }
+ c
+ }
+ override def available(): Int = stream.available
+ override def close() { stream.close }
+ }
+
+ val cmdline =
+ List(tar, "-o", "-x", "-f-") :::
+ (if (!gunzip) Nil else if (gzip == "") List("-z") else List("-I", gzip))
+
+ val proc = raw_execute(root, null, false, cmdline:_*)
+ val stdout = Simple_Thread.future("tar_stdout") { slurp(proc.getInputStream) }
+ val stderr = Simple_Thread.future("tar_stderr") { slurp(proc.getErrorStream) }
+ val stdin = new BufferedOutputStream(proc.getOutputStream)
+
+ try {
+ var c = -1
+ val io_err =
+ try { while ({ c = progress_stream.read; c != -1 }) stdin.write(c); false }
+ catch { case e: IOException => true }
+ stdin.close
+
+ val rc = try { proc.waitFor } finally { Thread.interrupted }
+ if (io_err || rc != 0) error(stderr.join.trim) else stdout.join
+ }
+ finally {
+ progress_stream.close
+ stdin.close
+ proc.destroy
+ }
+ }
}
--- a/src/Tools/jEdit/dist-template/etc/settings Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings Mon Sep 27 14:54:10 2010 +0200
@@ -6,7 +6,7 @@
JEDIT_OPTIONS="-reuseview -noserver -nobackground"
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8 -Dactors.enableForkJoin=false"
-JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
+JEDIT_SYSTEM_OPTIONS="-Dapple.awt.graphics.UseQuartz=true -Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
--- a/src/Tools/jEdit/plugin/Isabelle.props Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Sep 27 14:54:10 2010 +0200
@@ -32,6 +32,7 @@
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8000
options.isabelle.startup-timeout=10000
+options.isabelle.auto-start=true
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Sep 27 14:54:10 2010 +0200
@@ -208,16 +208,26 @@
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
- // background color: markup
+ // background color (1): markup
for {
Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
+ snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
+ // background color (2): markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
+ }
+
// sub-expression highlighting -- potentially from other snapshot
highlight_range match {
case Some((range, color)) if line_range.overlaps(range) =>
@@ -225,21 +235,11 @@
case None =>
case Some(r) =>
gfx.setColor(color)
- gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
+ gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
}
case _ =>
}
- // background boxes
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 2)
- }
-
// squiggly underline
for {
Text.Info(range, Some(color)) <-
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Mon Sep 27 14:54:10 2010 +0200
@@ -69,7 +69,7 @@
/* markup selectors */
private val subexp_include =
- Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
+ Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE)
val subexp: Markup_Tree.Select[(Text.Range, Color)] =
{
@@ -90,12 +90,12 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
}
- val background: Markup_Tree.Select[Color] =
+ val background1: Markup_Tree.Select[Color] =
{
case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
}
- val box: Markup_Tree.Select[Color] =
+ val background2: Markup_Tree.Select[Color] =
{
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
}
@@ -108,6 +108,7 @@
case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
+ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Sep 27 14:54:10 2010 +0200
@@ -201,8 +201,21 @@
case None =>
case Some(entry) => component.selection.item = entry
}
+ component.tooltip = "Isabelle logic image"
component
}
+
+ def start_session()
+ {
+ val timeout = Int_Property("startup-timeout") max 1000
+ val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+ val logic = {
+ val logic = Property("logic")
+ if (logic != null && logic != "") logic
+ else Isabelle.default_logic()
+ }
+ session.start(timeout, modes ::: List(logic))
+ }
}
@@ -210,20 +223,6 @@
{
/* session management */
- private def start_session()
- {
- if (Isabelle.session.phase == Session.Inactive) {
- val timeout = Isabelle.Int_Property("startup-timeout") max 1000
- val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
- val logic = {
- val logic = Isabelle.Property("logic")
- if (logic != null && logic != "") logic
- else Isabelle.default_logic()
- }
- Isabelle.session.start(timeout, modes ::: List(logic))
- }
- }
-
private def init_model(buffer: Buffer): Option[Document_Model] =
{
Document_Model(buffer) match {
@@ -262,14 +261,13 @@
private val session_manager = actor {
loop {
react {
- case (Session.Inactive, Session.Exit) =>
+ case Session.Failed =>
val text = new scala.swing.TextArea(Isabelle.session.syslog())
text.editable = false
Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
- case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
- case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
-
+ case Session.Ready => Isabelle.jedit_buffers.foreach(activate_buffer)
+ case Session.Shutdown => Isabelle.jedit_buffers.foreach(deactivate_buffer)
case _ =>
}
}
@@ -281,17 +279,18 @@
override def handleMessage(message: EBMessage)
{
message match {
- case msg: EditorStarted => start_session()
+ case msg: EditorStarted
+ if Isabelle.Boolean_Property("auto-start") => Isabelle.start_session()
case msg: BufferUpdate
- if Isabelle.session.phase == Session.Ready &&
+ if Isabelle.session.phase == Session.Ready && // FIXME race!?
msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
val buffer = msg.getBuffer
if (buffer != null) activate_buffer(buffer)
case msg: EditPaneUpdate
- if Isabelle.session.phase == Session.Ready &&
+ if Isabelle.session.phase == Session.Ready && // FIXME race!?
(msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED ||
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala Mon Sep 27 14:13:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Mon Sep 27 14:54:10 2010 +0200
@@ -11,10 +11,11 @@
import scala.actors.Actor._
import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
- Component, Swing}
+ Component, Swing, CheckBox}
import scala.swing.event.{ButtonClicked, SelectionChanged}
import java.awt.BorderLayout
+import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.View
@@ -51,8 +52,23 @@
/* controls */
val session_phase = new Label(Isabelle.session.phase.toString)
- session_phase.border = Swing.EtchedBorder(Swing.Lowered)
- session_phase.tooltip = "Prover process status"
+ session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
+ session_phase.tooltip = "Prover status"
+
+ private val auto_start = new CheckBox("Auto start") {
+ selected = Isabelle.Boolean_Property("auto-start")
+ reactions += {
+ case ButtonClicked(_) =>
+ Isabelle.Boolean_Property("auto-start") = selected
+ if (selected) Isabelle.start_session()
+ }
+ }
+
+ private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
+ logic.listenTo(logic.selection)
+ logic.reactions += {
+ case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
+ }
private val interrupt = new Button("Interrupt") {
reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
@@ -60,7 +76,7 @@
interrupt.tooltip = "Broadcast interrupt to all prover tasks"
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt)
+ new FlowPanel(FlowPanel.Alignment.Right)(session_phase, auto_start, logic, interrupt)
add(controls.peer, BorderLayout.NORTH)
@@ -78,8 +94,8 @@
}
}
- case (_, phase: Session.Phase) =>
- Swing_Thread.now { session_phase.text = phase.toString }
+ case phase: Session.Phase =>
+ Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
}