some rearrangement of Scala sources;
authorwenzelm
Wed May 05 22:23:45 2010 +0200 (2010-05-05)
changeset 36676ac7961d42ac3
parent 36675 806ea6e282e4
child 36677 1225dd15827d
some rearrangement of Scala sources;
src/Pure/General/download.scala
src/Pure/General/event_bus.scala
src/Pure/General/swing_thread.scala
src/Pure/PIDE/change.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/event_bus.scala
src/Pure/PIDE/markup_node.scala
src/Pure/PIDE/state.scala
src/Pure/PIDE/text_edit.scala
src/Pure/System/download.scala
src/Pure/System/session.scala
src/Pure/System/swing_thread.scala
src/Pure/Thy/change.scala
src/Pure/Thy/command.scala
src/Pure/Thy/document.scala
src/Pure/Thy/markup_node.scala
src/Pure/Thy/state.scala
src/Pure/Thy/text_edit.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/General/download.scala	Wed May 05 15:30:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,53 +0,0 @@
     1.4 -/*  Title:      Pure/General/download.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Download URLs -- with progress monitor.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
    1.14 -  File, InterruptedIOException}
    1.15 -import java.net.{URL, URLConnection}
    1.16 -import java.awt.{Component, HeadlessException}
    1.17 -import javax.swing.ProgressMonitorInputStream
    1.18 -
    1.19 -
    1.20 -object Download
    1.21 -{
    1.22 -  def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
    1.23 -  {
    1.24 -    val connection = url.openConnection
    1.25 -
    1.26 -    val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
    1.27 -    val monitor = stream.getProgressMonitor
    1.28 -    monitor.setNote(connection.getURL.toString)
    1.29 -
    1.30 -    val length = connection.getContentLength
    1.31 -    if (length != -1) monitor.setMaximum(length)
    1.32 -
    1.33 -    (connection, new BufferedInputStream(stream))
    1.34 -  }
    1.35 -
    1.36 -  def file(parent: Component, url: URL, file: File)
    1.37 -  {
    1.38 -    val (connection, instream) = stream(parent, url)
    1.39 -    val mod_time = connection.getLastModified
    1.40 -
    1.41 -    def read() =
    1.42 -      try { instream.read }
    1.43 -      catch { case _ : InterruptedIOException => error("Download canceled!") }
    1.44 -    try {
    1.45 -      val outstream = new BufferedOutputStream(new FileOutputStream(file))
    1.46 -      try {
    1.47 -        var c: Int = 0
    1.48 -        while ({ c = read(); c != -1}) outstream.write(c)
    1.49 -      }
    1.50 -      finally { outstream.close }
    1.51 -      if (mod_time > 0) file.setLastModified(mod_time)
    1.52 -    }
    1.53 -    finally { instream.close }
    1.54 -  }
    1.55 -}
    1.56 -
     2.1 --- a/src/Pure/General/event_bus.scala	Wed May 05 15:30:01 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,35 +0,0 @@
     2.4 -/*  Title:      Pure/General/event_bus.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Generic event bus with multiple receiving actors.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -import scala.actors.Actor, Actor._
    2.13 -import scala.collection.mutable.ListBuffer
    2.14 -
    2.15 -
    2.16 -class Event_Bus[Event]
    2.17 -{
    2.18 -  /* receivers */
    2.19 -
    2.20 -  private val receivers = new ListBuffer[Actor]
    2.21 -
    2.22 -  def += (r: Actor) { synchronized { receivers += r } }
    2.23 -  def + (r: Actor): Event_Bus[Event] = { this += r; this }
    2.24 -
    2.25 -  def += (f: Event => Unit) {
    2.26 -    this += actor { loop { react { case x: Event => f(x) } } }
    2.27 -  }
    2.28 -
    2.29 -  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
    2.30 -
    2.31 -  def -= (r: Actor) { synchronized { receivers -= r } }
    2.32 -  def - (r: Actor) = { this -= r; this }
    2.33 -
    2.34 -
    2.35 -  /* event invocation */
    2.36 -
    2.37 -  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
    2.38 -}
     3.1 --- a/src/Pure/General/swing_thread.scala	Wed May 05 15:30:01 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,63 +0,0 @@
     3.4 -/*  Title:      Pure/General/swing_thread.scala
     3.5 -    Author:     Makarius
     3.6 -    Author:     Fabian Immler, TU Munich
     3.7 -
     3.8 -Evaluation within the AWT/Swing thread.
     3.9 -*/
    3.10 -
    3.11 -package isabelle
    3.12 -
    3.13 -import javax.swing.{SwingUtilities, Timer}
    3.14 -import java.awt.event.{ActionListener, ActionEvent}
    3.15 -
    3.16 -
    3.17 -object Swing_Thread
    3.18 -{
    3.19 -  /* checks */
    3.20 -
    3.21 -  def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
    3.22 -  def require() = Predef.require(SwingUtilities.isEventDispatchThread())
    3.23 -
    3.24 -
    3.25 -  /* main dispatch queue */
    3.26 -
    3.27 -  def now[A](body: => A): A =
    3.28 -  {
    3.29 -    var result: Option[A] = None
    3.30 -    if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
    3.31 -    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
    3.32 -    result.get
    3.33 -  }
    3.34 -
    3.35 -  def future[A](body: => A): Future[A] =
    3.36 -  {
    3.37 -    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
    3.38 -    else Future.fork { now(body) }
    3.39 -  }
    3.40 -
    3.41 -  def later(body: => Unit)
    3.42 -  {
    3.43 -    if (SwingUtilities.isEventDispatchThread()) body
    3.44 -    else SwingUtilities.invokeLater(new Runnable { def run = body })
    3.45 -  }
    3.46 -
    3.47 -
    3.48 -  /* delayed actions */
    3.49 -
    3.50 -  private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
    3.51 -  {
    3.52 -    val listener =
    3.53 -      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
    3.54 -    val timer = new Timer(time_span, listener)
    3.55 -    timer.setRepeats(false)
    3.56 -
    3.57 -    def invoke() { if (first) timer.start() else timer.restart() }
    3.58 -    invoke _
    3.59 -  }
    3.60 -
    3.61 -  // delayed action after first invocation
    3.62 -  def delay_first = delayed_action(true) _
    3.63 -
    3.64 -  // delayed action after last invocation
    3.65 -  def delay_last = delayed_action(false) _
    3.66 -}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/PIDE/change.scala	Wed May 05 22:23:45 2010 +0200
     4.3 @@ -0,0 +1,42 @@
     4.4 +/*  Title:      Pure/PIDE/change.scala
     4.5 +    Author:     Fabian Immler, TU Munich
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +Changes of plain text.
     4.9 +*/
    4.10 +
    4.11 +package isabelle
    4.12 +
    4.13 +
    4.14 +class Change(
    4.15 +  val id: Isar_Document.Document_ID,
    4.16 +  val parent: Option[Change],
    4.17 +  val edits: List[Text_Edit],
    4.18 +  val result: Future[(List[Document.Edit], Document)])
    4.19 +{
    4.20 +  def ancestors: Iterator[Change] = new Iterator[Change]
    4.21 +  {
    4.22 +    private var state: Option[Change] = Some(Change.this)
    4.23 +    def hasNext = state.isDefined
    4.24 +    def next =
    4.25 +      state match {
    4.26 +        case Some(change) => state = change.parent; change
    4.27 +        case None => throw new NoSuchElementException("next on empty iterator")
    4.28 +      }
    4.29 +  }
    4.30 +
    4.31 +  def join_document: Document = result.join._2
    4.32 +  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    4.33 +
    4.34 +  def edit(session: Session, edits: List[Text_Edit]): Change =
    4.35 +  {
    4.36 +    val new_id = session.create_id()
    4.37 +    val result: Future[(List[Document.Edit], Document)] =
    4.38 +      Future.fork {
    4.39 +        val old_doc = join_document
    4.40 +        old_doc.await_assignment
    4.41 +        Document.text_edits(session, old_doc, new_id, edits)
    4.42 +      }
    4.43 +    new Change(new_id, Some(this), edits, result)
    4.44 +  }
    4.45 +}
    4.46 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/PIDE/command.scala	Wed May 05 22:23:45 2010 +0200
     5.3 @@ -0,0 +1,101 @@
     5.4 +/*  Title:      Pure/PIDE/command.scala
     5.5 +    Author:     Johannes Hölzl, TU Munich
     5.6 +    Author:     Fabian Immler, TU Munich
     5.7 +    Author:     Makarius
     5.8 +
     5.9 +Prover commands with semantic state.
    5.10 +*/
    5.11 +
    5.12 +package isabelle
    5.13 +
    5.14 +
    5.15 +import scala.actors.Actor, Actor._
    5.16 +import scala.collection.mutable
    5.17 +
    5.18 +
    5.19 +object Command
    5.20 +{
    5.21 +  object Status extends Enumeration
    5.22 +  {
    5.23 +    val UNPROCESSED = Value("UNPROCESSED")
    5.24 +    val FINISHED = Value("FINISHED")
    5.25 +    val FAILED = Value("FAILED")
    5.26 +  }
    5.27 +
    5.28 +  case class HighlightInfo(highlight: String) { override def toString = highlight }
    5.29 +  case class TypeInfo(ty: String)
    5.30 +  case class RefInfo(file: Option[String], line: Option[Int],
    5.31 +    command_id: Option[String], offset: Option[Int])
    5.32 +}
    5.33 +
    5.34 +
    5.35 +class Command(
    5.36 +    val id: Isar_Document.Command_ID,
    5.37 +    val span: Thy_Syntax.Span)
    5.38 +  extends Session.Entity
    5.39 +{
    5.40 +  /* classification */
    5.41 +
    5.42 +  def is_command: Boolean = !span.isEmpty && span.head.is_command
    5.43 +  def is_ignored: Boolean = span.forall(_.is_ignored)
    5.44 +  def is_malformed: Boolean = !is_command && !is_ignored
    5.45 +
    5.46 +  def name: String = if (is_command) span.head.content else ""
    5.47 +  override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
    5.48 +
    5.49 +
    5.50 +  /* source text */
    5.51 +
    5.52 +  val source: String = span.map(_.source).mkString
    5.53 +  def source(i: Int, j: Int): String = source.substring(i, j)
    5.54 +  def length: Int = source.length
    5.55 +
    5.56 +  lazy val symbol_index = new Symbol.Index(source)
    5.57 +
    5.58 +
    5.59 +  /* accumulated messages */
    5.60 +
    5.61 +  @volatile protected var state = new State(this)
    5.62 +  def current_state: State = state
    5.63 +
    5.64 +  private case class Consume(session: Session, message: XML.Tree)
    5.65 +  private case object Assign
    5.66 +
    5.67 +  private val accumulator = actor {
    5.68 +    var assigned = false
    5.69 +    loop {
    5.70 +      react {
    5.71 +        case Consume(session: Session, message: XML.Tree) if !assigned =>
    5.72 +          state = state.+(session, message)
    5.73 +
    5.74 +        case Assign =>
    5.75 +          assigned = true  // single assignment
    5.76 +          reply(())
    5.77 +
    5.78 +        case bad => System.err.println("command accumulator: ignoring bad message " + bad)
    5.79 +      }
    5.80 +    }
    5.81 +  }
    5.82 +
    5.83 +  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
    5.84 +
    5.85 +  def assign_state(state_id: Isar_Document.State_ID): Command =
    5.86 +  {
    5.87 +    val cmd = new Command(state_id, span)
    5.88 +    accumulator !? Assign
    5.89 +    cmd.state = current_state
    5.90 +    cmd
    5.91 +  }
    5.92 +
    5.93 +
    5.94 +  /* markup */
    5.95 +
    5.96 +  lazy val empty_markup = new Markup_Text(Nil, source)
    5.97 +
    5.98 +  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
    5.99 +  {
   5.100 +    val start = symbol_index.decode(begin)
   5.101 +    val stop = symbol_index.decode(end)
   5.102 +    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   5.103 +  }
   5.104 +}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/PIDE/document.scala	Wed May 05 22:23:45 2010 +0200
     6.3 @@ -0,0 +1,197 @@
     6.4 +/*  Title:      Pure/PIDE/document.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Document as editable list of commands.
     6.8 +*/
     6.9 +
    6.10 +package isabelle
    6.11 +
    6.12 +
    6.13 +object Document
    6.14 +{
    6.15 +  /* command start positions */
    6.16 +
    6.17 +  def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
    6.18 +  {
    6.19 +    var offset = 0
    6.20 +    for (cmd <- commands.iterator) yield {
    6.21 +      val start = offset
    6.22 +      offset += cmd.length
    6.23 +      (cmd, start)
    6.24 +    }
    6.25 +  }
    6.26 +
    6.27 +
    6.28 +  /* empty document */
    6.29 +
    6.30 +  def empty(id: Isar_Document.Document_ID): Document =
    6.31 +  {
    6.32 +    val doc = new Document(id, Linear_Set(), Map())
    6.33 +    doc.assign_states(Nil)
    6.34 +    doc
    6.35 +  }
    6.36 +
    6.37 +
    6.38 +  // FIXME
    6.39 +  var phase0: List[Text_Edit] = null
    6.40 +  var phase1: Linear_Set[Command] = null
    6.41 +  var phase2: Linear_Set[Command] = null
    6.42 +  var phase3: List[Edit] = null
    6.43 +
    6.44 +
    6.45 +
    6.46 +  /** document edits **/
    6.47 +
    6.48 +  type Edit = (Option[Command], Option[Command])
    6.49 +
    6.50 +  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
    6.51 +    edits: List[Text_Edit]): (List[Edit], Document) =
    6.52 +  {
    6.53 +    require(old_doc.assignment.is_finished)
    6.54 +
    6.55 +
    6.56 +    /* unparsed dummy commands */
    6.57 +
    6.58 +    def unparsed(source: String) =
    6.59 +      new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
    6.60 +
    6.61 +    def is_unparsed(command: Command) = command.id == null
    6.62 +
    6.63 +    assert(!old_doc.commands.exists(is_unparsed))   // FIXME remove
    6.64 +
    6.65 +
    6.66 +    /* phase 1: edit individual command source */
    6.67 +
    6.68 +    def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
    6.69 +    {
    6.70 +      eds match {
    6.71 +        case e :: es =>
    6.72 +          command_starts(commands).find {   // FIXME relative search!
    6.73 +            case (cmd, cmd_start) =>
    6.74 +              e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
    6.75 +          } match {
    6.76 +            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    6.77 +              val (rest, text) = e.edit(cmd.source, cmd_start)
    6.78 +              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
    6.79 +              edit_text(rest.toList ::: es, new_commands)
    6.80 +
    6.81 +            case Some((cmd, cmd_start)) =>
    6.82 +              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
    6.83 +
    6.84 +            case None =>
    6.85 +              require(e.is_insert && e.start == 0)
    6.86 +              edit_text(es, commands.insert_after(None, unparsed(e.text)))
    6.87 +          }
    6.88 +        case Nil => commands
    6.89 +      }
    6.90 +    }
    6.91 +
    6.92 +
    6.93 +    /* phase 2: recover command spans */
    6.94 +
    6.95 +    def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    6.96 +    {
    6.97 +      // FIXME relative search!
    6.98 +      commands.iterator.find(is_unparsed) match {
    6.99 +        case Some(first_unparsed) =>
   6.100 +          val prefix = commands.prev(first_unparsed)
   6.101 +          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
   6.102 +          val suffix = commands.next(body.last)
   6.103 +
   6.104 +          val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
   6.105 +          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
   6.106 +
   6.107 +          val (before_edit, spans1) =
   6.108 +            if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
   6.109 +              (prefix, spans0.tail)
   6.110 +            else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
   6.111 +
   6.112 +          val (after_edit, spans2) =
   6.113 +            if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
   6.114 +              (suffix, spans1.take(spans1.length - 1))
   6.115 +            else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
   6.116 +
   6.117 +          val inserted = spans2.map(span => new Command(session.create_id(), span))
   6.118 +          val new_commands =
   6.119 +            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
   6.120 +          parse_spans(new_commands)
   6.121 +
   6.122 +        case None => commands
   6.123 +      }
   6.124 +    }
   6.125 +
   6.126 +
   6.127 +    /* phase 3: resulting document edits */
   6.128 +
   6.129 +    val result = Library.timeit("text_edits") {
   6.130 +      val commands0 = old_doc.commands
   6.131 +      val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
   6.132 +      val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
   6.133 +
   6.134 +      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
   6.135 +      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
   6.136 +
   6.137 +      val doc_edits =
   6.138 +        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   6.139 +        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   6.140 +
   6.141 +      val former_states = old_doc.assignment.join -- removed_commands
   6.142 +
   6.143 +      phase0 = edits
   6.144 +      phase1 = commands1
   6.145 +      phase2 = commands2
   6.146 +      phase3 = doc_edits
   6.147 +
   6.148 +      (doc_edits, new Document(new_id, commands2, former_states))
   6.149 +    }
   6.150 +    result
   6.151 +  }
   6.152 +}
   6.153 +
   6.154 +
   6.155 +class Document(
   6.156 +    val id: Isar_Document.Document_ID,
   6.157 +    val commands: Linear_Set[Command],
   6.158 +    former_states: Map[Command, Command])
   6.159 +{
   6.160 +  /* command ranges */
   6.161 +
   6.162 +  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
   6.163 +
   6.164 +  def command_start(cmd: Command): Option[Int] =
   6.165 +    command_starts.find(_._1 == cmd).map(_._2)
   6.166 +
   6.167 +  def command_range(i: Int): Iterator[(Command, Int)] =
   6.168 +    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
   6.169 +
   6.170 +  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
   6.171 +    command_range(i) takeWhile { case (_, start) => start < j }
   6.172 +
   6.173 +  def command_at(i: Int): Option[(Command, Int)] =
   6.174 +  {
   6.175 +    val range = command_range(i)
   6.176 +    if (range.hasNext) Some(range.next) else None
   6.177 +  }
   6.178 +
   6.179 +
   6.180 +  /* command state assignment */
   6.181 +
   6.182 +  val assignment = Future.promise[Map[Command, Command]]
   6.183 +  def await_assignment { assignment.join }
   6.184 +
   6.185 +  @volatile private var tmp_states = former_states
   6.186 +  private val time0 = System.currentTimeMillis
   6.187 +
   6.188 +  def assign_states(new_states: List[(Command, Command)])
   6.189 +  {
   6.190 +    assignment.fulfill(tmp_states ++ new_states)
   6.191 +    tmp_states = Map()
   6.192 +    System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
   6.193 +  }
   6.194 +
   6.195 +  def current_state(cmd: Command): Option[State] =
   6.196 +  {
   6.197 +    require(assignment.is_finished)
   6.198 +    (assignment.join).get(cmd).map(_.current_state)
   6.199 +  }
   6.200 +}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/PIDE/event_bus.scala	Wed May 05 22:23:45 2010 +0200
     7.3 @@ -0,0 +1,35 @@
     7.4 +/*  Title:      Pure/PIDE/event_bus.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Generic event bus with multiple receiving actors.
     7.8 +*/
     7.9 +
    7.10 +package isabelle
    7.11 +
    7.12 +import scala.actors.Actor, Actor._
    7.13 +import scala.collection.mutable.ListBuffer
    7.14 +
    7.15 +
    7.16 +class Event_Bus[Event]
    7.17 +{
    7.18 +  /* receivers */
    7.19 +
    7.20 +  private val receivers = new ListBuffer[Actor]
    7.21 +
    7.22 +  def += (r: Actor) { synchronized { receivers += r } }
    7.23 +  def + (r: Actor): Event_Bus[Event] = { this += r; this }
    7.24 +
    7.25 +  def += (f: Event => Unit) {
    7.26 +    this += actor { loop { react { case x: Event => f(x) } } }
    7.27 +  }
    7.28 +
    7.29 +  def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
    7.30 +
    7.31 +  def -= (r: Actor) { synchronized { receivers -= r } }
    7.32 +  def - (r: Actor) = { this -= r; this }
    7.33 +
    7.34 +
    7.35 +  /* event invocation */
    7.36 +
    7.37 +  def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
    7.38 +}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/PIDE/markup_node.scala	Wed May 05 22:23:45 2010 +0200
     8.3 @@ -0,0 +1,111 @@
     8.4 +/*  Title:      Pure/PIDE/markup_node.scala
     8.5 +    Author:     Fabian Immler, TU Munich
     8.6 +    Author:     Makarius
     8.7 +
     8.8 +Document markup nodes, with connection to Swing tree model.
     8.9 +*/
    8.10 +
    8.11 +package isabelle
    8.12 +
    8.13 +
    8.14 +import javax.swing.tree.DefaultMutableTreeNode
    8.15 +
    8.16 +
    8.17 +
    8.18 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
    8.19 +{
    8.20 +  def fits_into(that: Markup_Node): Boolean =
    8.21 +    that.start <= this.start && this.stop <= that.stop
    8.22 +}
    8.23 +
    8.24 +
    8.25 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
    8.26 +{
    8.27 +  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
    8.28 +
    8.29 +  private def add(branch: Markup_Tree) =   // FIXME avoid sort
    8.30 +    set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
    8.31 +
    8.32 +  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
    8.33 +
    8.34 +  def + (new_tree: Markup_Tree): Markup_Tree =
    8.35 +  {
    8.36 +    val new_node = new_tree.node
    8.37 +    if (new_node fits_into node) {
    8.38 +      var inserted = false
    8.39 +      val new_branches =
    8.40 +        branches.map(branch =>
    8.41 +          if ((new_node fits_into branch.node) && !inserted) {
    8.42 +            inserted = true
    8.43 +            branch + new_tree
    8.44 +          }
    8.45 +          else branch)
    8.46 +      if (!inserted) {
    8.47 +        // new_tree did not fit into children of this
    8.48 +        // -> insert between this and its branches
    8.49 +        val fitting = branches filter(_.node fits_into new_node)
    8.50 +        (this remove fitting) add ((new_tree /: fitting)(_ + _))
    8.51 +      }
    8.52 +      else set_branches(new_branches)
    8.53 +    }
    8.54 +    else {
    8.55 +      System.err.println("ignored nonfitting markup: " + new_node)
    8.56 +      this
    8.57 +    }
    8.58 +  }
    8.59 +
    8.60 +  def flatten: List[Markup_Node] =
    8.61 +  {
    8.62 +    var next_x = node.start
    8.63 +    if (branches.isEmpty) List(this.node)
    8.64 +    else {
    8.65 +      val filled_gaps =
    8.66 +        for {
    8.67 +          child <- branches
    8.68 +          markups =
    8.69 +            if (next_x < child.node.start)
    8.70 +              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
    8.71 +            else child.flatten
    8.72 +          update = (next_x = child.node.stop)
    8.73 +          markup <- markups
    8.74 +        } yield markup
    8.75 +      if (next_x < node.stop)
    8.76 +        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
    8.77 +      else filled_gaps
    8.78 +    }
    8.79 +  }
    8.80 +}
    8.81 +
    8.82 +
    8.83 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
    8.84 +{
    8.85 +  private lazy val root =
    8.86 +    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
    8.87 +
    8.88 +  def + (new_tree: Markup_Tree): Markup_Text =
    8.89 +    new Markup_Text((root + new_tree).branches, content)
    8.90 +
    8.91 +  def filter(pred: Markup_Node => Boolean): Markup_Text =
    8.92 +  {
    8.93 +    def filt(tree: Markup_Tree): List[Markup_Tree] =
    8.94 +    {
    8.95 +      val branches = tree.branches.flatMap(filt(_))
    8.96 +      if (pred(tree.node)) List(tree.set_branches(branches))
    8.97 +      else branches
    8.98 +    }
    8.99 +    new Markup_Text(markup.flatMap(filt(_)), content)
   8.100 +  }
   8.101 +
   8.102 +  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
   8.103 +
   8.104 +  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
   8.105 +  {
   8.106 +    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
   8.107 +    {
   8.108 +      val node = swing_node(tree.node)
   8.109 +      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
   8.110 +      node
   8.111 +    }
   8.112 +    swing(root)
   8.113 +  }
   8.114 +}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/PIDE/state.scala	Wed May 05 22:23:45 2010 +0200
     9.3 @@ -0,0 +1,117 @@
     9.4 +/*  Title:      Pure/PIDE/state.scala
     9.5 +    Author:     Fabian Immler, TU Munich
     9.6 +    Author:     Makarius
     9.7 +
     9.8 +Accumulating results from prover.
     9.9 +*/
    9.10 +
    9.11 +package isabelle
    9.12 +
    9.13 +
    9.14 +class State(
    9.15 +  val command: Command,
    9.16 +  val status: Command.Status.Value,
    9.17 +  val rev_results: List[XML.Tree],
    9.18 +  val markup_root: Markup_Text)
    9.19 +{
    9.20 +  def this(command: Command) =
    9.21 +    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
    9.22 +
    9.23 +
    9.24 +  /* content */
    9.25 +
    9.26 +  private def set_status(st: Command.Status.Value): State =
    9.27 +    new State(command, st, rev_results, markup_root)
    9.28 +
    9.29 +  private def add_result(res: XML.Tree): State =
    9.30 +    new State(command, status, res :: rev_results, markup_root)
    9.31 +
    9.32 +  private def add_markup(node: Markup_Tree): State =
    9.33 +    new State(command, status, rev_results, markup_root + node)
    9.34 +
    9.35 +  lazy val results = rev_results.reverse
    9.36 +
    9.37 +
    9.38 +  /* markup */
    9.39 +
    9.40 +  lazy val highlight: Markup_Text =
    9.41 +  {
    9.42 +    markup_root.filter(_.info match {
    9.43 +      case Command.HighlightInfo(_) => true
    9.44 +      case _ => false
    9.45 +    })
    9.46 +  }
    9.47 +
    9.48 +  private lazy val types: List[Markup_Node] =
    9.49 +    markup_root.filter(_.info match {
    9.50 +      case Command.TypeInfo(_) => true
    9.51 +      case _ => false }).flatten
    9.52 +
    9.53 +  def type_at(pos: Int): Option[String] =
    9.54 +  {
    9.55 +    types.find(t => t.start <= pos && pos < t.stop) match {
    9.56 +      case Some(t) =>
    9.57 +        t.info match {
    9.58 +          case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
    9.59 +          case _ => None
    9.60 +        }
    9.61 +      case None => None
    9.62 +    }
    9.63 +  }
    9.64 +
    9.65 +  private lazy val refs: List[Markup_Node] =
    9.66 +    markup_root.filter(_.info match {
    9.67 +      case Command.RefInfo(_, _, _, _) => true
    9.68 +      case _ => false }).flatten
    9.69 +
    9.70 +  def ref_at(pos: Int): Option[Markup_Node] =
    9.71 +    refs.find(t => t.start <= pos && pos < t.stop)
    9.72 +
    9.73 +
    9.74 +  /* message dispatch */
    9.75 +
    9.76 +  def + (session: Session, message: XML.Tree): State =
    9.77 +  {
    9.78 +    val changed: State =
    9.79 +      message match {
    9.80 +        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
    9.81 +          (this /: elems)((state, elem) =>
    9.82 +            elem match {
    9.83 +              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    9.84 +              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    9.85 +              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    9.86 +              case XML.Elem(kind, atts, body) =>
    9.87 +                val (begin, end) = Position.get_offsets(atts)
    9.88 +                if (begin.isEmpty || end.isEmpty) state
    9.89 +                else if (kind == Markup.ML_TYPING) {
    9.90 +                  val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
    9.91 +                  state.add_markup(
    9.92 +                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
    9.93 +                }
    9.94 +                else if (kind == Markup.ML_REF) {
    9.95 +                  body match {
    9.96 +                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    9.97 +                      state.add_markup(command.markup_node(
    9.98 +                        begin.get - 1, end.get - 1,
    9.99 +                        Command.RefInfo(
   9.100 +                          Position.get_file(atts),
   9.101 +                          Position.get_line(atts),
   9.102 +                          Position.get_id(atts),
   9.103 +                          Position.get_offset(atts))))
   9.104 +                    case _ => state
   9.105 +                  }
   9.106 +                }
   9.107 +                else {
   9.108 +                  state.add_markup(
   9.109 +                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
   9.110 +                }
   9.111 +              case _ =>
   9.112 +                System.err.println("ignored status report: " + elem)
   9.113 +                state
   9.114 +            })
   9.115 +        case _ => add_result(message)
   9.116 +      }
   9.117 +    if (!(this eq changed)) session.command_change.event(command)
   9.118 +    changed
   9.119 +  }
   9.120 +}
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/PIDE/text_edit.scala	Wed May 05 22:23:45 2010 +0200
    10.3 @@ -0,0 +1,51 @@
    10.4 +/*  Title:      Pure/PIDE/text_edit.scala
    10.5 +    Author:     Fabian Immler, TU Munich
    10.6 +    Author:     Makarius
    10.7 +
    10.8 +Basic edits on plain text.
    10.9 +*/
   10.10 +
   10.11 +package isabelle
   10.12 +
   10.13 +
   10.14 +class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
   10.15 +{
   10.16 +  override def toString =
   10.17 +    (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
   10.18 +
   10.19 +
   10.20 +  /* transform offsets */
   10.21 +
   10.22 +  private def transform(do_insert: Boolean, offset: Int): Int =
   10.23 +    if (offset < start) offset
   10.24 +    else if (is_insert == do_insert) offset + text.length
   10.25 +    else (offset - text.length) max start
   10.26 +
   10.27 +  def after(offset: Int): Int = transform(true, offset)
   10.28 +  def before(offset: Int): Int = transform(false, offset)
   10.29 +
   10.30 +
   10.31 +  /* edit strings */
   10.32 +
   10.33 +  private def insert(index: Int, string: String): String =
   10.34 +    string.substring(0, index) + text + string.substring(index)
   10.35 +
   10.36 +  private def remove(index: Int, count: Int, string: String): String =
   10.37 +    string.substring(0, index) + string.substring(index + count)
   10.38 +
   10.39 +  def can_edit(string: String, shift: Int): Boolean =
   10.40 +    shift <= start && start < shift + string.length
   10.41 +
   10.42 +  def edit(string: String, shift: Int): (Option[Text_Edit], String) =
   10.43 +    if (!can_edit(string, shift)) (Some(this), string)
   10.44 +    else if (is_insert) (None, insert(start - shift, string))
   10.45 +    else {
   10.46 +      val index = start - shift
   10.47 +      val count = text.length min (string.length - index)
   10.48 +      val rest =
   10.49 +        if (count == text.length) None
   10.50 +        else Some(new Text_Edit(false, start, text.substring(count)))
   10.51 +      (rest, remove(index, count, string))
   10.52 +    }
   10.53 +}
   10.54 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/System/download.scala	Wed May 05 22:23:45 2010 +0200
    11.3 @@ -0,0 +1,53 @@
    11.4 +/*  Title:      Pure/System/download.scala
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Download URLs -- with progress monitor.
    11.8 +*/
    11.9 +
   11.10 +package isabelle
   11.11 +
   11.12 +
   11.13 +import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
   11.14 +  File, InterruptedIOException}
   11.15 +import java.net.{URL, URLConnection}
   11.16 +import java.awt.{Component, HeadlessException}
   11.17 +import javax.swing.ProgressMonitorInputStream
   11.18 +
   11.19 +
   11.20 +object Download
   11.21 +{
   11.22 +  def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
   11.23 +  {
   11.24 +    val connection = url.openConnection
   11.25 +
   11.26 +    val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
   11.27 +    val monitor = stream.getProgressMonitor
   11.28 +    monitor.setNote(connection.getURL.toString)
   11.29 +
   11.30 +    val length = connection.getContentLength
   11.31 +    if (length != -1) monitor.setMaximum(length)
   11.32 +
   11.33 +    (connection, new BufferedInputStream(stream))
   11.34 +  }
   11.35 +
   11.36 +  def file(parent: Component, url: URL, file: File)
   11.37 +  {
   11.38 +    val (connection, instream) = stream(parent, url)
   11.39 +    val mod_time = connection.getLastModified
   11.40 +
   11.41 +    def read() =
   11.42 +      try { instream.read }
   11.43 +      catch { case _ : InterruptedIOException => error("Download canceled!") }
   11.44 +    try {
   11.45 +      val outstream = new BufferedOutputStream(new FileOutputStream(file))
   11.46 +      try {
   11.47 +        var c: Int = 0
   11.48 +        while ({ c = read(); c != -1}) outstream.write(c)
   11.49 +      }
   11.50 +      finally { outstream.close }
   11.51 +      if (mod_time > 0) file.setLastModified(mod_time)
   11.52 +    }
   11.53 +    finally { instream.close }
   11.54 +  }
   11.55 +}
   11.56 +
    12.1 --- a/src/Pure/System/session.scala	Wed May 05 15:30:01 2010 +0200
    12.2 +++ b/src/Pure/System/session.scala	Wed May 05 22:23:45 2010 +0200
    12.3 @@ -1,8 +1,8 @@
    12.4 -/*
    12.5 - * Isabelle session, potentially with running prover
    12.6 - *
    12.7 - * @author Makarius
    12.8 - */
    12.9 +/*  Title:      Pure/System/session.scala
   12.10 +    Author:     Makarius
   12.11 +
   12.12 +Isabelle session, potentially with running prover.
   12.13 +*/
   12.14  
   12.15  package isabelle
   12.16  
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Pure/System/swing_thread.scala	Wed May 05 22:23:45 2010 +0200
    13.3 @@ -0,0 +1,63 @@
    13.4 +/*  Title:      Pure/System/swing_thread.scala
    13.5 +    Author:     Makarius
    13.6 +    Author:     Fabian Immler, TU Munich
    13.7 +
    13.8 +Evaluation within the AWT/Swing thread.
    13.9 +*/
   13.10 +
   13.11 +package isabelle
   13.12 +
   13.13 +import javax.swing.{SwingUtilities, Timer}
   13.14 +import java.awt.event.{ActionListener, ActionEvent}
   13.15 +
   13.16 +
   13.17 +object Swing_Thread
   13.18 +{
   13.19 +  /* checks */
   13.20 +
   13.21 +  def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
   13.22 +  def require() = Predef.require(SwingUtilities.isEventDispatchThread())
   13.23 +
   13.24 +
   13.25 +  /* main dispatch queue */
   13.26 +
   13.27 +  def now[A](body: => A): A =
   13.28 +  {
   13.29 +    var result: Option[A] = None
   13.30 +    if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
   13.31 +    else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
   13.32 +    result.get
   13.33 +  }
   13.34 +
   13.35 +  def future[A](body: => A): Future[A] =
   13.36 +  {
   13.37 +    if (SwingUtilities.isEventDispatchThread()) Future.value(body)
   13.38 +    else Future.fork { now(body) }
   13.39 +  }
   13.40 +
   13.41 +  def later(body: => Unit)
   13.42 +  {
   13.43 +    if (SwingUtilities.isEventDispatchThread()) body
   13.44 +    else SwingUtilities.invokeLater(new Runnable { def run = body })
   13.45 +  }
   13.46 +
   13.47 +
   13.48 +  /* delayed actions */
   13.49 +
   13.50 +  private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
   13.51 +  {
   13.52 +    val listener =
   13.53 +      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
   13.54 +    val timer = new Timer(time_span, listener)
   13.55 +    timer.setRepeats(false)
   13.56 +
   13.57 +    def invoke() { if (first) timer.start() else timer.restart() }
   13.58 +    invoke _
   13.59 +  }
   13.60 +
   13.61 +  // delayed action after first invocation
   13.62 +  def delay_first = delayed_action(true) _
   13.63 +
   13.64 +  // delayed action after last invocation
   13.65 +  def delay_last = delayed_action(false) _
   13.66 +}
    14.1 --- a/src/Pure/Thy/change.scala	Wed May 05 15:30:01 2010 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,42 +0,0 @@
    14.4 -/*
    14.5 - * Changes of plain text
    14.6 - *
    14.7 - * @author Fabian Immler, TU Munich
    14.8 - * @author Makarius
    14.9 - */
   14.10 -
   14.11 -package isabelle
   14.12 -
   14.13 -
   14.14 -class Change(
   14.15 -  val id: Isar_Document.Document_ID,
   14.16 -  val parent: Option[Change],
   14.17 -  val edits: List[Text_Edit],
   14.18 -  val result: Future[(List[Document.Edit], Document)])
   14.19 -{
   14.20 -  def ancestors: Iterator[Change] = new Iterator[Change]
   14.21 -  {
   14.22 -    private var state: Option[Change] = Some(Change.this)
   14.23 -    def hasNext = state.isDefined
   14.24 -    def next =
   14.25 -      state match {
   14.26 -        case Some(change) => state = change.parent; change
   14.27 -        case None => throw new NoSuchElementException("next on empty iterator")
   14.28 -      }
   14.29 -  }
   14.30 -
   14.31 -  def join_document: Document = result.join._2
   14.32 -  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
   14.33 -
   14.34 -  def edit(session: Session, edits: List[Text_Edit]): Change =
   14.35 -  {
   14.36 -    val new_id = session.create_id()
   14.37 -    val result: Future[(List[Document.Edit], Document)] =
   14.38 -      Future.fork {
   14.39 -        val old_doc = join_document
   14.40 -        old_doc.await_assignment
   14.41 -        Document.text_edits(session, old_doc, new_id, edits)
   14.42 -      }
   14.43 -    new Change(new_id, Some(this), edits, result)
   14.44 -  }
   14.45 -}
   14.46 \ No newline at end of file
    15.1 --- a/src/Pure/Thy/command.scala	Wed May 05 15:30:01 2010 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,100 +0,0 @@
    15.4 -/*
    15.5 - * Prover commands with semantic state
    15.6 - *
    15.7 - * @author Johannes Hölzl, TU Munich
    15.8 - * @author Fabian Immler, TU Munich
    15.9 - */
   15.10 -
   15.11 -package isabelle
   15.12 -
   15.13 -
   15.14 -import scala.actors.Actor, Actor._
   15.15 -import scala.collection.mutable
   15.16 -
   15.17 -
   15.18 -object Command
   15.19 -{
   15.20 -  object Status extends Enumeration
   15.21 -  {
   15.22 -    val UNPROCESSED = Value("UNPROCESSED")
   15.23 -    val FINISHED = Value("FINISHED")
   15.24 -    val FAILED = Value("FAILED")
   15.25 -  }
   15.26 -
   15.27 -  case class HighlightInfo(highlight: String) { override def toString = highlight }
   15.28 -  case class TypeInfo(ty: String)
   15.29 -  case class RefInfo(file: Option[String], line: Option[Int],
   15.30 -    command_id: Option[String], offset: Option[Int])
   15.31 -}
   15.32 -
   15.33 -
   15.34 -class Command(
   15.35 -    val id: Isar_Document.Command_ID,
   15.36 -    val span: Thy_Syntax.Span)
   15.37 -  extends Session.Entity
   15.38 -{
   15.39 -  /* classification */
   15.40 -
   15.41 -  def is_command: Boolean = !span.isEmpty && span.head.is_command
   15.42 -  def is_ignored: Boolean = span.forall(_.is_ignored)
   15.43 -  def is_malformed: Boolean = !is_command && !is_ignored
   15.44 -
   15.45 -  def name: String = if (is_command) span.head.content else ""
   15.46 -  override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
   15.47 -
   15.48 -
   15.49 -  /* source text */
   15.50 -
   15.51 -  val source: String = span.map(_.source).mkString
   15.52 -  def source(i: Int, j: Int): String = source.substring(i, j)
   15.53 -  def length: Int = source.length
   15.54 -
   15.55 -  lazy val symbol_index = new Symbol.Index(source)
   15.56 -
   15.57 -
   15.58 -  /* accumulated messages */
   15.59 -
   15.60 -  @volatile protected var state = new State(this)
   15.61 -  def current_state: State = state
   15.62 -
   15.63 -  private case class Consume(session: Session, message: XML.Tree)
   15.64 -  private case object Assign
   15.65 -
   15.66 -  private val accumulator = actor {
   15.67 -    var assigned = false
   15.68 -    loop {
   15.69 -      react {
   15.70 -        case Consume(session: Session, message: XML.Tree) if !assigned =>
   15.71 -          state = state.+(session, message)
   15.72 -
   15.73 -        case Assign =>
   15.74 -          assigned = true  // single assignment
   15.75 -          reply(())
   15.76 -
   15.77 -        case bad => System.err.println("command accumulator: ignoring bad message " + bad)
   15.78 -      }
   15.79 -    }
   15.80 -  }
   15.81 -
   15.82 -  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
   15.83 -
   15.84 -  def assign_state(state_id: Isar_Document.State_ID): Command =
   15.85 -  {
   15.86 -    val cmd = new Command(state_id, span)
   15.87 -    accumulator !? Assign
   15.88 -    cmd.state = current_state
   15.89 -    cmd
   15.90 -  }
   15.91 -
   15.92 -
   15.93 -  /* markup */
   15.94 -
   15.95 -  lazy val empty_markup = new Markup_Text(Nil, source)
   15.96 -
   15.97 -  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   15.98 -  {
   15.99 -    val start = symbol_index.decode(begin)
  15.100 -    val stop = symbol_index.decode(end)
  15.101 -    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
  15.102 -  }
  15.103 -}
    16.1 --- a/src/Pure/Thy/document.scala	Wed May 05 15:30:01 2010 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,197 +0,0 @@
    16.4 -/*
    16.5 - * Document as editable list of commands
    16.6 - *
    16.7 - * @author Makarius
    16.8 - */
    16.9 -
   16.10 -package isabelle
   16.11 -
   16.12 -
   16.13 -object Document
   16.14 -{
   16.15 -  /* command start positions */
   16.16 -
   16.17 -  def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
   16.18 -  {
   16.19 -    var offset = 0
   16.20 -    for (cmd <- commands.iterator) yield {
   16.21 -      val start = offset
   16.22 -      offset += cmd.length
   16.23 -      (cmd, start)
   16.24 -    }
   16.25 -  }
   16.26 -
   16.27 -
   16.28 -  /* empty document */
   16.29 -
   16.30 -  def empty(id: Isar_Document.Document_ID): Document =
   16.31 -  {
   16.32 -    val doc = new Document(id, Linear_Set(), Map())
   16.33 -    doc.assign_states(Nil)
   16.34 -    doc
   16.35 -  }
   16.36 -
   16.37 -
   16.38 -  // FIXME
   16.39 -  var phase0: List[Text_Edit] = null
   16.40 -  var phase1: Linear_Set[Command] = null
   16.41 -  var phase2: Linear_Set[Command] = null
   16.42 -  var phase3: List[Edit] = null
   16.43 -
   16.44 -
   16.45 -
   16.46 -  /** document edits **/
   16.47 -
   16.48 -  type Edit = (Option[Command], Option[Command])
   16.49 -
   16.50 -  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
   16.51 -    edits: List[Text_Edit]): (List[Edit], Document) =
   16.52 -  {
   16.53 -    require(old_doc.assignment.is_finished)
   16.54 -
   16.55 -
   16.56 -    /* unparsed dummy commands */
   16.57 -
   16.58 -    def unparsed(source: String) =
   16.59 -      new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
   16.60 -
   16.61 -    def is_unparsed(command: Command) = command.id == null
   16.62 -
   16.63 -    assert(!old_doc.commands.exists(is_unparsed))   // FIXME remove
   16.64 -
   16.65 -
   16.66 -    /* phase 1: edit individual command source */
   16.67 -
   16.68 -    def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
   16.69 -    {
   16.70 -      eds match {
   16.71 -        case e :: es =>
   16.72 -          command_starts(commands).find {   // FIXME relative search!
   16.73 -            case (cmd, cmd_start) =>
   16.74 -              e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
   16.75 -          } match {
   16.76 -            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
   16.77 -              val (rest, text) = e.edit(cmd.source, cmd_start)
   16.78 -              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
   16.79 -              edit_text(rest.toList ::: es, new_commands)
   16.80 -
   16.81 -            case Some((cmd, cmd_start)) =>
   16.82 -              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
   16.83 -
   16.84 -            case None =>
   16.85 -              require(e.is_insert && e.start == 0)
   16.86 -              edit_text(es, commands.insert_after(None, unparsed(e.text)))
   16.87 -          }
   16.88 -        case Nil => commands
   16.89 -      }
   16.90 -    }
   16.91 -
   16.92 -
   16.93 -    /* phase 2: recover command spans */
   16.94 -
   16.95 -    def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
   16.96 -    {
   16.97 -      // FIXME relative search!
   16.98 -      commands.iterator.find(is_unparsed) match {
   16.99 -        case Some(first_unparsed) =>
  16.100 -          val prefix = commands.prev(first_unparsed)
  16.101 -          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
  16.102 -          val suffix = commands.next(body.last)
  16.103 -
  16.104 -          val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
  16.105 -          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
  16.106 -
  16.107 -          val (before_edit, spans1) =
  16.108 -            if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
  16.109 -              (prefix, spans0.tail)
  16.110 -            else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
  16.111 -
  16.112 -          val (after_edit, spans2) =
  16.113 -            if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
  16.114 -              (suffix, spans1.take(spans1.length - 1))
  16.115 -            else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
  16.116 -
  16.117 -          val inserted = spans2.map(span => new Command(session.create_id(), span))
  16.118 -          val new_commands =
  16.119 -            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
  16.120 -          parse_spans(new_commands)
  16.121 -
  16.122 -        case None => commands
  16.123 -      }
  16.124 -    }
  16.125 -
  16.126 -
  16.127 -    /* phase 3: resulting document edits */
  16.128 -
  16.129 -    val result = Library.timeit("text_edits") {
  16.130 -      val commands0 = old_doc.commands
  16.131 -      val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
  16.132 -      val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
  16.133 -
  16.134 -      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
  16.135 -      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
  16.136 -
  16.137 -      val doc_edits =
  16.138 -        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
  16.139 -        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
  16.140 -
  16.141 -      val former_states = old_doc.assignment.join -- removed_commands
  16.142 -
  16.143 -      phase0 = edits
  16.144 -      phase1 = commands1
  16.145 -      phase2 = commands2
  16.146 -      phase3 = doc_edits
  16.147 -
  16.148 -      (doc_edits, new Document(new_id, commands2, former_states))
  16.149 -    }
  16.150 -    result
  16.151 -  }
  16.152 -}
  16.153 -
  16.154 -
  16.155 -class Document(
  16.156 -    val id: Isar_Document.Document_ID,
  16.157 -    val commands: Linear_Set[Command],
  16.158 -    former_states: Map[Command, Command])
  16.159 -{
  16.160 -  /* command ranges */
  16.161 -
  16.162 -  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
  16.163 -
  16.164 -  def command_start(cmd: Command): Option[Int] =
  16.165 -    command_starts.find(_._1 == cmd).map(_._2)
  16.166 -
  16.167 -  def command_range(i: Int): Iterator[(Command, Int)] =
  16.168 -    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
  16.169 -
  16.170 -  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
  16.171 -    command_range(i) takeWhile { case (_, start) => start < j }
  16.172 -
  16.173 -  def command_at(i: Int): Option[(Command, Int)] =
  16.174 -  {
  16.175 -    val range = command_range(i)
  16.176 -    if (range.hasNext) Some(range.next) else None
  16.177 -  }
  16.178 -
  16.179 -
  16.180 -  /* command state assignment */
  16.181 -
  16.182 -  val assignment = Future.promise[Map[Command, Command]]
  16.183 -  def await_assignment { assignment.join }
  16.184 -
  16.185 -  @volatile private var tmp_states = former_states
  16.186 -  private val time0 = System.currentTimeMillis
  16.187 -
  16.188 -  def assign_states(new_states: List[(Command, Command)])
  16.189 -  {
  16.190 -    assignment.fulfill(tmp_states ++ new_states)
  16.191 -    tmp_states = Map()
  16.192 -    System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
  16.193 -  }
  16.194 -
  16.195 -  def current_state(cmd: Command): Option[State] =
  16.196 -  {
  16.197 -    require(assignment.is_finished)
  16.198 -    (assignment.join).get(cmd).map(_.current_state)
  16.199 -  }
  16.200 -}
    17.1 --- a/src/Pure/Thy/markup_node.scala	Wed May 05 15:30:01 2010 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,111 +0,0 @@
    17.4 -/*
    17.5 - * Document markup nodes, with connection to Swing tree model
    17.6 - *
    17.7 - * @author Fabian Immler, TU Munich
    17.8 - * @author Makarius
    17.9 - */
   17.10 -
   17.11 -package isabelle
   17.12 -
   17.13 -
   17.14 -import javax.swing.tree.DefaultMutableTreeNode
   17.15 -
   17.16 -
   17.17 -
   17.18 -class Markup_Node(val start: Int, val stop: Int, val info: Any)
   17.19 -{
   17.20 -  def fits_into(that: Markup_Node): Boolean =
   17.21 -    that.start <= this.start && this.stop <= that.stop
   17.22 -}
   17.23 -
   17.24 -
   17.25 -class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
   17.26 -{
   17.27 -  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
   17.28 -
   17.29 -  private def add(branch: Markup_Tree) =   // FIXME avoid sort
   17.30 -    set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
   17.31 -
   17.32 -  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
   17.33 -
   17.34 -  def + (new_tree: Markup_Tree): Markup_Tree =
   17.35 -  {
   17.36 -    val new_node = new_tree.node
   17.37 -    if (new_node fits_into node) {
   17.38 -      var inserted = false
   17.39 -      val new_branches =
   17.40 -        branches.map(branch =>
   17.41 -          if ((new_node fits_into branch.node) && !inserted) {
   17.42 -            inserted = true
   17.43 -            branch + new_tree
   17.44 -          }
   17.45 -          else branch)
   17.46 -      if (!inserted) {
   17.47 -        // new_tree did not fit into children of this
   17.48 -        // -> insert between this and its branches
   17.49 -        val fitting = branches filter(_.node fits_into new_node)
   17.50 -        (this remove fitting) add ((new_tree /: fitting)(_ + _))
   17.51 -      }
   17.52 -      else set_branches(new_branches)
   17.53 -    }
   17.54 -    else {
   17.55 -      System.err.println("ignored nonfitting markup: " + new_node)
   17.56 -      this
   17.57 -    }
   17.58 -  }
   17.59 -
   17.60 -  def flatten: List[Markup_Node] =
   17.61 -  {
   17.62 -    var next_x = node.start
   17.63 -    if (branches.isEmpty) List(this.node)
   17.64 -    else {
   17.65 -      val filled_gaps =
   17.66 -        for {
   17.67 -          child <- branches
   17.68 -          markups =
   17.69 -            if (next_x < child.node.start)
   17.70 -              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
   17.71 -            else child.flatten
   17.72 -          update = (next_x = child.node.stop)
   17.73 -          markup <- markups
   17.74 -        } yield markup
   17.75 -      if (next_x < node.stop)
   17.76 -        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
   17.77 -      else filled_gaps
   17.78 -    }
   17.79 -  }
   17.80 -}
   17.81 -
   17.82 -
   17.83 -class Markup_Text(val markup: List[Markup_Tree], val content: String)
   17.84 -{
   17.85 -  private lazy val root =
   17.86 -    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
   17.87 -
   17.88 -  def + (new_tree: Markup_Tree): Markup_Text =
   17.89 -    new Markup_Text((root + new_tree).branches, content)
   17.90 -
   17.91 -  def filter(pred: Markup_Node => Boolean): Markup_Text =
   17.92 -  {
   17.93 -    def filt(tree: Markup_Tree): List[Markup_Tree] =
   17.94 -    {
   17.95 -      val branches = tree.branches.flatMap(filt(_))
   17.96 -      if (pred(tree.node)) List(tree.set_branches(branches))
   17.97 -      else branches
   17.98 -    }
   17.99 -    new Markup_Text(markup.flatMap(filt(_)), content)
  17.100 -  }
  17.101 -
  17.102 -  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
  17.103 -
  17.104 -  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
  17.105 -  {
  17.106 -    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
  17.107 -    {
  17.108 -      val node = swing_node(tree.node)
  17.109 -      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
  17.110 -      node
  17.111 -    }
  17.112 -    swing(root)
  17.113 -  }
  17.114 -}
    18.1 --- a/src/Pure/Thy/state.scala	Wed May 05 15:30:01 2010 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,117 +0,0 @@
    18.4 -/*
    18.5 - * Accumulating results from prover
    18.6 - *
    18.7 - * @author Fabian Immler, TU Munich
    18.8 - * @author Makarius
    18.9 - */
   18.10 -
   18.11 -package isabelle
   18.12 -
   18.13 -
   18.14 -class State(
   18.15 -  val command: Command,
   18.16 -  val status: Command.Status.Value,
   18.17 -  val rev_results: List[XML.Tree],
   18.18 -  val markup_root: Markup_Text)
   18.19 -{
   18.20 -  def this(command: Command) =
   18.21 -    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
   18.22 -
   18.23 -
   18.24 -  /* content */
   18.25 -
   18.26 -  private def set_status(st: Command.Status.Value): State =
   18.27 -    new State(command, st, rev_results, markup_root)
   18.28 -
   18.29 -  private def add_result(res: XML.Tree): State =
   18.30 -    new State(command, status, res :: rev_results, markup_root)
   18.31 -
   18.32 -  private def add_markup(node: Markup_Tree): State =
   18.33 -    new State(command, status, rev_results, markup_root + node)
   18.34 -
   18.35 -  lazy val results = rev_results.reverse
   18.36 -
   18.37 -
   18.38 -  /* markup */
   18.39 -
   18.40 -  lazy val highlight: Markup_Text =
   18.41 -  {
   18.42 -    markup_root.filter(_.info match {
   18.43 -      case Command.HighlightInfo(_) => true
   18.44 -      case _ => false
   18.45 -    })
   18.46 -  }
   18.47 -
   18.48 -  private lazy val types: List[Markup_Node] =
   18.49 -    markup_root.filter(_.info match {
   18.50 -      case Command.TypeInfo(_) => true
   18.51 -      case _ => false }).flatten
   18.52 -
   18.53 -  def type_at(pos: Int): Option[String] =
   18.54 -  {
   18.55 -    types.find(t => t.start <= pos && pos < t.stop) match {
   18.56 -      case Some(t) =>
   18.57 -        t.info match {
   18.58 -          case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
   18.59 -          case _ => None
   18.60 -        }
   18.61 -      case None => None
   18.62 -    }
   18.63 -  }
   18.64 -
   18.65 -  private lazy val refs: List[Markup_Node] =
   18.66 -    markup_root.filter(_.info match {
   18.67 -      case Command.RefInfo(_, _, _, _) => true
   18.68 -      case _ => false }).flatten
   18.69 -
   18.70 -  def ref_at(pos: Int): Option[Markup_Node] =
   18.71 -    refs.find(t => t.start <= pos && pos < t.stop)
   18.72 -
   18.73 -
   18.74 -  /* message dispatch */
   18.75 -
   18.76 -  def + (session: Session, message: XML.Tree): State =
   18.77 -  {
   18.78 -    val changed: State =
   18.79 -      message match {
   18.80 -        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
   18.81 -          (this /: elems)((state, elem) =>
   18.82 -            elem match {
   18.83 -              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
   18.84 -              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
   18.85 -              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
   18.86 -              case XML.Elem(kind, atts, body) =>
   18.87 -                val (begin, end) = Position.get_offsets(atts)
   18.88 -                if (begin.isEmpty || end.isEmpty) state
   18.89 -                else if (kind == Markup.ML_TYPING) {
   18.90 -                  val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
   18.91 -                  state.add_markup(
   18.92 -                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
   18.93 -                }
   18.94 -                else if (kind == Markup.ML_REF) {
   18.95 -                  body match {
   18.96 -                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
   18.97 -                      state.add_markup(command.markup_node(
   18.98 -                        begin.get - 1, end.get - 1,
   18.99 -                        Command.RefInfo(
  18.100 -                          Position.get_file(atts),
  18.101 -                          Position.get_line(atts),
  18.102 -                          Position.get_id(atts),
  18.103 -                          Position.get_offset(atts))))
  18.104 -                    case _ => state
  18.105 -                  }
  18.106 -                }
  18.107 -                else {
  18.108 -                  state.add_markup(
  18.109 -                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
  18.110 -                }
  18.111 -              case _ =>
  18.112 -                System.err.println("ignored status report: " + elem)
  18.113 -                state
  18.114 -            })
  18.115 -        case _ => add_result(message)
  18.116 -      }
  18.117 -    if (!(this eq changed)) session.command_change.event(command)
  18.118 -    changed
  18.119 -  }
  18.120 -}
    19.1 --- a/src/Pure/Thy/text_edit.scala	Wed May 05 15:30:01 2010 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,51 +0,0 @@
    19.4 -/*  Title:      Pure/Thy/text_edit.scala
    19.5 -    Author:     Fabian Immler, TU Munich
    19.6 -    Author:     Makarius
    19.7 -
    19.8 -Basic edits on plain text.
    19.9 -*/
   19.10 -
   19.11 -package isabelle
   19.12 -
   19.13 -
   19.14 -class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
   19.15 -{
   19.16 -  override def toString =
   19.17 -    (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
   19.18 -
   19.19 -
   19.20 -  /* transform offsets */
   19.21 -
   19.22 -  private def transform(do_insert: Boolean, offset: Int): Int =
   19.23 -    if (offset < start) offset
   19.24 -    else if (is_insert == do_insert) offset + text.length
   19.25 -    else (offset - text.length) max start
   19.26 -
   19.27 -  def after(offset: Int): Int = transform(true, offset)
   19.28 -  def before(offset: Int): Int = transform(false, offset)
   19.29 -
   19.30 -
   19.31 -  /* edit strings */
   19.32 -
   19.33 -  private def insert(index: Int, string: String): String =
   19.34 -    string.substring(0, index) + text + string.substring(index)
   19.35 -
   19.36 -  private def remove(index: Int, count: Int, string: String): String =
   19.37 -    string.substring(0, index) + string.substring(index + count)
   19.38 -
   19.39 -  def can_edit(string: String, shift: Int): Boolean =
   19.40 -    shift <= start && start < shift + string.length
   19.41 -
   19.42 -  def edit(string: String, shift: Int): (Option[Text_Edit], String) =
   19.43 -    if (!can_edit(string, shift)) (Some(this), string)
   19.44 -    else if (is_insert) (None, insert(start - shift, string))
   19.45 -    else {
   19.46 -      val index = start - shift
   19.47 -      val count = text.length min (string.length - index)
   19.48 -      val rest =
   19.49 -        if (count == text.length) None
   19.50 -        else Some(new Text_Edit(false, start, text.substring(count)))
   19.51 -      (rest, remove(index, count, string))
   19.52 -    }
   19.53 -}
   19.54 -
    20.1 --- a/src/Pure/build-jars	Wed May 05 15:30:01 2010 +0200
    20.2 +++ b/src/Pure/build-jars	Wed May 05 22:23:45 2010 +0200
    20.3 @@ -23,14 +23,11 @@
    20.4  
    20.5  declare -a SOURCES=(
    20.6    Concurrent/future.scala
    20.7 -  General/download.scala
    20.8 -  General/event_bus.scala
    20.9    General/exn.scala
   20.10    General/linear_set.scala
   20.11    General/markup.scala
   20.12    General/position.scala
   20.13    General/scan.scala
   20.14 -  General/swing_thread.scala
   20.15    General/symbol.scala
   20.16    General/xml.scala
   20.17    General/yxml.scala
   20.18 @@ -39,7 +36,15 @@
   20.19    Isar/outer_lex.scala
   20.20    Isar/outer_parse.scala
   20.21    Isar/outer_syntax.scala
   20.22 +  PIDE/change.scala
   20.23 +  PIDE/command.scala
   20.24 +  PIDE/document.scala
   20.25 +  PIDE/event_bus.scala
   20.26 +  PIDE/markup_node.scala
   20.27 +  PIDE/state.scala
   20.28 +  PIDE/text_edit.scala
   20.29    System/cygwin.scala
   20.30 +  System/download.scala
   20.31    System/gui_setup.scala
   20.32    System/isabelle_process.scala
   20.33    System/isabelle_syntax.scala
   20.34 @@ -48,14 +53,9 @@
   20.35    System/session.scala
   20.36    System/session_manager.scala
   20.37    System/standard_system.scala
   20.38 -  Thy/change.scala
   20.39 -  Thy/command.scala
   20.40 +  System/swing_thread.scala
   20.41    Thy/completion.scala
   20.42 -  Thy/document.scala
   20.43    Thy/html.scala
   20.44 -  Thy/markup_node.scala
   20.45 -  Thy/state.scala
   20.46 -  Thy/text_edit.scala
   20.47    Thy/thy_header.scala
   20.48    Thy/thy_syntax.scala
   20.49    library.scala