--- 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 }
- }
-}
-
--- 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) } }
-}
--- 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"
--- 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) }
}
--- 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;
--- /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
+ }
+}
--- 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 =
--- 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) _
-}
--- 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 */
--- 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)
}
}
--- 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
+ }
+ }
}
--- 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";
--- 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
+ }
+ }
}
--- /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
--- /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) "<ignored>" else "<malformed>"
+
+
+ /* source text */
+
+ val source: String = span.map(_.source).mkString
+ def source(i: Int, j: Int): String = source.substring(i, j)
+ def length: Int = source.length
+
+ lazy val symbol_index = new Symbol.Index(source)
+
+
+ /* accumulated messages */
+
+ @volatile protected var state = new State(this)
+ def current_state: State = state
+
+ private case class Consume(session: Session, message: XML.Tree)
+ private case object Assign
+
+ private val accumulator = actor {
+ var assigned = false
+ loop {
+ react {
+ case Consume(session: Session, message: XML.Tree) if !assigned =>
+ state = state.+(session, message)
+
+ case Assign =>
+ assigned = true // single assignment
+ reply(())
+
+ case bad => System.err.println("command accumulator: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+
+ def assign_state(state_id: Isar_Document.State_ID): Command =
+ {
+ val cmd = new Command(state_id, span)
+ accumulator !? Assign
+ cmd.state = current_state
+ cmd
+ }
+
+
+ /* markup */
+
+ lazy val empty_markup = new Markup_Text(Nil, source)
+
+ def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
+ {
+ val start = symbol_index.decode(begin)
+ val stop = symbol_index.decode(end)
+ new Markup_Tree(new Markup_Node(start, stop, info), Nil)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document.scala 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)
+ }
+}
--- /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) } }
+}
--- /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)
+ }
+}
--- /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
+ }
+}
--- /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))
+ }
+}
+
--- 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);
--- /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 }
+ }
+}
+
--- 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 {
--- 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)
}
--- /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) _
+}
--- 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
--- 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) "<ignored>" else "<malformed>"
-
-
- /* source text */
-
- val source: String = span.map(_.source).mkString
- def source(i: Int, j: Int): String = source.substring(i, j)
- def length: Int = source.length
-
- lazy val symbol_index = new Symbol.Index(source)
-
-
- /* accumulated messages */
-
- @volatile protected var state = new State(this)
- def current_state: State = state
-
- private case class Consume(session: Session, message: XML.Tree)
- private case object Assign
-
- private val accumulator = actor {
- var assigned = false
- loop {
- react {
- case Consume(session: Session, message: XML.Tree) if !assigned =>
- state = state.+(session, message)
-
- case Assign =>
- assigned = true // single assignment
- reply(())
-
- case bad => System.err.println("command accumulator: ignoring bad message " + bad)
- }
- }
- }
-
- def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
-
- def assign_state(state_id: Isar_Document.State_ID): Command =
- {
- val cmd = new Command(state_id, span)
- accumulator !? Assign
- cmd.state = current_state
- cmd
- }
-
-
- /* markup */
-
- lazy val empty_markup = new Markup_Text(Nil, source)
-
- def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
- {
- val start = symbol_index.decode(begin)
- val stop = symbol_index.decode(end)
- new Markup_Tree(new Markup_Node(start, stop, info), Nil)
- }
-}
--- a/src/Pure/Thy/document.scala 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)
- }
-}
--- 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)
- }
-}
--- 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
- }
-}
--- 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))
- }
-}
-
--- 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
--- 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)