--- 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 }
- }
-}
-
--- 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) } }
-}
--- 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) _
-}
--- /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
--- /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) "<ignored>" else "<malformed>"
+
+
+ /* 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)
+ }
+}
--- /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)
+ }
+}
--- /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) } }
+}
--- /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)
+ }
+}
--- /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
+ }
+}
--- /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))
+ }
+}
+
--- /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 }
+ }
+}
+
--- 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
--- /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) _
+}
--- 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
--- 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) "<ignored>" else "<malformed>"
-
-
- /* 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)
- }
-}
--- 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)
- }
-}
--- 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)
- }
-}
--- 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
- }
-}
--- 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))
- }
-}
-
--- 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