# HG changeset patch # User wenzelm # Date 1273236429 -7200 # Node ID 51e3b38a5e412b7d422bf6327c212e90d6f4a264 # Parent 47ba1770da8e4a4464bca536807e01444c916907# Parent 97d2780ad6f0deda2821af15a92f680ed049b3e8 merged diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/download.scala --- a/src/Pure/General/download.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -/* Title: Pure/General/download.scala - Author: Makarius - -Download URLs -- with progress monitor. -*/ - -package isabelle - - -import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, - File, InterruptedIOException} -import java.net.{URL, URLConnection} -import java.awt.{Component, HeadlessException} -import javax.swing.ProgressMonitorInputStream - - -object Download -{ - def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) = - { - val connection = url.openConnection - - val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream) - val monitor = stream.getProgressMonitor - monitor.setNote(connection.getURL.toString) - - val length = connection.getContentLength - if (length != -1) monitor.setMaximum(length) - - (connection, new BufferedInputStream(stream)) - } - - def file(parent: Component, url: URL, file: File) - { - val (connection, instream) = stream(parent, url) - val mod_time = connection.getLastModified - - def read() = - try { instream.read } - catch { case _ : InterruptedIOException => error("Download canceled!") } - try { - val outstream = new BufferedOutputStream(new FileOutputStream(file)) - try { - var c: Int = 0 - while ({ c = read(); c != -1}) outstream.write(c) - } - finally { outstream.close } - if (mod_time > 0) file.setLastModified(mod_time) - } - finally { instream.close } - } -} - diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/event_bus.scala --- a/src/Pure/General/event_bus.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -/* Title: Pure/General/event_bus.scala - Author: Makarius - -Generic event bus with multiple receiving actors. -*/ - -package isabelle - -import scala.actors.Actor, Actor._ -import scala.collection.mutable.ListBuffer - - -class Event_Bus[Event] -{ - /* receivers */ - - private val receivers = new ListBuffer[Actor] - - def += (r: Actor) { synchronized { receivers += r } } - def + (r: Actor): Event_Bus[Event] = { this += r; this } - - def += (f: Event => Unit) { - this += actor { loop { react { case x: Event => f(x) } } } - } - - def + (f: Event => Unit): Event_Bus[Event] = { this += f; this } - - def -= (r: Actor) { synchronized { receivers -= r } } - def - (r: Actor) = { this -= r; this } - - - /* event invocation */ - - def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } -} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/General/markup.scala Fri May 07 14:47:09 2010 +0200 @@ -9,6 +9,24 @@ object Markup { + /* property values */ + + def get_string(name: String, props: List[(String, String)]): Option[String] = + props.find(p => p._1 == name).map(_._2) + + def parse_int(s: String): Option[Int] = + try { Some(Integer.parseInt(s)) } + catch { case _: NumberFormatException => None } + + def get_int(name: String, props: List[(String, String)]): Option[Int] = + { + get_string(name, props) match { + case None => None + case Some(value) => parse_int(value) + } + } + + /* name */ val NAME = "name" @@ -40,6 +58,14 @@ val LOCATION = "location" + /* pretty printing */ + + val INDENT = "indent" + val BLOCK = "block" + val WIDTH = "width" + val BREAK = "break" + + /* hidden text */ val HIDDEN = "hidden" diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/General/position.scala Fri May 07 14:47:09 2010 +0200 @@ -11,32 +11,22 @@ { type T = List[(String, String)] - private def get_string(name: String, pos: T): Option[String] = - pos.find(p => p._1 == name).map(_._2) - - private def get_int(name: String, pos: T): Option[Int] = - { - get_string(name, pos) match { - case None => None - case Some(value) => - try { Some(Integer.parseInt(value)) } - catch { case _: NumberFormatException => None } - } - } + def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos) + def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos) + def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos) + def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos) + def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos) + def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos) + def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos) + def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos) - def get_line(pos: T): Option[Int] = get_int(Markup.LINE, pos) - def get_column(pos: T): Option[Int] = get_int(Markup.COLUMN, pos) - def get_offset(pos: T): Option[Int] = get_int(Markup.OFFSET, pos) - def get_end_line(pos: T): Option[Int] = get_int(Markup.END_LINE, pos) - def get_end_column(pos: T): Option[Int] = get_int(Markup.END_COLUMN, pos) - def get_end_offset(pos: T): Option[Int] = get_int(Markup.END_OFFSET, pos) - def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos) - def get_id(pos: T): Option[String] = get_string(Markup.ID, pos) + def get_range(pos: T): Option[(Int, Int)] = + (get_offset(pos), get_end_offset(pos)) match { + case (Some(begin), Some(end)) => Some(begin, end) + case (Some(begin), None) => Some(begin, begin + 1) + case (None, _) => None + } - def get_offsets(pos: T): (Option[Int], Option[Int]) = - { - val begin = get_offset(pos) - val end = get_end_offset(pos) - (begin, if (end.isDefined) end else begin.map(_ + 1)) - } + object Id { def unapply(pos: T): Option[String] = get_id(pos) } + object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) } } diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/General/pretty.ML Fri May 07 14:47:09 2010 +0200 @@ -119,7 +119,7 @@ val str = String o Output.output_width; fun brk wd = Break (false, wd); -val fbrk = Break (true, 2); +val fbrk = Break (true, 1); fun breaks prts = Library.separate (brk 1) prts; fun fbreaks prts = Library.separate fbrk prts; @@ -249,14 +249,14 @@ (*Add the lengths of the expressions until the next Break; if no Break then include "after", to account for text following this block.*) -fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after) +fun breakdist (Break _ :: _, _) = 0 + | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after) | breakdist (String (_, len) :: es, after) = len + breakdist (es, after) - | breakdist (Break _ :: _, _) = 0 | breakdist ([], after) = after; (*Search for the next break (at this or higher levels) and force it to occur.*) fun forcenext [] = [] - | forcenext (Break _ :: es) = Break (true, 0) :: es + | forcenext (Break _ :: es) = fbrk :: es | forcenext (e :: es) = e :: forcenext es; (*es is list of expressions to print; @@ -280,7 +280,6 @@ (*if this block was broken then force the next break*) val es' = if nl < #nl btext then forcenext es else es; in format (es', block, after) btext end - | String str => format (es, block, after) (string str text) | Break (force, wd) => let val {margin, breakgain, ...} = ! margin_info in (*no break if text to next break fits on this line @@ -290,7 +289,8 @@ pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain) then text |> blanks wd (*just insert wd blanks*) else text |> newline |> indentation block) - end); + end + | String str => format (es, block, after) (string str text)); in @@ -309,7 +309,7 @@ Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en | out (String (s, _)) = Buffer.add s | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd)) - | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1)); + | out (Break (true, _)) = Buffer.add (Output.output "\n"); in out prt Buffer.empty end; (*unformatted output*) @@ -317,8 +317,7 @@ let fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en | fmt (String (s, _)) = Buffer.add s - | fmt (Break (false, wd)) = Buffer.add (output_spaces wd) - | fmt (Break (true, _)) = Buffer.add (output_spaces 1); + | fmt (Break (_, wd)) = Buffer.add (output_spaces wd); in fmt (prune prt) Buffer.empty end; diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/pretty.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/pretty.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,111 @@ +/* Title: Pure/General/pretty.scala + Author: Makarius + +Generic pretty printing module. +*/ + +package isabelle + + +object Pretty +{ + /* markup trees with physical blocks and breaks */ + + object Block + { + def apply(indent: Int, body: List[XML.Tree]): XML.Tree = + XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body) + + def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] = + tree match { + case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) => + Markup.parse_int(indent) match { + case Some(i) => Some((i, body)) + case None => None + } + case _ => None + } + } + + object Break + { + def apply(width: Int): XML.Tree = + XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), List(XML.Text(" " * width))) + + def unapply(tree: XML.Tree): Option[Int] = + tree match { + case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width) + case _ => None + } + } + + val FBreak = XML.Text("\n") + + + /* formatted output */ + + private case class Text(tx: List[String] = Nil, val pos: Int = 0, val nl: Int = 0) + { + def newline: Text = copy(tx = "\n" :: tx, pos = 0, nl = nl + 1) + def string(s: String): Text = copy(tx = s :: tx, pos = pos + s.length) + def blanks(wd: Int): Text = string(" " * wd) + def content: String = tx.reverse.mkString + } + + private def breakdist(trees: List[XML.Tree], after: Int): Int = + trees match { + case Break(_) :: _ => 0 + case FBreak :: _ => 0 + case XML.Elem(_, _, body) :: ts => + (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after) + case XML.Text(s) :: ts => s.length + breakdist(ts, after) + case Nil => after + } + + private def forcenext(trees: List[XML.Tree]): List[XML.Tree] = + trees match { + case Nil => Nil + case FBreak :: _ => trees + case Break(_) :: ts => FBreak :: ts + case t :: ts => t :: forcenext(ts) + } + + private def standard(tree: XML.Tree): List[XML.Tree] = + tree match { + case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard))) + case XML.Text(text) => + Library.separate(FBreak, + Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString))) + } + + def string_of(input: List[XML.Tree], margin: Int = 76): String = + { + val breakgain = margin / 20 + val emergencypos = margin / 2 + + def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text = + trees match { + case Nil => text + + case Block(indent, body) :: ts => + val pos1 = text.pos + indent + val pos2 = pos1 % emergencypos + val blockin1 = + if (pos1 < emergencypos) pos1 + else pos2 + val btext = format(body, blockin1, breakdist(ts, after), text) + val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts + format(ts1, blockin, after, btext) + + case Break(wd) :: ts => + if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain)) + format(ts, blockin, after, text.blanks(wd)) + else format(ts, blockin, after, text.newline.blanks(blockin)) + case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin)) + + case XML.Elem(_, _, body) :: ts => format(body ::: ts, blockin, after, text) + case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s)) + } + format(input.flatMap(standard), 0, 0, Text()).content + } +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/General/scan.scala Fri May 07 14:47:09 2010 +0200 @@ -8,6 +8,7 @@ import scala.collection.generic.Addable +import scala.collection.IndexedSeq import scala.collection.immutable.PagedSeq import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader} import scala.util.parsing.combinator.RegexParsers @@ -306,7 +307,7 @@ /** read file without decoding -- enables efficient length operation **/ - private class Restricted_Seq(seq: RandomAccessSeq[Char], start: Int, end: Int) + private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int) extends CharSequence { def charAt(i: Int): Char = diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/swing_thread.scala --- a/src/Pure/General/swing_thread.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -/* Title: Pure/General/swing_thread.scala - Author: Makarius - Author: Fabian Immler, TU Munich - -Evaluation within the AWT/Swing thread. -*/ - -package isabelle - -import javax.swing.{SwingUtilities, Timer} -import java.awt.event.{ActionListener, ActionEvent} - - -object Swing_Thread -{ - /* checks */ - - def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) - def require() = Predef.require(SwingUtilities.isEventDispatchThread()) - - - /* main dispatch queue */ - - def now[A](body: => A): A = - { - var result: Option[A] = None - if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } - else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) - result.get - } - - def future[A](body: => A): Future[A] = - { - if (SwingUtilities.isEventDispatchThread()) Future.value(body) - else Future.fork { now(body) } - } - - def later(body: => Unit) - { - if (SwingUtilities.isEventDispatchThread()) body - else SwingUtilities.invokeLater(new Runnable { def run = body }) - } - - - /* delayed actions */ - - private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit = - { - val listener = - new ActionListener { override def actionPerformed(e: ActionEvent) { action } } - val timer = new Timer(time_span, listener) - timer.setRepeats(false) - - def invoke() { if (first) timer.start() else timer.restart() } - invoke _ - } - - // delayed action after first invocation - def delay_first = delayed_action(true) _ - - // delayed action after last invocation - def delay_last = delayed_action(false) _ -} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/xml.scala --- a/src/Pure/General/xml.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/General/xml.scala Fri May 07 14:47:09 2010 +0200 @@ -92,6 +92,12 @@ } } + def content_length(tree: XML.Tree): Int = + tree match { + case Elem(_, _, body) => (0 /: body)(_ + content_length(_)) + case Text(s) => s.length + } + /* cache for partial sharing -- NOT THREAD SAFE */ diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/General/yxml.scala Fri May 07 14:47:09 2010 +0200 @@ -7,6 +7,9 @@ package isabelle +import scala.collection.mutable.ListBuffer + + object YXML { /* chunk markers */ @@ -17,29 +20,6 @@ private val Y_string = Y.toString - /* iterate over chunks (resembles space_explode in ML) */ - - private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] - { - private val end = source.length - private var state = if (end == 0) None else get_chunk(-1) - private def get_chunk(i: Int) = - { - if (i < end) { - var j = i; do j += 1 while (j < end && source.charAt(j) != sep) - Some((source.subSequence(i + 1, j), j)) - } - else None - } - - def hasNext() = state.isDefined - def next() = state match { - case Some((s, i)) => { state = get_chunk(i); s } - case None => throw new NoSuchElementException("next on empty iterator") - } - } - - /* decoding pseudo UTF-8 */ private class Decode_Chars(decode: String => String, @@ -83,30 +63,36 @@ { /* stack operations */ - var stack: List[((String, XML.Attributes), List[XML.Tree])] = null + def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree] + var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer())) - def add(x: XML.Tree) = (stack: @unchecked) match { - case ((elem, body) :: pending) => stack = (elem, x :: body) :: pending + def add(x: XML.Tree) + { + (stack: @unchecked) match { case ((_, body) :: _) => body += x } } - def push(name: String, atts: XML.Attributes) = + def push(name: String, atts: XML.Attributes) + { if (name == "") err_element() - else stack = ((name, atts), Nil) :: stack + else stack = ((name, atts), buffer()) :: stack + } - def pop() = (stack: @unchecked) match { - case ((("", _), _) :: _) => err_unbalanced("") - case (((name, atts), body) :: pending) => - stack = pending; add(XML.Elem(name, atts, body.reverse)) + def pop() + { + (stack: @unchecked) match { + case ((("", _), _) :: _) => err_unbalanced("") + case (((name, atts), body) :: pending) => + stack = pending; add(XML.Elem(name, atts, body.toList)) + } } /* parse chunks */ - stack = List((("", Nil), Nil)) - for (chunk <- chunks(X, source) if chunk.length != 0) { + for (chunk <- Library.chunks(source, X) if chunk.length != 0) { if (chunk.length == 1 && chunk.charAt(0) == Y) pop() else { - chunks(Y, chunk).toList match { + Library.chunks(chunk, Y).toList match { case ch :: name :: atts if ch.length == 0 => push(name.toString.intern, atts.map(parse_attrib)) case txts => for (txt <- txts) add(XML.Text(txt.toString)) @@ -114,7 +100,7 @@ } } stack match { - case List((("", _), result)) => result.reverse + case List((("", _), body)) => body.toList case ((name, _), _) :: _ => err_unbalanced(name) } } diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Isar/isar_document.scala --- a/src/Pure/Isar/isar_document.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/Isar/isar_document.scala Fri May 07 14:47:09 2010 +0200 @@ -14,6 +14,26 @@ type State_ID = String type Command_ID = String type Document_ID = String + + + /* reports */ + + object Assign { + def unapply(msg: XML.Tree): Option[List[XML.Tree]] = + msg match { + case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits) + case _ => None + } + } + + object Edit { + def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] = + msg match { + case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) => + Some(cmd_id, state_id) + case _ => None + } + } } diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Isar/outer_keyword.ML --- a/src/Pure/Isar/outer_keyword.ML Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/Isar/outer_keyword.ML Fri May 07 14:47:09 2010 +0200 @@ -146,7 +146,7 @@ fun command_tags name = these (Option.map tags_of (command_keyword name)); -(* report *) +(* reports *) val keyword_status_reportN = "keyword_status_report"; diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Isar/outer_keyword.scala --- a/src/Pure/Isar/outer_keyword.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/Isar/outer_keyword.scala Fri May 07 14:47:09 2010 +0200 @@ -9,6 +9,8 @@ object Outer_Keyword { + /* kinds */ + val MINOR = "minor" val CONTROL = "control" val DIAG = "diag" @@ -33,6 +35,9 @@ val PRF_ASM_GOAL = "proof-asm-goal" val PRF_SCRIPT = "proof-script" + + /* categories */ + val minor = Set(MINOR) val control = Set(CONTROL) val diag = Set(DIAG) @@ -43,5 +48,25 @@ Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL) val proof2 = Set(PRF_ASM, PRF_ASM_GOAL) val improper = Set(THY_SCRIPT, PRF_SCRIPT) + + + /* reports */ + + object Keyword_Decl { + def unapply(msg: XML.Tree): Option[String] = + msg match { + case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name) + case _ => None + } + } + + object Command_Decl { + def unapply(msg: XML.Tree): Option[(String, String)] = + msg match { + case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) => + Some((name, kind)) + case _ => None + } + } } diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/change.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/change.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,42 @@ +/* Title: Pure/PIDE/change.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Changes of plain text. +*/ + +package isabelle + + +class Change( + val id: Isar_Document.Document_ID, + val parent: Option[Change], + val edits: List[Text_Edit], + val result: Future[(List[Document.Edit], Document)]) +{ + def ancestors: Iterator[Change] = new Iterator[Change] + { + private var state: Option[Change] = Some(Change.this) + def hasNext = state.isDefined + def next = + state match { + case Some(change) => state = change.parent; change + case None => throw new NoSuchElementException("next on empty iterator") + } + } + + def join_document: Document = result.join._2 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished + + def edit(session: Session, edits: List[Text_Edit]): Change = + { + val new_id = session.create_id() + val result: Future[(List[Document.Edit], Document)] = + Future.fork { + val old_doc = join_document + old_doc.await_assignment + Document.text_edits(session, old_doc, new_id, edits) + } + new Change(new_id, Some(this), edits, result) + } +} \ No newline at end of file diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/command.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/command.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,101 @@ +/* Title: Pure/PIDE/command.scala + Author: Johannes Hölzl, TU Munich + Author: Fabian Immler, TU Munich + Author: Makarius + +Prover commands with semantic state. +*/ + +package isabelle + + +import scala.actors.Actor, Actor._ +import scala.collection.mutable + + +object Command +{ + object Status extends Enumeration + { + val UNPROCESSED = Value("UNPROCESSED") + val FINISHED = Value("FINISHED") + val FAILED = Value("FAILED") + } + + case class HighlightInfo(highlight: String) { override def toString = highlight } + case class TypeInfo(ty: String) + case class RefInfo(file: Option[String], line: Option[Int], + command_id: Option[String], offset: Option[Int]) +} + + +class Command( + val id: Isar_Document.Command_ID, + val span: Thy_Syntax.Span) + extends Session.Entity +{ + /* classification */ + + def is_command: Boolean = !span.isEmpty && span.head.is_command + def is_ignored: Boolean = span.forall(_.is_ignored) + def is_malformed: Boolean = !is_command && !is_ignored + + def name: String = if (is_command) span.head.content else "" + override def toString = if (is_command) name else if (is_ignored) "" else "" + + + /* source text */ + + val source: String = span.map(_.source).mkString + def source(i: Int, j: Int): String = source.substring(i, j) + def length: Int = source.length + + lazy val symbol_index = new Symbol.Index(source) + + + /* accumulated messages */ + + @volatile protected var state = new State(this) + def current_state: State = state + + private case class Consume(session: Session, message: XML.Tree) + private case object Assign + + private val accumulator = actor { + var assigned = false + loop { + react { + case Consume(session: Session, message: XML.Tree) if !assigned => + state = state.+(session, message) + + case Assign => + assigned = true // single assignment + reply(()) + + case bad => System.err.println("command accumulator: ignoring bad message " + bad) + } + } + } + + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } + + def assign_state(state_id: Isar_Document.State_ID): Command = + { + val cmd = new Command(state_id, span) + accumulator !? Assign + cmd.state = current_state + cmd + } + + + /* markup */ + + lazy val empty_markup = new Markup_Text(Nil, source) + + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = + { + val start = symbol_index.decode(begin) + val stop = symbol_index.decode(end) + new Markup_Tree(new Markup_Node(start, stop, info), Nil) + } +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/document.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/document.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,197 @@ +/* Title: Pure/PIDE/document.scala + Author: Makarius + +Document as editable list of commands. +*/ + +package isabelle + + +object Document +{ + /* command start positions */ + + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] = + { + var offset = 0 + for (cmd <- commands.iterator) yield { + val start = offset + offset += cmd.length + (cmd, start) + } + } + + + /* empty document */ + + def empty(id: Isar_Document.Document_ID): Document = + { + val doc = new Document(id, Linear_Set(), Map()) + doc.assign_states(Nil) + doc + } + + + // FIXME + var phase0: List[Text_Edit] = null + var phase1: Linear_Set[Command] = null + var phase2: Linear_Set[Command] = null + var phase3: List[Edit] = null + + + + /** document edits **/ + + type Edit = (Option[Command], Option[Command]) + + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, + edits: List[Text_Edit]): (List[Edit], Document) = + { + require(old_doc.assignment.is_finished) + + + /* unparsed dummy commands */ + + def unparsed(source: String) = + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) + + def is_unparsed(command: Command) = command.id == null + + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove + + + /* phase 1: edit individual command source */ + + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = + { + eds match { + case e :: es => + command_starts(commands).find { // FIXME relative search! + case (cmd, cmd_start) => + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length + } match { + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => + val (rest, text) = e.edit(cmd.source, cmd_start) + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd + edit_text(rest.toList ::: es, new_commands) + + case Some((cmd, cmd_start)) => + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) + + case None => + require(e.is_insert && e.start == 0) + edit_text(es, commands.insert_after(None, unparsed(e.text))) + } + case Nil => commands + } + } + + + /* phase 2: recover command spans */ + + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = + { + // FIXME relative search! + commands.iterator.find(is_unparsed) match { + case Some(first_unparsed) => + val prefix = commands.prev(first_unparsed) + val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList + val suffix = commands.next(body.last) + + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) + + val (before_edit, spans1) = + if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) + (prefix, spans0.tail) + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) + + val (after_edit, spans2) = + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) + (suffix, spans1.take(spans1.length - 1)) + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) + + val inserted = spans2.map(span => new Command(session.create_id(), span)) + val new_commands = + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) + parse_spans(new_commands) + + case None => commands + } + } + + + /* phase 3: resulting document edits */ + + val result = Library.timeit("text_edits") { + val commands0 = old_doc.commands + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) } + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) } + + val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList + val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList + + val doc_edits = + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) + + val former_states = old_doc.assignment.join -- removed_commands + + phase0 = edits + phase1 = commands1 + phase2 = commands2 + phase3 = doc_edits + + (doc_edits, new Document(new_id, commands2, former_states)) + } + result + } +} + + +class Document( + val id: Isar_Document.Document_ID, + val commands: Linear_Set[Command], + former_states: Map[Command, Command]) +{ + /* command ranges */ + + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) + + def command_start(cmd: Command): Option[Int] = + command_starts.find(_._1 == cmd).map(_._2) + + def command_range(i: Int): Iterator[(Command, Int)] = + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } + + def command_range(i: Int, j: Int): Iterator[(Command, Int)] = + command_range(i) takeWhile { case (_, start) => start < j } + + def command_at(i: Int): Option[(Command, Int)] = + { + val range = command_range(i) + if (range.hasNext) Some(range.next) else None + } + + + /* command state assignment */ + + val assignment = Future.promise[Map[Command, Command]] + def await_assignment { assignment.join } + + @volatile private var tmp_states = former_states + private val time0 = System.currentTimeMillis + + def assign_states(new_states: List[(Command, Command)]) + { + assignment.fulfill(tmp_states ++ new_states) + tmp_states = Map() + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") + } + + def current_state(cmd: Command): Option[State] = + { + require(assignment.is_finished) + (assignment.join).get(cmd).map(_.current_state) + } +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/event_bus.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/event_bus.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,35 @@ +/* Title: Pure/PIDE/event_bus.scala + Author: Makarius + +Generic event bus with multiple receiving actors. +*/ + +package isabelle + +import scala.actors.Actor, Actor._ +import scala.collection.mutable.ListBuffer + + +class Event_Bus[Event] +{ + /* receivers */ + + private val receivers = new ListBuffer[Actor] + + def += (r: Actor) { synchronized { receivers += r } } + def + (r: Actor): Event_Bus[Event] = { this += r; this } + + def += (f: Event => Unit) { + this += actor { loop { react { case x: Event => f(x) } } } + } + + def + (f: Event => Unit): Event_Bus[Event] = { this += f; this } + + def -= (r: Actor) { synchronized { receivers -= r } } + def - (r: Actor) = { this -= r; this } + + + /* event invocation */ + + def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/markup_node.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/markup_node.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,110 @@ +/* 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 + + + +case 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 +} + + +case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) +{ + private def add(branch: Markup_Tree) = // FIXME avoid sort + copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start)) + + private def remove(bs: List[Markup_Tree]) = + copy(branches = branches.filterNot(bs.contains(_))) + + 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 copy(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 + } + } +} + + +case 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.copy(branches = branches)) + else branches + } + new Markup_Text(markup.flatMap(filt(_)), content) + } + + def flatten: List[Markup_Node] = markup.flatten(_.flatten) + + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = + { + def swing(tree: Markup_Tree): DefaultMutableTreeNode = + { + val node = swing_node(tree.node) + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) + node + } + swing(root) + } +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/state.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/state.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,119 @@ +/* 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) => + atts match { + case Position.Range(begin, end) => + if (kind == Markup.ML_TYPING) { + val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!? + state.add_markup( + command.markup_node(begin - 1, end - 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 - 1, end - 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 - 1, end - 1, Command.HighlightInfo(kind))) + } + case _ => state + } + case _ => + System.err.println("ignored status report: " + elem) + state + }) + case _ => add_result(message) + } + if (!(this eq changed)) session.command_change.event(command) + changed + } +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/PIDE/text_edit.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/text_edit.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,51 @@ +/* Title: Pure/PIDE/text_edit.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Basic edits on plain text. +*/ + +package isabelle + + +class Text_Edit(val is_insert: Boolean, val start: Int, val text: String) +{ + override def toString = + (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" + + + /* transform offsets */ + + private def transform(do_insert: Boolean, offset: Int): Int = + if (offset < start) offset + else if (is_insert == do_insert) offset + text.length + else (offset - text.length) max start + + def after(offset: Int): Int = transform(true, offset) + def before(offset: Int): Int = transform(false, offset) + + + /* edit strings */ + + private def insert(index: Int, string: String): String = + string.substring(0, index) + text + string.substring(index) + + private def remove(index: Int, count: Int, string: String): String = + string.substring(0, index) + string.substring(index + count) + + def can_edit(string: String, shift: Int): Boolean = + shift <= start && start < shift + string.length + + def edit(string: String, shift: Int): (Option[Text_Edit], String) = + if (!can_edit(string, shift)) (Some(this), string) + else if (is_insert) (None, insert(start - shift, string)) + else { + val index = start - shift + val count = text.length min (string.length - index) + val rest = + if (count == text.length) None + else Some(new Text_Edit(false, start, text.substring(count))) + (rest, remove(index, count, string)) + } +} + diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri May 07 14:47:09 2010 +0200 @@ -115,8 +115,6 @@ [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}] else if name = Markup.breakN then [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}] - else if name = Markup.fbreakN then - [Pgml.Break {mandatory = SOME true, indent = NONE}] else content end | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/System/download.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/download.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,53 @@ +/* Title: Pure/System/download.scala + Author: Makarius + +Download URLs -- with progress monitor. +*/ + +package isabelle + + +import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, + File, InterruptedIOException} +import java.net.{URL, URLConnection} +import java.awt.{Component, HeadlessException} +import javax.swing.ProgressMonitorInputStream + + +object Download +{ + def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) = + { + val connection = url.openConnection + + val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream) + val monitor = stream.getProgressMonitor + monitor.setNote(connection.getURL.toString) + + val length = connection.getContentLength + if (length != -1) monitor.setMaximum(length) + + (connection, new BufferedInputStream(stream)) + } + + def file(parent: Component, url: URL, file: File) + { + val (connection, instream) = stream(parent, url) + val mod_time = connection.getLastModified + + def read() = + try { instream.read } + catch { case _ : InterruptedIOException => error("Download canceled!") } + try { + val outstream = new BufferedOutputStream(new FileOutputStream(file)) + try { + var c: Int = 0 + while ({ c = read(); c != -1}) outstream.write(c) + } + finally { outstream.close } + if (mod_time > 0) file.setLastModified(mod_time) + } + finally { instream.close } + } +} + diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/System/gui_setup.scala --- a/src/Pure/System/gui_setup.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/System/gui_setup.scala Fri May 07 14:47:09 2010 +0200 @@ -12,15 +12,13 @@ import scala.swing.event._ -object GUI_Setup extends GUIApplication +object GUI_Setup extends SwingApplication { - def main(args: Array[String]) = + def startup(args: Array[String]) = { - Swing_Thread.later { - UIManager.setLookAndFeel(Platform.look_and_feel) - top.pack() - top.visible = true - } + UIManager.setLookAndFeel(Platform.look_and_feel) + top.pack() + top.visible = true } def top = new MainFrame { diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/System/session.scala Fri May 07 14:47:09 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 @@ -123,12 +123,12 @@ result.body match { // document state assignment - case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined => + case List(Isar_Document.Assign(edits)) if target_id.isDefined => documents.get(target_id.get) match { case Some(doc) => val states = for { - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits + Isar_Document.Edit(cmd_id, state_id) <- edits cmd <- lookup_command(cmd_id) } yield { val st = cmd.assign_state(state_id) @@ -139,11 +139,9 @@ case None => bad_result(result) } - // command and keyword declarations - case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => - syntax += (name, kind) - case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => - syntax += name + // keyword declarations + case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind) + case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name case _ => if (!result.is_ready) bad_result(result) } diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/System/swing_thread.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/swing_thread.scala Fri May 07 14:47:09 2010 +0200 @@ -0,0 +1,63 @@ +/* Title: Pure/System/swing_thread.scala + Author: Makarius + Author: Fabian Immler, TU Munich + +Evaluation within the AWT/Swing thread. +*/ + +package isabelle + +import javax.swing.{SwingUtilities, Timer} +import java.awt.event.{ActionListener, ActionEvent} + + +object Swing_Thread +{ + /* checks */ + + def assert() = Predef.assert(SwingUtilities.isEventDispatchThread()) + def require() = Predef.require(SwingUtilities.isEventDispatchThread()) + + + /* main dispatch queue */ + + def now[A](body: => A): A = + { + var result: Option[A] = None + if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } + else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) + result.get + } + + def future[A](body: => A): Future[A] = + { + if (SwingUtilities.isEventDispatchThread()) Future.value(body) + else Future.fork { now(body) } + } + + def later(body: => Unit) + { + if (SwingUtilities.isEventDispatchThread()) body + else SwingUtilities.invokeLater(new Runnable { def run = body }) + } + + + /* delayed actions */ + + private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit = + { + val listener = + new ActionListener { override def actionPerformed(e: ActionEvent) { action } } + val timer = new Timer(time_span, listener) + timer.setRepeats(false) + + def invoke() { if (first) timer.start() else timer.restart() } + invoke _ + } + + // delayed action after first invocation + def delay_first = delayed_action(true) _ + + // delayed action after last invocation + def delay_last = delayed_action(false) _ +} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Thy/change.scala --- a/src/Pure/Thy/change.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -/* - * Changes of plain text - * - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle - - -class Change( - val id: Isar_Document.Document_ID, - val parent: Option[Change], - val edits: List[Text_Edit], - val result: Future[(List[Document.Edit], Document)]) -{ - def ancestors: Iterator[Change] = new Iterator[Change] - { - private var state: Option[Change] = Some(Change.this) - def hasNext = state.isDefined - def next = - state match { - case Some(change) => state = change.parent; change - case None => throw new NoSuchElementException("next on empty iterator") - } - } - - def join_document: Document = result.join._2 - def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished - - def edit(session: Session, edits: List[Text_Edit]): Change = - { - val new_id = session.create_id() - val result: Future[(List[Document.Edit], Document)] = - Future.fork { - val old_doc = join_document - old_doc.await_assignment - Document.text_edits(session, old_doc, new_id, edits) - } - new Change(new_id, Some(this), edits, result) - } -} \ No newline at end of file diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Thy/command.scala --- a/src/Pure/Thy/command.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -/* - * Prover commands with semantic state - * - * @author Johannes Hölzl, TU Munich - * @author Fabian Immler, TU Munich - */ - -package isabelle - - -import scala.actors.Actor, Actor._ -import scala.collection.mutable - - -object Command -{ - object Status extends Enumeration - { - val UNPROCESSED = Value("UNPROCESSED") - val FINISHED = Value("FINISHED") - val FAILED = Value("FAILED") - } - - case class HighlightInfo(highlight: String) { override def toString = highlight } - case class TypeInfo(ty: String) - case class RefInfo(file: Option[String], line: Option[Int], - command_id: Option[String], offset: Option[Int]) -} - - -class Command( - val id: Isar_Document.Command_ID, - val span: Thy_Syntax.Span) - extends Session.Entity -{ - /* classification */ - - def is_command: Boolean = !span.isEmpty && span.head.is_command - def is_ignored: Boolean = span.forall(_.is_ignored) - def is_malformed: Boolean = !is_command && !is_ignored - - def name: String = if (is_command) span.head.content else "" - override def toString = if (is_command) name else if (is_ignored) "" else "" - - - /* source text */ - - val source: String = span.map(_.source).mkString - def source(i: Int, j: Int): String = source.substring(i, j) - def length: Int = source.length - - lazy val symbol_index = new Symbol.Index(source) - - - /* accumulated messages */ - - @volatile protected var state = new State(this) - def current_state: State = state - - private case class Consume(session: Session, message: XML.Tree) - private case object Assign - - private val accumulator = actor { - var assigned = false - loop { - react { - case Consume(session: Session, message: XML.Tree) if !assigned => - state = state.+(session, message) - - case Assign => - assigned = true // single assignment - reply(()) - - case bad => System.err.println("command accumulator: ignoring bad message " + bad) - } - } - } - - def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } - - def assign_state(state_id: Isar_Document.State_ID): Command = - { - val cmd = new Command(state_id, span) - accumulator !? Assign - cmd.state = current_state - cmd - } - - - /* markup */ - - lazy val empty_markup = new Markup_Text(Nil, source) - - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = - { - val start = symbol_index.decode(begin) - val stop = symbol_index.decode(end) - new Markup_Tree(new Markup_Node(start, stop, info), Nil) - } -} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Thy/document.scala --- a/src/Pure/Thy/document.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,197 +0,0 @@ -/* - * Document as editable list of commands - * - * @author Makarius - */ - -package isabelle - - -object Document -{ - /* command start positions */ - - def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] = - { - var offset = 0 - for (cmd <- commands.iterator) yield { - val start = offset - offset += cmd.length - (cmd, start) - } - } - - - /* empty document */ - - def empty(id: Isar_Document.Document_ID): Document = - { - val doc = new Document(id, Linear_Set(), Map()) - doc.assign_states(Nil) - doc - } - - - // FIXME - var phase0: List[Text_Edit] = null - var phase1: Linear_Set[Command] = null - var phase2: Linear_Set[Command] = null - var phase3: List[Edit] = null - - - - /** document edits **/ - - type Edit = (Option[Command], Option[Command]) - - def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, - edits: List[Text_Edit]): (List[Edit], Document) = - { - require(old_doc.assignment.is_finished) - - - /* unparsed dummy commands */ - - def unparsed(source: String) = - new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) - - def is_unparsed(command: Command) = command.id == null - - assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove - - - /* phase 1: edit individual command source */ - - def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = - { - eds match { - case e :: es => - command_starts(commands).find { // FIXME relative search! - case (cmd, cmd_start) => - e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length - } match { - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => - val (rest, text) = e.edit(cmd.source, cmd_start) - val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd - edit_text(rest.toList ::: es, new_commands) - - case Some((cmd, cmd_start)) => - edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) - - case None => - require(e.is_insert && e.start == 0) - edit_text(es, commands.insert_after(None, unparsed(e.text))) - } - case Nil => commands - } - } - - - /* phase 2: recover command spans */ - - def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = - { - // FIXME relative search! - commands.iterator.find(is_unparsed) match { - case Some(first_unparsed) => - val prefix = commands.prev(first_unparsed) - val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList - val suffix = commands.next(body.last) - - val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) - val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) - - val (before_edit, spans1) = - if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) - (prefix, spans0.tail) - else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) - - val (after_edit, spans2) = - if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) - (suffix, spans1.take(spans1.length - 1)) - else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) - - val inserted = spans2.map(span => new Command(session.create_id(), span)) - val new_commands = - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) - parse_spans(new_commands) - - case None => commands - } - } - - - /* phase 3: resulting document edits */ - - val result = Library.timeit("text_edits") { - val commands0 = old_doc.commands - val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) } - val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) } - - val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList - val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList - - val doc_edits = - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) - - val former_states = old_doc.assignment.join -- removed_commands - - phase0 = edits - phase1 = commands1 - phase2 = commands2 - phase3 = doc_edits - - (doc_edits, new Document(new_id, commands2, former_states)) - } - result - } -} - - -class Document( - val id: Isar_Document.Document_ID, - val commands: Linear_Set[Command], - former_states: Map[Command, Command]) -{ - /* command ranges */ - - def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) - - def command_start(cmd: Command): Option[Int] = - command_starts.find(_._1 == cmd).map(_._2) - - def command_range(i: Int): Iterator[(Command, Int)] = - command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } - - def command_range(i: Int, j: Int): Iterator[(Command, Int)] = - command_range(i) takeWhile { case (_, start) => start < j } - - def command_at(i: Int): Option[(Command, Int)] = - { - val range = command_range(i) - if (range.hasNext) Some(range.next) else None - } - - - /* command state assignment */ - - val assignment = Future.promise[Map[Command, Command]] - def await_assignment { assignment.join } - - @volatile private var tmp_states = former_states - private val time0 = System.currentTimeMillis - - def assign_states(new_states: List[(Command, Command)]) - { - assignment.fulfill(tmp_states ++ new_states) - tmp_states = Map() - System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") - } - - def current_state(cmd: Command): Option[State] = - { - require(assignment.is_finished) - (assignment.join).get(cmd).map(_.current_state) - } -} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Thy/markup_node.scala --- a/src/Pure/Thy/markup_node.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,111 +0,0 @@ -/* - * Document markup nodes, with connection to Swing tree model - * - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle - - -import javax.swing.tree.DefaultMutableTreeNode - - - -class Markup_Node(val start: Int, val stop: Int, val info: Any) -{ - def fits_into(that: Markup_Node): Boolean = - that.start <= this.start && this.stop <= that.stop -} - - -class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) -{ - def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs) - - private def add(branch: Markup_Tree) = // FIXME avoid sort - set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start)) - - private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs) - - def + (new_tree: Markup_Tree): Markup_Tree = - { - val new_node = new_tree.node - if (new_node fits_into node) { - var inserted = false - val new_branches = - branches.map(branch => - if ((new_node fits_into branch.node) && !inserted) { - inserted = true - branch + new_tree - } - else branch) - if (!inserted) { - // new_tree did not fit into children of this - // -> insert between this and its branches - val fitting = branches filter(_.node fits_into new_node) - (this remove fitting) add ((new_tree /: fitting)(_ + _)) - } - else set_branches(new_branches) - } - else { - System.err.println("ignored nonfitting markup: " + new_node) - this - } - } - - def flatten: List[Markup_Node] = - { - var next_x = node.start - if (branches.isEmpty) List(this.node) - else { - val filled_gaps = - for { - child <- branches - markups = - if (next_x < child.node.start) - new Markup_Node(next_x, child.node.start, node.info) :: child.flatten - else child.flatten - update = (next_x = child.node.stop) - markup <- markups - } yield markup - if (next_x < node.stop) - filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info)) - else filled_gaps - } - } -} - - -class Markup_Text(val markup: List[Markup_Tree], val content: String) -{ - private lazy val root = - new Markup_Tree(new Markup_Node(0, content.length, None), markup) - - def + (new_tree: Markup_Tree): Markup_Text = - new Markup_Text((root + new_tree).branches, content) - - def filter(pred: Markup_Node => Boolean): Markup_Text = - { - def filt(tree: Markup_Tree): List[Markup_Tree] = - { - val branches = tree.branches.flatMap(filt(_)) - if (pred(tree.node)) List(tree.set_branches(branches)) - else branches - } - new Markup_Text(markup.flatMap(filt(_)), content) - } - - def flatten: List[Markup_Node] = markup.flatten(_.flatten) - - def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = - { - def swing(tree: Markup_Tree): DefaultMutableTreeNode = - { - val node = swing_node(tree.node) - tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) - node - } - swing(root) - } -} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Thy/state.scala --- a/src/Pure/Thy/state.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -/* - * Accumulating results from prover - * - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle - - -class State( - val command: Command, - val status: Command.Status.Value, - val rev_results: List[XML.Tree], - val markup_root: Markup_Text) -{ - def this(command: Command) = - this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup) - - - /* content */ - - private def set_status(st: Command.Status.Value): State = - new State(command, st, rev_results, markup_root) - - private def add_result(res: XML.Tree): State = - new State(command, status, res :: rev_results, markup_root) - - private def add_markup(node: Markup_Tree): State = - new State(command, status, rev_results, markup_root + node) - - lazy val results = rev_results.reverse - - - /* markup */ - - lazy val highlight: Markup_Text = - { - markup_root.filter(_.info match { - case Command.HighlightInfo(_) => true - case _ => false - }) - } - - private lazy val types: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.TypeInfo(_) => true - case _ => false }).flatten - - def type_at(pos: Int): Option[String] = - { - types.find(t => t.start <= pos && pos < t.stop) match { - case Some(t) => - t.info match { - case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty) - case _ => None - } - case None => None - } - } - - private lazy val refs: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.RefInfo(_, _, _, _) => true - case _ => false }).flatten - - def ref_at(pos: Int): Option[Markup_Node] = - refs.find(t => t.start <= pos && pos < t.stop) - - - /* message dispatch */ - - def + (session: Session, message: XML.Tree): State = - { - val changed: State = - message match { - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) - case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) - case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) - case XML.Elem(kind, atts, body) => - val (begin, end) = Position.get_offsets(atts) - if (begin.isEmpty || end.isEmpty) state - else if (kind == Markup.ML_TYPING) { - val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!? - state.add_markup( - command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info))) - } - else if (kind == Markup.ML_REF) { - body match { - case List(XML.Elem(Markup.ML_DEF, atts, _)) => - state.add_markup(command.markup_node( - begin.get - 1, end.get - 1, - Command.RefInfo( - Position.get_file(atts), - Position.get_line(atts), - Position.get_id(atts), - Position.get_offset(atts)))) - case _ => state - } - } - else { - state.add_markup( - command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind))) - } - case _ => - System.err.println("ignored status report: " + elem) - state - }) - case _ => add_result(message) - } - if (!(this eq changed)) session.command_change.event(command) - changed - } -} diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/Thy/text_edit.scala --- a/src/Pure/Thy/text_edit.scala Fri May 07 09:59:59 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -/* Title: Pure/Thy/text_edit.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -Basic edits on plain text. -*/ - -package isabelle - - -class Text_Edit(val is_insert: Boolean, val start: Int, val text: String) -{ - override def toString = - (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" - - - /* transform offsets */ - - private def transform(do_insert: Boolean, offset: Int): Int = - if (offset < start) offset - else if (is_insert == do_insert) offset + text.length - else (offset - text.length) max start - - def after(offset: Int): Int = transform(true, offset) - def before(offset: Int): Int = transform(false, offset) - - - /* edit strings */ - - private def insert(index: Int, string: String): String = - string.substring(0, index) + text + string.substring(index) - - private def remove(index: Int, count: Int, string: String): String = - string.substring(0, index) + string.substring(index + count) - - def can_edit(string: String, shift: Int): Boolean = - shift <= start && start < shift + string.length - - def edit(string: String, shift: Int): (Option[Text_Edit], String) = - if (!can_edit(string, shift)) (Some(this), string) - else if (is_insert) (None, insert(start - shift, string)) - else { - val index = start - shift - val count = text.length min (string.length - index) - val rest = - if (count == text.length) None - else Some(new Text_Edit(false, start, text.substring(count))) - (rest, remove(index, count, string)) - } -} - diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/build-jars --- a/src/Pure/build-jars Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/build-jars Fri May 07 14:47:09 2010 +0200 @@ -23,14 +23,12 @@ 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/pretty.scala General/scan.scala - General/swing_thread.scala General/symbol.scala General/xml.scala General/yxml.scala @@ -39,7 +37,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 +54,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 diff -r 47ba1770da8e -r 51e3b38a5e41 src/Pure/library.scala --- a/src/Pure/library.scala Fri May 07 09:59:59 2010 +0200 +++ b/src/Pure/library.scala Fri May 07 14:47:09 2010 +0200 @@ -13,6 +13,15 @@ object Library { + /* separate */ + + def separate[A](s: A, list: List[A]): List[A] = + list match { + case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs) + case _ => list + } + + /* reverse CharSequence */ class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence @@ -38,6 +47,30 @@ } + /* iterate over chunks (cf. space_explode/split_lines in ML) */ + + def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence] + { + private val end = source.length + private def next_chunk(i: Int): Option[(CharSequence, Int)] = + { + if (i < end) { + var j = i; do j += 1 while (j < end && source.charAt(j) != sep) + Some((source.subSequence(i + 1, j), j)) + } + else None + } + private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) + + def hasNext(): Boolean = state.isDefined + def next(): CharSequence = + state match { + case Some((s, i)) => { state = next_chunk(i); s } + case None => throw new NoSuchElementException("next on empty iterator") + } + } + + /* simple dialogs */ private def simple_dialog(kind: Int, default_title: String)