# HG changeset patch # User wenzelm # Date 1285592050 -7200 # Node ID 6a64f04cb648b96dde8487e33dbffa7d2fabef51 # Parent 832c42be723e09933bc884376c0bf73bc601eede# Parent 1fa4c5c7d53412b630ca72e72c9724115d69512d merged diff -r 832c42be723e -r 6a64f04cb648 src/Pure/PIDE/document.scala --- 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) diff -r 832c42be723e -r 6a64f04cb648 src/Pure/System/cygwin.scala --- 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, diff -r 832c42be723e -r 6a64f04cb648 src/Pure/System/download.scala --- 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 { diff -r 832c42be723e -r 6a64f04cb648 src/Pure/System/isabelle_system.scala --- 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 = diff -r 832c42be723e -r 6a64f04cb648 src/Pure/System/session.scala --- 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(()) diff -r 832c42be723e -r 6a64f04cb648 src/Pure/System/standard_system.scala --- 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 + } + } } diff -r 832c42be723e -r 6a64f04cb648 src/Tools/jEdit/dist-template/etc/settings --- 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" diff -r 832c42be723e -r 6a64f04cb648 src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 832c42be723e -r 6a64f04cb648 src/Tools/jEdit/src/jedit/document_view.scala --- 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)) <- diff -r 832c42be723e -r 6a64f04cb648 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- 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" } diff -r 832c42be723e -r 6a64f04cb648 src/Tools/jEdit/src/jedit/plugin.scala --- 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 || diff -r 832c42be723e -r 6a64f04cb648 src/Tools/jEdit/src/jedit/session_dockable.scala --- 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) }