# HG changeset patch # User wenzelm # Date 1273091025 -7200 # Node ID ac7961d42ac35f0b6bae8b97142a273ad9a8ace3 # Parent 806ea6e282e4673d7fee5947f1e262dcb5673eab some rearrangement of Scala sources; diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/General/download.scala --- a/src/Pure/General/download.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -/* Title: Pure/General/download.scala - Author: Makarius - -Download URLs -- with progress monitor. -*/ - -package isabelle - - -import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, - File, InterruptedIOException} -import java.net.{URL, URLConnection} -import java.awt.{Component, HeadlessException} -import javax.swing.ProgressMonitorInputStream - - -object Download -{ - def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) = - { - val connection = url.openConnection - - val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream) - val monitor = stream.getProgressMonitor - monitor.setNote(connection.getURL.toString) - - val length = connection.getContentLength - if (length != -1) monitor.setMaximum(length) - - (connection, new BufferedInputStream(stream)) - } - - def file(parent: Component, url: URL, file: File) - { - val (connection, instream) = stream(parent, url) - val mod_time = connection.getLastModified - - def read() = - try { instream.read } - catch { case _ : InterruptedIOException => error("Download canceled!") } - try { - val outstream = new BufferedOutputStream(new FileOutputStream(file)) - try { - var c: Int = 0 - while ({ c = read(); c != -1}) outstream.write(c) - } - finally { outstream.close } - if (mod_time > 0) file.setLastModified(mod_time) - } - finally { instream.close } - } -} - diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/General/event_bus.scala --- a/src/Pure/General/event_bus.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -/* Title: Pure/General/event_bus.scala - Author: Makarius - -Generic event bus with multiple receiving actors. -*/ - -package isabelle - -import scala.actors.Actor, Actor._ -import scala.collection.mutable.ListBuffer - - -class Event_Bus[Event] -{ - /* receivers */ - - private val receivers = new ListBuffer[Actor] - - def += (r: Actor) { synchronized { receivers += r } } - def + (r: Actor): Event_Bus[Event] = { this += r; this } - - def += (f: Event => Unit) { - this += actor { loop { react { case x: Event => f(x) } } } - } - - def + (f: Event => Unit): Event_Bus[Event] = { this += f; this } - - def -= (r: Actor) { synchronized { receivers -= r } } - def - (r: Actor) = { this -= r; this } - - - /* event invocation */ - - def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } -} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/General/swing_thread.scala --- a/src/Pure/General/swing_thread.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -/* Title: Pure/General/swing_thread.scala - Author: Makarius - Author: Fabian Immler, TU Munich - -Evaluation within the AWT/Swing thread. -*/ - -package isabelle - -import javax.swing.{SwingUtilities, Timer} -import java.awt.event.{ActionListener, ActionEvent} - - -object Swing_Thread -{ - /* checks */ - - def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) - def require() = Predef.require(SwingUtilities.isEventDispatchThread()) - - - /* main dispatch queue */ - - def now[A](body: => A): A = - { - var result: Option[A] = None - if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } - else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) - result.get - } - - def future[A](body: => A): Future[A] = - { - if (SwingUtilities.isEventDispatchThread()) Future.value(body) - else Future.fork { now(body) } - } - - def later(body: => Unit) - { - if (SwingUtilities.isEventDispatchThread()) body - else SwingUtilities.invokeLater(new Runnable { def run = body }) - } - - - /* delayed actions */ - - private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit = - { - val listener = - new ActionListener { override def actionPerformed(e: ActionEvent) { action } } - val timer = new Timer(time_span, listener) - timer.setRepeats(false) - - def invoke() { if (first) timer.start() else timer.restart() } - invoke _ - } - - // delayed action after first invocation - def delay_first = delayed_action(true) _ - - // delayed action after last invocation - def delay_last = delayed_action(false) _ -} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/change.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/change.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,42 @@ +/* Title: Pure/PIDE/change.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Changes of plain text. +*/ + +package isabelle + + +class Change( + val id: Isar_Document.Document_ID, + val parent: Option[Change], + val edits: List[Text_Edit], + val result: Future[(List[Document.Edit], Document)]) +{ + def ancestors: Iterator[Change] = new Iterator[Change] + { + private var state: Option[Change] = Some(Change.this) + def hasNext = state.isDefined + def next = + state match { + case Some(change) => state = change.parent; change + case None => throw new NoSuchElementException("next on empty iterator") + } + } + + def join_document: Document = result.join._2 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished + + def edit(session: Session, edits: List[Text_Edit]): Change = + { + val new_id = session.create_id() + val result: Future[(List[Document.Edit], Document)] = + Future.fork { + val old_doc = join_document + old_doc.await_assignment + Document.text_edits(session, old_doc, new_id, edits) + } + new Change(new_id, Some(this), edits, result) + } +} \ No newline at end of file diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/command.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/command.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,101 @@ +/* Title: Pure/PIDE/command.scala + Author: Johannes Hölzl, TU Munich + Author: Fabian Immler, TU Munich + Author: Makarius + +Prover commands with semantic state. +*/ + +package isabelle + + +import scala.actors.Actor, Actor._ +import scala.collection.mutable + + +object Command +{ + object Status extends Enumeration + { + val UNPROCESSED = Value("UNPROCESSED") + val FINISHED = Value("FINISHED") + val FAILED = Value("FAILED") + } + + case class HighlightInfo(highlight: String) { override def toString = highlight } + case class TypeInfo(ty: String) + case class RefInfo(file: Option[String], line: Option[Int], + command_id: Option[String], offset: Option[Int]) +} + + +class Command( + val id: Isar_Document.Command_ID, + val span: Thy_Syntax.Span) + extends Session.Entity +{ + /* classification */ + + def is_command: Boolean = !span.isEmpty && span.head.is_command + def is_ignored: Boolean = span.forall(_.is_ignored) + def is_malformed: Boolean = !is_command && !is_ignored + + def name: String = if (is_command) span.head.content else "" + override def toString = if (is_command) name else if (is_ignored) "" else "" + + + /* source text */ + + val source: String = span.map(_.source).mkString + def source(i: Int, j: Int): String = source.substring(i, j) + def length: Int = source.length + + lazy val symbol_index = new Symbol.Index(source) + + + /* accumulated messages */ + + @volatile protected var state = new State(this) + def current_state: State = state + + private case class Consume(session: Session, message: XML.Tree) + private case object Assign + + private val accumulator = actor { + var assigned = false + loop { + react { + case Consume(session: Session, message: XML.Tree) if !assigned => + state = state.+(session, message) + + case Assign => + assigned = true // single assignment + reply(()) + + case bad => System.err.println("command accumulator: ignoring bad message " + bad) + } + } + } + + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } + + def assign_state(state_id: Isar_Document.State_ID): Command = + { + val cmd = new Command(state_id, span) + accumulator !? Assign + cmd.state = current_state + cmd + } + + + /* markup */ + + lazy val empty_markup = new Markup_Text(Nil, source) + + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = + { + val start = symbol_index.decode(begin) + val stop = symbol_index.decode(end) + new Markup_Tree(new Markup_Node(start, stop, info), Nil) + } +} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/document.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/document.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,197 @@ +/* Title: Pure/PIDE/document.scala + Author: Makarius + +Document as editable list of commands. +*/ + +package isabelle + + +object Document +{ + /* command start positions */ + + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] = + { + var offset = 0 + for (cmd <- commands.iterator) yield { + val start = offset + offset += cmd.length + (cmd, start) + } + } + + + /* empty document */ + + def empty(id: Isar_Document.Document_ID): Document = + { + val doc = new Document(id, Linear_Set(), Map()) + doc.assign_states(Nil) + doc + } + + + // FIXME + var phase0: List[Text_Edit] = null + var phase1: Linear_Set[Command] = null + var phase2: Linear_Set[Command] = null + var phase3: List[Edit] = null + + + + /** document edits **/ + + type Edit = (Option[Command], Option[Command]) + + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, + edits: List[Text_Edit]): (List[Edit], Document) = + { + require(old_doc.assignment.is_finished) + + + /* unparsed dummy commands */ + + def unparsed(source: String) = + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) + + def is_unparsed(command: Command) = command.id == null + + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove + + + /* phase 1: edit individual command source */ + + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = + { + eds match { + case e :: es => + command_starts(commands).find { // FIXME relative search! + case (cmd, cmd_start) => + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length + } match { + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => + val (rest, text) = e.edit(cmd.source, cmd_start) + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd + edit_text(rest.toList ::: es, new_commands) + + case Some((cmd, cmd_start)) => + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) + + case None => + require(e.is_insert && e.start == 0) + edit_text(es, commands.insert_after(None, unparsed(e.text))) + } + case Nil => commands + } + } + + + /* phase 2: recover command spans */ + + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = + { + // FIXME relative search! + commands.iterator.find(is_unparsed) match { + case Some(first_unparsed) => + val prefix = commands.prev(first_unparsed) + val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList + val suffix = commands.next(body.last) + + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) + + val (before_edit, spans1) = + if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) + (prefix, spans0.tail) + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) + + val (after_edit, spans2) = + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) + (suffix, spans1.take(spans1.length - 1)) + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) + + val inserted = spans2.map(span => new Command(session.create_id(), span)) + val new_commands = + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) + parse_spans(new_commands) + + case None => commands + } + } + + + /* phase 3: resulting document edits */ + + val result = Library.timeit("text_edits") { + val commands0 = old_doc.commands + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) } + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) } + + val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList + val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList + + val doc_edits = + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) + + val former_states = old_doc.assignment.join -- removed_commands + + phase0 = edits + phase1 = commands1 + phase2 = commands2 + phase3 = doc_edits + + (doc_edits, new Document(new_id, commands2, former_states)) + } + result + } +} + + +class Document( + val id: Isar_Document.Document_ID, + val commands: Linear_Set[Command], + former_states: Map[Command, Command]) +{ + /* command ranges */ + + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) + + def command_start(cmd: Command): Option[Int] = + command_starts.find(_._1 == cmd).map(_._2) + + def command_range(i: Int): Iterator[(Command, Int)] = + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } + + def command_range(i: Int, j: Int): Iterator[(Command, Int)] = + command_range(i) takeWhile { case (_, start) => start < j } + + def command_at(i: Int): Option[(Command, Int)] = + { + val range = command_range(i) + if (range.hasNext) Some(range.next) else None + } + + + /* command state assignment */ + + val assignment = Future.promise[Map[Command, Command]] + def await_assignment { assignment.join } + + @volatile private var tmp_states = former_states + private val time0 = System.currentTimeMillis + + def assign_states(new_states: List[(Command, Command)]) + { + assignment.fulfill(tmp_states ++ new_states) + tmp_states = Map() + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") + } + + def current_state(cmd: Command): Option[State] = + { + require(assignment.is_finished) + (assignment.join).get(cmd).map(_.current_state) + } +} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/event_bus.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/event_bus.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,35 @@ +/* Title: Pure/PIDE/event_bus.scala + Author: Makarius + +Generic event bus with multiple receiving actors. +*/ + +package isabelle + +import scala.actors.Actor, Actor._ +import scala.collection.mutable.ListBuffer + + +class Event_Bus[Event] +{ + /* receivers */ + + private val receivers = new ListBuffer[Actor] + + def += (r: Actor) { synchronized { receivers += r } } + def + (r: Actor): Event_Bus[Event] = { this += r; this } + + def += (f: Event => Unit) { + this += actor { loop { react { case x: Event => f(x) } } } + } + + def + (f: Event => Unit): Event_Bus[Event] = { this += f; this } + + def -= (r: Actor) { synchronized { receivers -= r } } + def - (r: Actor) = { this -= r; this } + + + /* event invocation */ + + def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } +} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/markup_node.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/markup_node.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,111 @@ +/* Title: Pure/PIDE/markup_node.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Document markup nodes, with connection to Swing tree model. +*/ + +package isabelle + + +import javax.swing.tree.DefaultMutableTreeNode + + + +class Markup_Node(val start: Int, val stop: Int, val info: Any) +{ + def fits_into(that: Markup_Node): Boolean = + that.start <= this.start && this.stop <= that.stop +} + + +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) +{ + def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs) + + private def add(branch: Markup_Tree) = // FIXME avoid sort + set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start)) + + private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs) + + def + (new_tree: Markup_Tree): Markup_Tree = + { + val new_node = new_tree.node + if (new_node fits_into node) { + var inserted = false + val new_branches = + branches.map(branch => + if ((new_node fits_into branch.node) && !inserted) { + inserted = true + branch + new_tree + } + else branch) + if (!inserted) { + // new_tree did not fit into children of this + // -> insert between this and its branches + val fitting = branches filter(_.node fits_into new_node) + (this remove fitting) add ((new_tree /: fitting)(_ + _)) + } + else set_branches(new_branches) + } + else { + System.err.println("ignored nonfitting markup: " + new_node) + this + } + } + + def flatten: List[Markup_Node] = + { + var next_x = node.start + if (branches.isEmpty) List(this.node) + else { + val filled_gaps = + for { + child <- branches + markups = + if (next_x < child.node.start) + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten + else child.flatten + update = (next_x = child.node.stop) + markup <- markups + } yield markup + if (next_x < node.stop) + filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) + else filled_gaps + } + } +} + + +class Markup_Text(val markup: List[Markup_Tree], val content: String) +{ + private lazy val root = + new Markup_Tree(new Markup_Node(0, content.length, None), markup) + + def + (new_tree: Markup_Tree): Markup_Text = + new Markup_Text((root + new_tree).branches, content) + + def filter(pred: Markup_Node => Boolean): Markup_Text = + { + def filt(tree: Markup_Tree): List[Markup_Tree] = + { + val branches = tree.branches.flatMap(filt(_)) + if (pred(tree.node)) List(tree.set_branches(branches)) + else branches + } + new Markup_Text(markup.flatMap(filt(_)), content) + } + + def flatten: List[Markup_Node] = markup.flatten(_.flatten) + + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = + { + def swing(tree: Markup_Tree): DefaultMutableTreeNode = + { + val node = swing_node(tree.node) + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) + node + } + swing(root) + } +} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/state.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/state.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,117 @@ +/* Title: Pure/PIDE/state.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Accumulating results from prover. +*/ + +package isabelle + + +class State( + val command: Command, + val status: Command.Status.Value, + val rev_results: List[XML.Tree], + val markup_root: Markup_Text) +{ + def this(command: Command) = + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup) + + + /* content */ + + private def set_status(st: Command.Status.Value): State = + new State(command, st, rev_results, markup_root) + + private def add_result(res: XML.Tree): State = + new State(command, status, res :: rev_results, markup_root) + + private def add_markup(node: Markup_Tree): State = + new State(command, status, rev_results, markup_root + node) + + lazy val results = rev_results.reverse + + + /* markup */ + + lazy val highlight: Markup_Text = + { + markup_root.filter(_.info match { + case Command.HighlightInfo(_) => true + case _ => false + }) + } + + private lazy val types: List[Markup_Node] = + markup_root.filter(_.info match { + case Command.TypeInfo(_) => true + case _ => false }).flatten + + def type_at(pos: Int): Option[String] = + { + types.find(t => t.start <= pos && pos < t.stop) match { + case Some(t) => + t.info match { + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty) + case _ => None + } + case None => None + } + } + + private lazy val refs: List[Markup_Node] = + markup_root.filter(_.info match { + case Command.RefInfo(_, _, _, _) => true + case _ => false }).flatten + + def ref_at(pos: Int): Option[Markup_Node] = + refs.find(t => t.start <= pos && pos < t.stop) + + + /* message dispatch */ + + def + (session: Session, message: XML.Tree): State = + { + val changed: State = + message match { + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => + (this /: elems)((state, elem) => + elem match { + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) + case XML.Elem(kind, atts, body) => + val (begin, end) = Position.get_offsets(atts) + if (begin.isEmpty || end.isEmpty) state + else if (kind == Markup.ML_TYPING) { + val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!? + state.add_markup( + command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info))) + } + else if (kind == Markup.ML_REF) { + body match { + case List(XML.Elem(Markup.ML_DEF, atts, _)) => + state.add_markup(command.markup_node( + begin.get - 1, end.get - 1, + Command.RefInfo( + Position.get_file(atts), + Position.get_line(atts), + Position.get_id(atts), + Position.get_offset(atts)))) + case _ => state + } + } + else { + state.add_markup( + command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind))) + } + case _ => + System.err.println("ignored status report: " + elem) + state + }) + case _ => add_result(message) + } + if (!(this eq changed)) session.command_change.event(command) + changed + } +} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/PIDE/text_edit.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/text_edit.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,51 @@ +/* Title: Pure/PIDE/text_edit.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Basic edits on plain text. +*/ + +package isabelle + + +class Text_Edit(val is_insert: Boolean, val start: Int, val text: String) +{ + override def toString = + (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" + + + /* transform offsets */ + + private def transform(do_insert: Boolean, offset: Int): Int = + if (offset < start) offset + else if (is_insert == do_insert) offset + text.length + else (offset - text.length) max start + + def after(offset: Int): Int = transform(true, offset) + def before(offset: Int): Int = transform(false, offset) + + + /* edit strings */ + + private def insert(index: Int, string: String): String = + string.substring(0, index) + text + string.substring(index) + + private def remove(index: Int, count: Int, string: String): String = + string.substring(0, index) + string.substring(index + count) + + def can_edit(string: String, shift: Int): Boolean = + shift <= start && start < shift + string.length + + def edit(string: String, shift: Int): (Option[Text_Edit], String) = + if (!can_edit(string, shift)) (Some(this), string) + else if (is_insert) (None, insert(start - shift, string)) + else { + val index = start - shift + val count = text.length min (string.length - index) + val rest = + if (count == text.length) None + else Some(new Text_Edit(false, start, text.substring(count))) + (rest, remove(index, count, string)) + } +} + diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/System/download.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/download.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,53 @@ +/* Title: Pure/System/download.scala + Author: Makarius + +Download URLs -- with progress monitor. +*/ + +package isabelle + + +import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, + File, InterruptedIOException} +import java.net.{URL, URLConnection} +import java.awt.{Component, HeadlessException} +import javax.swing.ProgressMonitorInputStream + + +object Download +{ + def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) = + { + val connection = url.openConnection + + val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream) + val monitor = stream.getProgressMonitor + monitor.setNote(connection.getURL.toString) + + val length = connection.getContentLength + if (length != -1) monitor.setMaximum(length) + + (connection, new BufferedInputStream(stream)) + } + + def file(parent: Component, url: URL, file: File) + { + val (connection, instream) = stream(parent, url) + val mod_time = connection.getLastModified + + def read() = + try { instream.read } + catch { case _ : InterruptedIOException => error("Download canceled!") } + try { + val outstream = new BufferedOutputStream(new FileOutputStream(file)) + try { + var c: Int = 0 + while ({ c = read(); c != -1}) outstream.write(c) + } + finally { outstream.close } + if (mod_time > 0) file.setLastModified(mod_time) + } + finally { instream.close } + } +} + diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed May 05 15:30:01 2010 +0200 +++ b/src/Pure/System/session.scala Wed May 05 22:23:45 2010 +0200 @@ -1,8 +1,8 @@ -/* - * Isabelle session, potentially with running prover - * - * @author Makarius - */ +/* Title: Pure/System/session.scala + Author: Makarius + +Isabelle session, potentially with running prover. +*/ package isabelle diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/System/swing_thread.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/swing_thread.scala Wed May 05 22:23:45 2010 +0200 @@ -0,0 +1,63 @@ +/* Title: Pure/System/swing_thread.scala + Author: Makarius + Author: Fabian Immler, TU Munich + +Evaluation within the AWT/Swing thread. +*/ + +package isabelle + +import javax.swing.{SwingUtilities, Timer} +import java.awt.event.{ActionListener, ActionEvent} + + +object Swing_Thread +{ + /* checks */ + + def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) + def require() = Predef.require(SwingUtilities.isEventDispatchThread()) + + + /* main dispatch queue */ + + def now[A](body: => A): A = + { + var result: Option[A] = None + if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } + else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) + result.get + } + + def future[A](body: => A): Future[A] = + { + if (SwingUtilities.isEventDispatchThread()) Future.value(body) + else Future.fork { now(body) } + } + + def later(body: => Unit) + { + if (SwingUtilities.isEventDispatchThread()) body + else SwingUtilities.invokeLater(new Runnable { def run = body }) + } + + + /* delayed actions */ + + private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit = + { + val listener = + new ActionListener { override def actionPerformed(e: ActionEvent) { action } } + val timer = new Timer(time_span, listener) + timer.setRepeats(false) + + def invoke() { if (first) timer.start() else timer.restart() } + invoke _ + } + + // delayed action after first invocation + def delay_first = delayed_action(true) _ + + // delayed action after last invocation + def delay_last = delayed_action(false) _ +} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/Thy/change.scala --- a/src/Pure/Thy/change.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -/* - * Changes of plain text - * - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle - - -class Change( - val id: Isar_Document.Document_ID, - val parent: Option[Change], - val edits: List[Text_Edit], - val result: Future[(List[Document.Edit], Document)]) -{ - def ancestors: Iterator[Change] = new Iterator[Change] - { - private var state: Option[Change] = Some(Change.this) - def hasNext = state.isDefined - def next = - state match { - case Some(change) => state = change.parent; change - case None => throw new NoSuchElementException("next on empty iterator") - } - } - - def join_document: Document = result.join._2 - def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished - - def edit(session: Session, edits: List[Text_Edit]): Change = - { - val new_id = session.create_id() - val result: Future[(List[Document.Edit], Document)] = - Future.fork { - val old_doc = join_document - old_doc.await_assignment - Document.text_edits(session, old_doc, new_id, edits) - } - new Change(new_id, Some(this), edits, result) - } -} \ No newline at end of file diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/Thy/command.scala --- a/src/Pure/Thy/command.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -/* - * Prover commands with semantic state - * - * @author Johannes Hölzl, TU Munich - * @author Fabian Immler, TU Munich - */ - -package isabelle - - -import scala.actors.Actor, Actor._ -import scala.collection.mutable - - -object Command -{ - object Status extends Enumeration - { - val UNPROCESSED = Value("UNPROCESSED") - val FINISHED = Value("FINISHED") - val FAILED = Value("FAILED") - } - - case class HighlightInfo(highlight: String) { override def toString = highlight } - case class TypeInfo(ty: String) - case class RefInfo(file: Option[String], line: Option[Int], - command_id: Option[String], offset: Option[Int]) -} - - -class Command( - val id: Isar_Document.Command_ID, - val span: Thy_Syntax.Span) - extends Session.Entity -{ - /* classification */ - - def is_command: Boolean = !span.isEmpty && span.head.is_command - def is_ignored: Boolean = span.forall(_.is_ignored) - def is_malformed: Boolean = !is_command && !is_ignored - - def name: String = if (is_command) span.head.content else "" - override def toString = if (is_command) name else if (is_ignored) "" else "" - - - /* source text */ - - val source: String = span.map(_.source).mkString - def source(i: Int, j: Int): String = source.substring(i, j) - def length: Int = source.length - - lazy val symbol_index = new Symbol.Index(source) - - - /* accumulated messages */ - - @volatile protected var state = new State(this) - def current_state: State = state - - private case class Consume(session: Session, message: XML.Tree) - private case object Assign - - private val accumulator = actor { - var assigned = false - loop { - react { - case Consume(session: Session, message: XML.Tree) if !assigned => - state = state.+(session, message) - - case Assign => - assigned = true // single assignment - reply(()) - - case bad => System.err.println("command accumulator: ignoring bad message " + bad) - } - } - } - - def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } - - def assign_state(state_id: Isar_Document.State_ID): Command = - { - val cmd = new Command(state_id, span) - accumulator !? Assign - cmd.state = current_state - cmd - } - - - /* markup */ - - lazy val empty_markup = new Markup_Text(Nil, source) - - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = - { - val start = symbol_index.decode(begin) - val stop = symbol_index.decode(end) - new Markup_Tree(new Markup_Node(start, stop, info), Nil) - } -} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/Thy/document.scala --- a/src/Pure/Thy/document.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,197 +0,0 @@ -/* - * Document as editable list of commands - * - * @author Makarius - */ - -package isabelle - - -object Document -{ - /* command start positions */ - - def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] = - { - var offset = 0 - for (cmd <- commands.iterator) yield { - val start = offset - offset += cmd.length - (cmd, start) - } - } - - - /* empty document */ - - def empty(id: Isar_Document.Document_ID): Document = - { - val doc = new Document(id, Linear_Set(), Map()) - doc.assign_states(Nil) - doc - } - - - // FIXME - var phase0: List[Text_Edit] = null - var phase1: Linear_Set[Command] = null - var phase2: Linear_Set[Command] = null - var phase3: List[Edit] = null - - - - /** document edits **/ - - type Edit = (Option[Command], Option[Command]) - - def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, - edits: List[Text_Edit]): (List[Edit], Document) = - { - require(old_doc.assignment.is_finished) - - - /* unparsed dummy commands */ - - def unparsed(source: String) = - new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) - - def is_unparsed(command: Command) = command.id == null - - assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove - - - /* phase 1: edit individual command source */ - - def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = - { - eds match { - case e :: es => - command_starts(commands).find { // FIXME relative search! - case (cmd, cmd_start) => - e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length - } match { - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => - val (rest, text) = e.edit(cmd.source, cmd_start) - val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd - edit_text(rest.toList ::: es, new_commands) - - case Some((cmd, cmd_start)) => - edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) - - case None => - require(e.is_insert && e.start == 0) - edit_text(es, commands.insert_after(None, unparsed(e.text))) - } - case Nil => commands - } - } - - - /* phase 2: recover command spans */ - - def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = - { - // FIXME relative search! - commands.iterator.find(is_unparsed) match { - case Some(first_unparsed) => - val prefix = commands.prev(first_unparsed) - val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList - val suffix = commands.next(body.last) - - val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) - val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) - - val (before_edit, spans1) = - if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) - (prefix, spans0.tail) - else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) - - val (after_edit, spans2) = - if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) - (suffix, spans1.take(spans1.length - 1)) - else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) - - val inserted = spans2.map(span => new Command(session.create_id(), span)) - val new_commands = - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) - parse_spans(new_commands) - - case None => commands - } - } - - - /* phase 3: resulting document edits */ - - val result = Library.timeit("text_edits") { - val commands0 = old_doc.commands - val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) } - val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) } - - val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList - val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList - - val doc_edits = - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) - - val former_states = old_doc.assignment.join -- removed_commands - - phase0 = edits - phase1 = commands1 - phase2 = commands2 - phase3 = doc_edits - - (doc_edits, new Document(new_id, commands2, former_states)) - } - result - } -} - - -class Document( - val id: Isar_Document.Document_ID, - val commands: Linear_Set[Command], - former_states: Map[Command, Command]) -{ - /* command ranges */ - - def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) - - def command_start(cmd: Command): Option[Int] = - command_starts.find(_._1 == cmd).map(_._2) - - def command_range(i: Int): Iterator[(Command, Int)] = - command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } - - def command_range(i: Int, j: Int): Iterator[(Command, Int)] = - command_range(i) takeWhile { case (_, start) => start < j } - - def command_at(i: Int): Option[(Command, Int)] = - { - val range = command_range(i) - if (range.hasNext) Some(range.next) else None - } - - - /* command state assignment */ - - val assignment = Future.promise[Map[Command, Command]] - def await_assignment { assignment.join } - - @volatile private var tmp_states = former_states - private val time0 = System.currentTimeMillis - - def assign_states(new_states: List[(Command, Command)]) - { - assignment.fulfill(tmp_states ++ new_states) - tmp_states = Map() - System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") - } - - def current_state(cmd: Command): Option[State] = - { - require(assignment.is_finished) - (assignment.join).get(cmd).map(_.current_state) - } -} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/Thy/markup_node.scala --- a/src/Pure/Thy/markup_node.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,111 +0,0 @@ -/* - * Document markup nodes, with connection to Swing tree model - * - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle - - -import javax.swing.tree.DefaultMutableTreeNode - - - -class Markup_Node(val start: Int, val stop: Int, val info: Any) -{ - def fits_into(that: Markup_Node): Boolean = - that.start <= this.start && this.stop <= that.stop -} - - -class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) -{ - def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs) - - private def add(branch: Markup_Tree) = // FIXME avoid sort - set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start)) - - private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs) - - def + (new_tree: Markup_Tree): Markup_Tree = - { - val new_node = new_tree.node - if (new_node fits_into node) { - var inserted = false - val new_branches = - branches.map(branch => - if ((new_node fits_into branch.node) && !inserted) { - inserted = true - branch + new_tree - } - else branch) - if (!inserted) { - // new_tree did not fit into children of this - // -> insert between this and its branches - val fitting = branches filter(_.node fits_into new_node) - (this remove fitting) add ((new_tree /: fitting)(_ + _)) - } - else set_branches(new_branches) - } - else { - System.err.println("ignored nonfitting markup: " + new_node) - this - } - } - - def flatten: List[Markup_Node] = - { - var next_x = node.start - if (branches.isEmpty) List(this.node) - else { - val filled_gaps = - for { - child <- branches - markups = - if (next_x < child.node.start) - new Markup_Node(next_x, child.node.start, node.info) :: child.flatten - else child.flatten - update = (next_x = child.node.stop) - markup <- markups - } yield markup - if (next_x < node.stop) - filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) - else filled_gaps - } - } -} - - -class Markup_Text(val markup: List[Markup_Tree], val content: String) -{ - private lazy val root = - new Markup_Tree(new Markup_Node(0, content.length, None), markup) - - def + (new_tree: Markup_Tree): Markup_Text = - new Markup_Text((root + new_tree).branches, content) - - def filter(pred: Markup_Node => Boolean): Markup_Text = - { - def filt(tree: Markup_Tree): List[Markup_Tree] = - { - val branches = tree.branches.flatMap(filt(_)) - if (pred(tree.node)) List(tree.set_branches(branches)) - else branches - } - new Markup_Text(markup.flatMap(filt(_)), content) - } - - def flatten: List[Markup_Node] = markup.flatten(_.flatten) - - def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = - { - def swing(tree: Markup_Tree): DefaultMutableTreeNode = - { - val node = swing_node(tree.node) - tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) - node - } - swing(root) - } -} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/Thy/state.scala --- a/src/Pure/Thy/state.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -/* - * Accumulating results from prover - * - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle - - -class State( - val command: Command, - val status: Command.Status.Value, - val rev_results: List[XML.Tree], - val markup_root: Markup_Text) -{ - def this(command: Command) = - this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup) - - - /* content */ - - private def set_status(st: Command.Status.Value): State = - new State(command, st, rev_results, markup_root) - - private def add_result(res: XML.Tree): State = - new State(command, status, res :: rev_results, markup_root) - - private def add_markup(node: Markup_Tree): State = - new State(command, status, rev_results, markup_root + node) - - lazy val results = rev_results.reverse - - - /* markup */ - - lazy val highlight: Markup_Text = - { - markup_root.filter(_.info match { - case Command.HighlightInfo(_) => true - case _ => false - }) - } - - private lazy val types: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.TypeInfo(_) => true - case _ => false }).flatten - - def type_at(pos: Int): Option[String] = - { - types.find(t => t.start <= pos && pos < t.stop) match { - case Some(t) => - t.info match { - case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty) - case _ => None - } - case None => None - } - } - - private lazy val refs: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.RefInfo(_, _, _, _) => true - case _ => false }).flatten - - def ref_at(pos: Int): Option[Markup_Node] = - refs.find(t => t.start <= pos && pos < t.stop) - - - /* message dispatch */ - - def + (session: Session, message: XML.Tree): State = - { - val changed: State = - message match { - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) - case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) - case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) - case XML.Elem(kind, atts, body) => - val (begin, end) = Position.get_offsets(atts) - if (begin.isEmpty || end.isEmpty) state - else if (kind == Markup.ML_TYPING) { - val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!? - state.add_markup( - command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info))) - } - else if (kind == Markup.ML_REF) { - body match { - case List(XML.Elem(Markup.ML_DEF, atts, _)) => - state.add_markup(command.markup_node( - begin.get - 1, end.get - 1, - Command.RefInfo( - Position.get_file(atts), - Position.get_line(atts), - Position.get_id(atts), - Position.get_offset(atts)))) - case _ => state - } - } - else { - state.add_markup( - command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind))) - } - case _ => - System.err.println("ignored status report: " + elem) - state - }) - case _ => add_result(message) - } - if (!(this eq changed)) session.command_change.event(command) - changed - } -} diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/Thy/text_edit.scala --- a/src/Pure/Thy/text_edit.scala Wed May 05 15:30:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -/* Title: Pure/Thy/text_edit.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -Basic edits on plain text. -*/ - -package isabelle - - -class Text_Edit(val is_insert: Boolean, val start: Int, val text: String) -{ - override def toString = - (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" - - - /* transform offsets */ - - private def transform(do_insert: Boolean, offset: Int): Int = - if (offset < start) offset - else if (is_insert == do_insert) offset + text.length - else (offset - text.length) max start - - def after(offset: Int): Int = transform(true, offset) - def before(offset: Int): Int = transform(false, offset) - - - /* edit strings */ - - private def insert(index: Int, string: String): String = - string.substring(0, index) + text + string.substring(index) - - private def remove(index: Int, count: Int, string: String): String = - string.substring(0, index) + string.substring(index + count) - - def can_edit(string: String, shift: Int): Boolean = - shift <= start && start < shift + string.length - - def edit(string: String, shift: Int): (Option[Text_Edit], String) = - if (!can_edit(string, shift)) (Some(this), string) - else if (is_insert) (None, insert(start - shift, string)) - else { - val index = start - shift - val count = text.length min (string.length - index) - val rest = - if (count == text.length) None - else Some(new Text_Edit(false, start, text.substring(count))) - (rest, remove(index, count, string)) - } -} - diff -r 806ea6e282e4 -r ac7961d42ac3 src/Pure/build-jars --- a/src/Pure/build-jars Wed May 05 15:30:01 2010 +0200 +++ b/src/Pure/build-jars Wed May 05 22:23:45 2010 +0200 @@ -23,14 +23,11 @@ declare -a SOURCES=( Concurrent/future.scala - General/download.scala - General/event_bus.scala General/exn.scala General/linear_set.scala General/markup.scala General/position.scala General/scan.scala - General/swing_thread.scala General/symbol.scala General/xml.scala General/yxml.scala @@ -39,7 +36,15 @@ Isar/outer_lex.scala Isar/outer_parse.scala Isar/outer_syntax.scala + PIDE/change.scala + PIDE/command.scala + PIDE/document.scala + PIDE/event_bus.scala + PIDE/markup_node.scala + PIDE/state.scala + PIDE/text_edit.scala System/cygwin.scala + System/download.scala System/gui_setup.scala System/isabelle_process.scala System/isabelle_syntax.scala @@ -48,14 +53,9 @@ System/session.scala System/session_manager.scala System/standard_system.scala - Thy/change.scala - Thy/command.scala + System/swing_thread.scala Thy/completion.scala - Thy/document.scala Thy/html.scala - Thy/markup_node.scala - Thy/state.scala - Thy/text_edit.scala Thy/thy_header.scala Thy/thy_syntax.scala library.scala