1.1 --- a/src/Pure/General/download.scala Fri May 07 09:59:59 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,53 +0,0 @@
1.4 -/* Title: Pure/General/download.scala
1.5 - Author: Makarius
1.6 -
1.7 -Download URLs -- with progress monitor.
1.8 -*/
1.9 -
1.10 -package isabelle
1.11 -
1.12 -
1.13 -import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
1.14 - File, InterruptedIOException}
1.15 -import java.net.{URL, URLConnection}
1.16 -import java.awt.{Component, HeadlessException}
1.17 -import javax.swing.ProgressMonitorInputStream
1.18 -
1.19 -
1.20 -object Download
1.21 -{
1.22 - def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
1.23 - {
1.24 - val connection = url.openConnection
1.25 -
1.26 - val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
1.27 - val monitor = stream.getProgressMonitor
1.28 - monitor.setNote(connection.getURL.toString)
1.29 -
1.30 - val length = connection.getContentLength
1.31 - if (length != -1) monitor.setMaximum(length)
1.32 -
1.33 - (connection, new BufferedInputStream(stream))
1.34 - }
1.35 -
1.36 - def file(parent: Component, url: URL, file: File)
1.37 - {
1.38 - val (connection, instream) = stream(parent, url)
1.39 - val mod_time = connection.getLastModified
1.40 -
1.41 - def read() =
1.42 - try { instream.read }
1.43 - catch { case _ : InterruptedIOException => error("Download canceled!") }
1.44 - try {
1.45 - val outstream = new BufferedOutputStream(new FileOutputStream(file))
1.46 - try {
1.47 - var c: Int = 0
1.48 - while ({ c = read(); c != -1}) outstream.write(c)
1.49 - }
1.50 - finally { outstream.close }
1.51 - if (mod_time > 0) file.setLastModified(mod_time)
1.52 - }
1.53 - finally { instream.close }
1.54 - }
1.55 -}
1.56 -
2.1 --- a/src/Pure/General/event_bus.scala Fri May 07 09:59:59 2010 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,35 +0,0 @@
2.4 -/* Title: Pure/General/event_bus.scala
2.5 - Author: Makarius
2.6 -
2.7 -Generic event bus with multiple receiving actors.
2.8 -*/
2.9 -
2.10 -package isabelle
2.11 -
2.12 -import scala.actors.Actor, Actor._
2.13 -import scala.collection.mutable.ListBuffer
2.14 -
2.15 -
2.16 -class Event_Bus[Event]
2.17 -{
2.18 - /* receivers */
2.19 -
2.20 - private val receivers = new ListBuffer[Actor]
2.21 -
2.22 - def += (r: Actor) { synchronized { receivers += r } }
2.23 - def + (r: Actor): Event_Bus[Event] = { this += r; this }
2.24 -
2.25 - def += (f: Event => Unit) {
2.26 - this += actor { loop { react { case x: Event => f(x) } } }
2.27 - }
2.28 -
2.29 - def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
2.30 -
2.31 - def -= (r: Actor) { synchronized { receivers -= r } }
2.32 - def - (r: Actor) = { this -= r; this }
2.33 -
2.34 -
2.35 - /* event invocation */
2.36 -
2.37 - def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
2.38 -}
3.1 --- a/src/Pure/General/markup.scala Fri May 07 09:59:59 2010 +0200
3.2 +++ b/src/Pure/General/markup.scala Fri May 07 14:47:09 2010 +0200
3.3 @@ -9,6 +9,24 @@
3.4
3.5 object Markup
3.6 {
3.7 + /* property values */
3.8 +
3.9 + def get_string(name: String, props: List[(String, String)]): Option[String] =
3.10 + props.find(p => p._1 == name).map(_._2)
3.11 +
3.12 + def parse_int(s: String): Option[Int] =
3.13 + try { Some(Integer.parseInt(s)) }
3.14 + catch { case _: NumberFormatException => None }
3.15 +
3.16 + def get_int(name: String, props: List[(String, String)]): Option[Int] =
3.17 + {
3.18 + get_string(name, props) match {
3.19 + case None => None
3.20 + case Some(value) => parse_int(value)
3.21 + }
3.22 + }
3.23 +
3.24 +
3.25 /* name */
3.26
3.27 val NAME = "name"
3.28 @@ -40,6 +58,14 @@
3.29 val LOCATION = "location"
3.30
3.31
3.32 + /* pretty printing */
3.33 +
3.34 + val INDENT = "indent"
3.35 + val BLOCK = "block"
3.36 + val WIDTH = "width"
3.37 + val BREAK = "break"
3.38 +
3.39 +
3.40 /* hidden text */
3.41
3.42 val HIDDEN = "hidden"
4.1 --- a/src/Pure/General/position.scala Fri May 07 09:59:59 2010 +0200
4.2 +++ b/src/Pure/General/position.scala Fri May 07 14:47:09 2010 +0200
4.3 @@ -11,32 +11,22 @@
4.4 {
4.5 type T = List[(String, String)]
4.6
4.7 - private def get_string(name: String, pos: T): Option[String] =
4.8 - pos.find(p => p._1 == name).map(_._2)
4.9 + def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
4.10 + def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
4.11 + def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
4.12 + def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
4.13 + def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
4.14 + def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
4.15 + def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
4.16 + def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
4.17
4.18 - private def get_int(name: String, pos: T): Option[Int] =
4.19 - {
4.20 - get_string(name, pos) match {
4.21 - case None => None
4.22 - case Some(value) =>
4.23 - try { Some(Integer.parseInt(value)) }
4.24 - catch { case _: NumberFormatException => None }
4.25 + def get_range(pos: T): Option[(Int, Int)] =
4.26 + (get_offset(pos), get_end_offset(pos)) match {
4.27 + case (Some(begin), Some(end)) => Some(begin, end)
4.28 + case (Some(begin), None) => Some(begin, begin + 1)
4.29 + case (None, _) => None
4.30 }
4.31 - }
4.32
4.33 - def get_line(pos: T): Option[Int] = get_int(Markup.LINE, pos)
4.34 - def get_column(pos: T): Option[Int] = get_int(Markup.COLUMN, pos)
4.35 - def get_offset(pos: T): Option[Int] = get_int(Markup.OFFSET, pos)
4.36 - def get_end_line(pos: T): Option[Int] = get_int(Markup.END_LINE, pos)
4.37 - def get_end_column(pos: T): Option[Int] = get_int(Markup.END_COLUMN, pos)
4.38 - def get_end_offset(pos: T): Option[Int] = get_int(Markup.END_OFFSET, pos)
4.39 - def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos)
4.40 - def get_id(pos: T): Option[String] = get_string(Markup.ID, pos)
4.41 -
4.42 - def get_offsets(pos: T): (Option[Int], Option[Int]) =
4.43 - {
4.44 - val begin = get_offset(pos)
4.45 - val end = get_end_offset(pos)
4.46 - (begin, if (end.isDefined) end else begin.map(_ + 1))
4.47 - }
4.48 + object Id { def unapply(pos: T): Option[String] = get_id(pos) }
4.49 + object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
4.50 }
5.1 --- a/src/Pure/General/pretty.ML Fri May 07 09:59:59 2010 +0200
5.2 +++ b/src/Pure/General/pretty.ML Fri May 07 14:47:09 2010 +0200
5.3 @@ -119,7 +119,7 @@
5.4 val str = String o Output.output_width;
5.5
5.6 fun brk wd = Break (false, wd);
5.7 -val fbrk = Break (true, 2);
5.8 +val fbrk = Break (true, 1);
5.9
5.10 fun breaks prts = Library.separate (brk 1) prts;
5.11 fun fbreaks prts = Library.separate fbrk prts;
5.12 @@ -249,14 +249,14 @@
5.13
5.14 (*Add the lengths of the expressions until the next Break; if no Break then
5.15 include "after", to account for text following this block.*)
5.16 -fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
5.17 +fun breakdist (Break _ :: _, _) = 0
5.18 + | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
5.19 | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
5.20 - | breakdist (Break _ :: _, _) = 0
5.21 | breakdist ([], after) = after;
5.22
5.23 (*Search for the next break (at this or higher levels) and force it to occur.*)
5.24 fun forcenext [] = []
5.25 - | forcenext (Break _ :: es) = Break (true, 0) :: es
5.26 + | forcenext (Break _ :: es) = fbrk :: es
5.27 | forcenext (e :: es) = e :: forcenext es;
5.28
5.29 (*es is list of expressions to print;
5.30 @@ -280,7 +280,6 @@
5.31 (*if this block was broken then force the next break*)
5.32 val es' = if nl < #nl btext then forcenext es else es;
5.33 in format (es', block, after) btext end
5.34 - | String str => format (es, block, after) (string str text)
5.35 | Break (force, wd) =>
5.36 let val {margin, breakgain, ...} = ! margin_info in
5.37 (*no break if text to next break fits on this line
5.38 @@ -290,7 +289,8 @@
5.39 pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
5.40 then text |> blanks wd (*just insert wd blanks*)
5.41 else text |> newline |> indentation block)
5.42 - end);
5.43 + end
5.44 + | String str => format (es, block, after) (string str text));
5.45
5.46 in
5.47
5.48 @@ -309,7 +309,7 @@
5.49 Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
5.50 | out (String (s, _)) = Buffer.add s
5.51 | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
5.52 - | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
5.53 + | out (Break (true, _)) = Buffer.add (Output.output "\n");
5.54 in out prt Buffer.empty end;
5.55
5.56 (*unformatted output*)
5.57 @@ -317,8 +317,7 @@
5.58 let
5.59 fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
5.60 | fmt (String (s, _)) = Buffer.add s
5.61 - | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
5.62 - | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
5.63 + | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
5.64 in fmt (prune prt) Buffer.empty end;
5.65
5.66
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/General/pretty.scala Fri May 07 14:47:09 2010 +0200
6.3 @@ -0,0 +1,111 @@
6.4 +/* Title: Pure/General/pretty.scala
6.5 + Author: Makarius
6.6 +
6.7 +Generic pretty printing module.
6.8 +*/
6.9 +
6.10 +package isabelle
6.11 +
6.12 +
6.13 +object Pretty
6.14 +{
6.15 + /* markup trees with physical blocks and breaks */
6.16 +
6.17 + object Block
6.18 + {
6.19 + def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
6.20 + XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
6.21 +
6.22 + def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
6.23 + tree match {
6.24 + case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
6.25 + Markup.parse_int(indent) match {
6.26 + case Some(i) => Some((i, body))
6.27 + case None => None
6.28 + }
6.29 + case _ => None
6.30 + }
6.31 + }
6.32 +
6.33 + object Break
6.34 + {
6.35 + def apply(width: Int): XML.Tree =
6.36 + XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), List(XML.Text(" " * width)))
6.37 +
6.38 + def unapply(tree: XML.Tree): Option[Int] =
6.39 + tree match {
6.40 + case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
6.41 + case _ => None
6.42 + }
6.43 + }
6.44 +
6.45 + val FBreak = XML.Text("\n")
6.46 +
6.47 +
6.48 + /* formatted output */
6.49 +
6.50 + private case class Text(tx: List[String] = Nil, val pos: Int = 0, val nl: Int = 0)
6.51 + {
6.52 + def newline: Text = copy(tx = "\n" :: tx, pos = 0, nl = nl + 1)
6.53 + def string(s: String): Text = copy(tx = s :: tx, pos = pos + s.length)
6.54 + def blanks(wd: Int): Text = string(" " * wd)
6.55 + def content: String = tx.reverse.mkString
6.56 + }
6.57 +
6.58 + private def breakdist(trees: List[XML.Tree], after: Int): Int =
6.59 + trees match {
6.60 + case Break(_) :: _ => 0
6.61 + case FBreak :: _ => 0
6.62 + case XML.Elem(_, _, body) :: ts =>
6.63 + (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after)
6.64 + case XML.Text(s) :: ts => s.length + breakdist(ts, after)
6.65 + case Nil => after
6.66 + }
6.67 +
6.68 + private def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
6.69 + trees match {
6.70 + case Nil => Nil
6.71 + case FBreak :: _ => trees
6.72 + case Break(_) :: ts => FBreak :: ts
6.73 + case t :: ts => t :: forcenext(ts)
6.74 + }
6.75 +
6.76 + private def standard(tree: XML.Tree): List[XML.Tree] =
6.77 + tree match {
6.78 + case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard)))
6.79 + case XML.Text(text) =>
6.80 + Library.separate(FBreak,
6.81 + Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
6.82 + }
6.83 +
6.84 + def string_of(input: List[XML.Tree], margin: Int = 76): String =
6.85 + {
6.86 + val breakgain = margin / 20
6.87 + val emergencypos = margin / 2
6.88 +
6.89 + def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text =
6.90 + trees match {
6.91 + case Nil => text
6.92 +
6.93 + case Block(indent, body) :: ts =>
6.94 + val pos1 = text.pos + indent
6.95 + val pos2 = pos1 % emergencypos
6.96 + val blockin1 =
6.97 + if (pos1 < emergencypos) pos1
6.98 + else pos2
6.99 + val btext = format(body, blockin1, breakdist(ts, after), text)
6.100 + val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
6.101 + format(ts1, blockin, after, btext)
6.102 +
6.103 + case Break(wd) :: ts =>
6.104 + if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
6.105 + format(ts, blockin, after, text.blanks(wd))
6.106 + else format(ts, blockin, after, text.newline.blanks(blockin))
6.107 + case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
6.108 +
6.109 + case XML.Elem(_, _, body) :: ts => format(body ::: ts, blockin, after, text)
6.110 + case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
6.111 + }
6.112 + format(input.flatMap(standard), 0, 0, Text()).content
6.113 + }
6.114 +}
7.1 --- a/src/Pure/General/scan.scala Fri May 07 09:59:59 2010 +0200
7.2 +++ b/src/Pure/General/scan.scala Fri May 07 14:47:09 2010 +0200
7.3 @@ -8,6 +8,7 @@
7.4
7.5
7.6 import scala.collection.generic.Addable
7.7 +import scala.collection.IndexedSeq
7.8 import scala.collection.immutable.PagedSeq
7.9 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
7.10 import scala.util.parsing.combinator.RegexParsers
7.11 @@ -306,7 +307,7 @@
7.12
7.13 /** read file without decoding -- enables efficient length operation **/
7.14
7.15 - private class Restricted_Seq(seq: RandomAccessSeq[Char], start: Int, end: Int)
7.16 + private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
7.17 extends CharSequence
7.18 {
7.19 def charAt(i: Int): Char =
8.1 --- a/src/Pure/General/swing_thread.scala Fri May 07 09:59:59 2010 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,63 +0,0 @@
8.4 -/* Title: Pure/General/swing_thread.scala
8.5 - Author: Makarius
8.6 - Author: Fabian Immler, TU Munich
8.7 -
8.8 -Evaluation within the AWT/Swing thread.
8.9 -*/
8.10 -
8.11 -package isabelle
8.12 -
8.13 -import javax.swing.{SwingUtilities, Timer}
8.14 -import java.awt.event.{ActionListener, ActionEvent}
8.15 -
8.16 -
8.17 -object Swing_Thread
8.18 -{
8.19 - /* checks */
8.20 -
8.21 - def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
8.22 - def require() = Predef.require(SwingUtilities.isEventDispatchThread())
8.23 -
8.24 -
8.25 - /* main dispatch queue */
8.26 -
8.27 - def now[A](body: => A): A =
8.28 - {
8.29 - var result: Option[A] = None
8.30 - if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
8.31 - else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
8.32 - result.get
8.33 - }
8.34 -
8.35 - def future[A](body: => A): Future[A] =
8.36 - {
8.37 - if (SwingUtilities.isEventDispatchThread()) Future.value(body)
8.38 - else Future.fork { now(body) }
8.39 - }
8.40 -
8.41 - def later(body: => Unit)
8.42 - {
8.43 - if (SwingUtilities.isEventDispatchThread()) body
8.44 - else SwingUtilities.invokeLater(new Runnable { def run = body })
8.45 - }
8.46 -
8.47 -
8.48 - /* delayed actions */
8.49 -
8.50 - private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
8.51 - {
8.52 - val listener =
8.53 - new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
8.54 - val timer = new Timer(time_span, listener)
8.55 - timer.setRepeats(false)
8.56 -
8.57 - def invoke() { if (first) timer.start() else timer.restart() }
8.58 - invoke _
8.59 - }
8.60 -
8.61 - // delayed action after first invocation
8.62 - def delay_first = delayed_action(true) _
8.63 -
8.64 - // delayed action after last invocation
8.65 - def delay_last = delayed_action(false) _
8.66 -}
9.1 --- a/src/Pure/General/xml.scala Fri May 07 09:59:59 2010 +0200
9.2 +++ b/src/Pure/General/xml.scala Fri May 07 14:47:09 2010 +0200
9.3 @@ -92,6 +92,12 @@
9.4 }
9.5 }
9.6
9.7 + def content_length(tree: XML.Tree): Int =
9.8 + tree match {
9.9 + case Elem(_, _, body) => (0 /: body)(_ + content_length(_))
9.10 + case Text(s) => s.length
9.11 + }
9.12 +
9.13
9.14 /* cache for partial sharing -- NOT THREAD SAFE */
9.15
10.1 --- a/src/Pure/General/yxml.scala Fri May 07 09:59:59 2010 +0200
10.2 +++ b/src/Pure/General/yxml.scala Fri May 07 14:47:09 2010 +0200
10.3 @@ -7,6 +7,9 @@
10.4 package isabelle
10.5
10.6
10.7 +import scala.collection.mutable.ListBuffer
10.8 +
10.9 +
10.10 object YXML
10.11 {
10.12 /* chunk markers */
10.13 @@ -17,29 +20,6 @@
10.14 private val Y_string = Y.toString
10.15
10.16
10.17 - /* iterate over chunks (resembles space_explode in ML) */
10.18 -
10.19 - private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence]
10.20 - {
10.21 - private val end = source.length
10.22 - private var state = if (end == 0) None else get_chunk(-1)
10.23 - private def get_chunk(i: Int) =
10.24 - {
10.25 - if (i < end) {
10.26 - var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
10.27 - Some((source.subSequence(i + 1, j), j))
10.28 - }
10.29 - else None
10.30 - }
10.31 -
10.32 - def hasNext() = state.isDefined
10.33 - def next() = state match {
10.34 - case Some((s, i)) => { state = get_chunk(i); s }
10.35 - case None => throw new NoSuchElementException("next on empty iterator")
10.36 - }
10.37 - }
10.38 -
10.39 -
10.40 /* decoding pseudo UTF-8 */
10.41
10.42 private class Decode_Chars(decode: String => String,
10.43 @@ -83,30 +63,36 @@
10.44 {
10.45 /* stack operations */
10.46
10.47 - var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
10.48 + def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
10.49 + var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
10.50
10.51 - def add(x: XML.Tree) = (stack: @unchecked) match {
10.52 - case ((elem, body) :: pending) => stack = (elem, x :: body) :: pending
10.53 + def add(x: XML.Tree)
10.54 + {
10.55 + (stack: @unchecked) match { case ((_, body) :: _) => body += x }
10.56 }
10.57
10.58 - def push(name: String, atts: XML.Attributes) =
10.59 + def push(name: String, atts: XML.Attributes)
10.60 + {
10.61 if (name == "") err_element()
10.62 - else stack = ((name, atts), Nil) :: stack
10.63 + else stack = ((name, atts), buffer()) :: stack
10.64 + }
10.65
10.66 - def pop() = (stack: @unchecked) match {
10.67 - case ((("", _), _) :: _) => err_unbalanced("")
10.68 - case (((name, atts), body) :: pending) =>
10.69 - stack = pending; add(XML.Elem(name, atts, body.reverse))
10.70 + def pop()
10.71 + {
10.72 + (stack: @unchecked) match {
10.73 + case ((("", _), _) :: _) => err_unbalanced("")
10.74 + case (((name, atts), body) :: pending) =>
10.75 + stack = pending; add(XML.Elem(name, atts, body.toList))
10.76 + }
10.77 }
10.78
10.79
10.80 /* parse chunks */
10.81
10.82 - stack = List((("", Nil), Nil))
10.83 - for (chunk <- chunks(X, source) if chunk.length != 0) {
10.84 + for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
10.85 if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
10.86 else {
10.87 - chunks(Y, chunk).toList match {
10.88 + Library.chunks(chunk, Y).toList match {
10.89 case ch :: name :: atts if ch.length == 0 =>
10.90 push(name.toString.intern, atts.map(parse_attrib))
10.91 case txts => for (txt <- txts) add(XML.Text(txt.toString))
10.92 @@ -114,7 +100,7 @@
10.93 }
10.94 }
10.95 stack match {
10.96 - case List((("", _), result)) => result.reverse
10.97 + case List((("", _), body)) => body.toList
10.98 case ((name, _), _) :: _ => err_unbalanced(name)
10.99 }
10.100 }
11.1 --- a/src/Pure/Isar/isar_document.scala Fri May 07 09:59:59 2010 +0200
11.2 +++ b/src/Pure/Isar/isar_document.scala Fri May 07 14:47:09 2010 +0200
11.3 @@ -14,6 +14,26 @@
11.4 type State_ID = String
11.5 type Command_ID = String
11.6 type Document_ID = String
11.7 +
11.8 +
11.9 + /* reports */
11.10 +
11.11 + object Assign {
11.12 + def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
11.13 + msg match {
11.14 + case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
11.15 + case _ => None
11.16 + }
11.17 + }
11.18 +
11.19 + object Edit {
11.20 + def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
11.21 + msg match {
11.22 + case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
11.23 + Some(cmd_id, state_id)
11.24 + case _ => None
11.25 + }
11.26 + }
11.27 }
11.28
11.29
12.1 --- a/src/Pure/Isar/outer_keyword.ML Fri May 07 09:59:59 2010 +0200
12.2 +++ b/src/Pure/Isar/outer_keyword.ML Fri May 07 14:47:09 2010 +0200
12.3 @@ -146,7 +146,7 @@
12.4 fun command_tags name = these (Option.map tags_of (command_keyword name));
12.5
12.6
12.7 -(* report *)
12.8 +(* reports *)
12.9
12.10 val keyword_status_reportN = "keyword_status_report";
12.11
13.1 --- a/src/Pure/Isar/outer_keyword.scala Fri May 07 09:59:59 2010 +0200
13.2 +++ b/src/Pure/Isar/outer_keyword.scala Fri May 07 14:47:09 2010 +0200
13.3 @@ -9,6 +9,8 @@
13.4
13.5 object Outer_Keyword
13.6 {
13.7 + /* kinds */
13.8 +
13.9 val MINOR = "minor"
13.10 val CONTROL = "control"
13.11 val DIAG = "diag"
13.12 @@ -33,6 +35,9 @@
13.13 val PRF_ASM_GOAL = "proof-asm-goal"
13.14 val PRF_SCRIPT = "proof-script"
13.15
13.16 +
13.17 + /* categories */
13.18 +
13.19 val minor = Set(MINOR)
13.20 val control = Set(CONTROL)
13.21 val diag = Set(DIAG)
13.22 @@ -43,5 +48,25 @@
13.23 Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
13.24 val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
13.25 val improper = Set(THY_SCRIPT, PRF_SCRIPT)
13.26 +
13.27 +
13.28 + /* reports */
13.29 +
13.30 + object Keyword_Decl {
13.31 + def unapply(msg: XML.Tree): Option[String] =
13.32 + msg match {
13.33 + case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
13.34 + case _ => None
13.35 + }
13.36 + }
13.37 +
13.38 + object Command_Decl {
13.39 + def unapply(msg: XML.Tree): Option[(String, String)] =
13.40 + msg match {
13.41 + case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
13.42 + Some((name, kind))
13.43 + case _ => None
13.44 + }
13.45 + }
13.46 }
13.47
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Pure/PIDE/change.scala Fri May 07 14:47:09 2010 +0200
14.3 @@ -0,0 +1,42 @@
14.4 +/* Title: Pure/PIDE/change.scala
14.5 + Author: Fabian Immler, TU Munich
14.6 + Author: Makarius
14.7 +
14.8 +Changes of plain text.
14.9 +*/
14.10 +
14.11 +package isabelle
14.12 +
14.13 +
14.14 +class Change(
14.15 + val id: Isar_Document.Document_ID,
14.16 + val parent: Option[Change],
14.17 + val edits: List[Text_Edit],
14.18 + val result: Future[(List[Document.Edit], Document)])
14.19 +{
14.20 + def ancestors: Iterator[Change] = new Iterator[Change]
14.21 + {
14.22 + private var state: Option[Change] = Some(Change.this)
14.23 + def hasNext = state.isDefined
14.24 + def next =
14.25 + state match {
14.26 + case Some(change) => state = change.parent; change
14.27 + case None => throw new NoSuchElementException("next on empty iterator")
14.28 + }
14.29 + }
14.30 +
14.31 + def join_document: Document = result.join._2
14.32 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
14.33 +
14.34 + def edit(session: Session, edits: List[Text_Edit]): Change =
14.35 + {
14.36 + val new_id = session.create_id()
14.37 + val result: Future[(List[Document.Edit], Document)] =
14.38 + Future.fork {
14.39 + val old_doc = join_document
14.40 + old_doc.await_assignment
14.41 + Document.text_edits(session, old_doc, new_id, edits)
14.42 + }
14.43 + new Change(new_id, Some(this), edits, result)
14.44 + }
14.45 +}
14.46 \ No newline at end of file
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/Pure/PIDE/command.scala Fri May 07 14:47:09 2010 +0200
15.3 @@ -0,0 +1,101 @@
15.4 +/* Title: Pure/PIDE/command.scala
15.5 + Author: Johannes Hölzl, TU Munich
15.6 + Author: Fabian Immler, TU Munich
15.7 + Author: Makarius
15.8 +
15.9 +Prover commands with semantic state.
15.10 +*/
15.11 +
15.12 +package isabelle
15.13 +
15.14 +
15.15 +import scala.actors.Actor, Actor._
15.16 +import scala.collection.mutable
15.17 +
15.18 +
15.19 +object Command
15.20 +{
15.21 + object Status extends Enumeration
15.22 + {
15.23 + val UNPROCESSED = Value("UNPROCESSED")
15.24 + val FINISHED = Value("FINISHED")
15.25 + val FAILED = Value("FAILED")
15.26 + }
15.27 +
15.28 + case class HighlightInfo(highlight: String) { override def toString = highlight }
15.29 + case class TypeInfo(ty: String)
15.30 + case class RefInfo(file: Option[String], line: Option[Int],
15.31 + command_id: Option[String], offset: Option[Int])
15.32 +}
15.33 +
15.34 +
15.35 +class Command(
15.36 + val id: Isar_Document.Command_ID,
15.37 + val span: Thy_Syntax.Span)
15.38 + extends Session.Entity
15.39 +{
15.40 + /* classification */
15.41 +
15.42 + def is_command: Boolean = !span.isEmpty && span.head.is_command
15.43 + def is_ignored: Boolean = span.forall(_.is_ignored)
15.44 + def is_malformed: Boolean = !is_command && !is_ignored
15.45 +
15.46 + def name: String = if (is_command) span.head.content else ""
15.47 + override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
15.48 +
15.49 +
15.50 + /* source text */
15.51 +
15.52 + val source: String = span.map(_.source).mkString
15.53 + def source(i: Int, j: Int): String = source.substring(i, j)
15.54 + def length: Int = source.length
15.55 +
15.56 + lazy val symbol_index = new Symbol.Index(source)
15.57 +
15.58 +
15.59 + /* accumulated messages */
15.60 +
15.61 + @volatile protected var state = new State(this)
15.62 + def current_state: State = state
15.63 +
15.64 + private case class Consume(session: Session, message: XML.Tree)
15.65 + private case object Assign
15.66 +
15.67 + private val accumulator = actor {
15.68 + var assigned = false
15.69 + loop {
15.70 + react {
15.71 + case Consume(session: Session, message: XML.Tree) if !assigned =>
15.72 + state = state.+(session, message)
15.73 +
15.74 + case Assign =>
15.75 + assigned = true // single assignment
15.76 + reply(())
15.77 +
15.78 + case bad => System.err.println("command accumulator: ignoring bad message " + bad)
15.79 + }
15.80 + }
15.81 + }
15.82 +
15.83 + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
15.84 +
15.85 + def assign_state(state_id: Isar_Document.State_ID): Command =
15.86 + {
15.87 + val cmd = new Command(state_id, span)
15.88 + accumulator !? Assign
15.89 + cmd.state = current_state
15.90 + cmd
15.91 + }
15.92 +
15.93 +
15.94 + /* markup */
15.95 +
15.96 + lazy val empty_markup = new Markup_Text(Nil, source)
15.97 +
15.98 + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
15.99 + {
15.100 + val start = symbol_index.decode(begin)
15.101 + val stop = symbol_index.decode(end)
15.102 + new Markup_Tree(new Markup_Node(start, stop, info), Nil)
15.103 + }
15.104 +}
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/Pure/PIDE/document.scala Fri May 07 14:47:09 2010 +0200
16.3 @@ -0,0 +1,197 @@
16.4 +/* Title: Pure/PIDE/document.scala
16.5 + Author: Makarius
16.6 +
16.7 +Document as editable list of commands.
16.8 +*/
16.9 +
16.10 +package isabelle
16.11 +
16.12 +
16.13 +object Document
16.14 +{
16.15 + /* command start positions */
16.16 +
16.17 + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
16.18 + {
16.19 + var offset = 0
16.20 + for (cmd <- commands.iterator) yield {
16.21 + val start = offset
16.22 + offset += cmd.length
16.23 + (cmd, start)
16.24 + }
16.25 + }
16.26 +
16.27 +
16.28 + /* empty document */
16.29 +
16.30 + def empty(id: Isar_Document.Document_ID): Document =
16.31 + {
16.32 + val doc = new Document(id, Linear_Set(), Map())
16.33 + doc.assign_states(Nil)
16.34 + doc
16.35 + }
16.36 +
16.37 +
16.38 + // FIXME
16.39 + var phase0: List[Text_Edit] = null
16.40 + var phase1: Linear_Set[Command] = null
16.41 + var phase2: Linear_Set[Command] = null
16.42 + var phase3: List[Edit] = null
16.43 +
16.44 +
16.45 +
16.46 + /** document edits **/
16.47 +
16.48 + type Edit = (Option[Command], Option[Command])
16.49 +
16.50 + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
16.51 + edits: List[Text_Edit]): (List[Edit], Document) =
16.52 + {
16.53 + require(old_doc.assignment.is_finished)
16.54 +
16.55 +
16.56 + /* unparsed dummy commands */
16.57 +
16.58 + def unparsed(source: String) =
16.59 + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
16.60 +
16.61 + def is_unparsed(command: Command) = command.id == null
16.62 +
16.63 + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
16.64 +
16.65 +
16.66 + /* phase 1: edit individual command source */
16.67 +
16.68 + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
16.69 + {
16.70 + eds match {
16.71 + case e :: es =>
16.72 + command_starts(commands).find { // FIXME relative search!
16.73 + case (cmd, cmd_start) =>
16.74 + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
16.75 + } match {
16.76 + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
16.77 + val (rest, text) = e.edit(cmd.source, cmd_start)
16.78 + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
16.79 + edit_text(rest.toList ::: es, new_commands)
16.80 +
16.81 + case Some((cmd, cmd_start)) =>
16.82 + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
16.83 +
16.84 + case None =>
16.85 + require(e.is_insert && e.start == 0)
16.86 + edit_text(es, commands.insert_after(None, unparsed(e.text)))
16.87 + }
16.88 + case Nil => commands
16.89 + }
16.90 + }
16.91 +
16.92 +
16.93 + /* phase 2: recover command spans */
16.94 +
16.95 + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
16.96 + {
16.97 + // FIXME relative search!
16.98 + commands.iterator.find(is_unparsed) match {
16.99 + case Some(first_unparsed) =>
16.100 + val prefix = commands.prev(first_unparsed)
16.101 + val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
16.102 + val suffix = commands.next(body.last)
16.103 +
16.104 + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
16.105 + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
16.106 +
16.107 + val (before_edit, spans1) =
16.108 + if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
16.109 + (prefix, spans0.tail)
16.110 + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
16.111 +
16.112 + val (after_edit, spans2) =
16.113 + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
16.114 + (suffix, spans1.take(spans1.length - 1))
16.115 + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
16.116 +
16.117 + val inserted = spans2.map(span => new Command(session.create_id(), span))
16.118 + val new_commands =
16.119 + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
16.120 + parse_spans(new_commands)
16.121 +
16.122 + case None => commands
16.123 + }
16.124 + }
16.125 +
16.126 +
16.127 + /* phase 3: resulting document edits */
16.128 +
16.129 + val result = Library.timeit("text_edits") {
16.130 + val commands0 = old_doc.commands
16.131 + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
16.132 + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
16.133 +
16.134 + val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
16.135 + val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
16.136 +
16.137 + val doc_edits =
16.138 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
16.139 + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
16.140 +
16.141 + val former_states = old_doc.assignment.join -- removed_commands
16.142 +
16.143 + phase0 = edits
16.144 + phase1 = commands1
16.145 + phase2 = commands2
16.146 + phase3 = doc_edits
16.147 +
16.148 + (doc_edits, new Document(new_id, commands2, former_states))
16.149 + }
16.150 + result
16.151 + }
16.152 +}
16.153 +
16.154 +
16.155 +class Document(
16.156 + val id: Isar_Document.Document_ID,
16.157 + val commands: Linear_Set[Command],
16.158 + former_states: Map[Command, Command])
16.159 +{
16.160 + /* command ranges */
16.161 +
16.162 + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
16.163 +
16.164 + def command_start(cmd: Command): Option[Int] =
16.165 + command_starts.find(_._1 == cmd).map(_._2)
16.166 +
16.167 + def command_range(i: Int): Iterator[(Command, Int)] =
16.168 + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
16.169 +
16.170 + def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
16.171 + command_range(i) takeWhile { case (_, start) => start < j }
16.172 +
16.173 + def command_at(i: Int): Option[(Command, Int)] =
16.174 + {
16.175 + val range = command_range(i)
16.176 + if (range.hasNext) Some(range.next) else None
16.177 + }
16.178 +
16.179 +
16.180 + /* command state assignment */
16.181 +
16.182 + val assignment = Future.promise[Map[Command, Command]]
16.183 + def await_assignment { assignment.join }
16.184 +
16.185 + @volatile private var tmp_states = former_states
16.186 + private val time0 = System.currentTimeMillis
16.187 +
16.188 + def assign_states(new_states: List[(Command, Command)])
16.189 + {
16.190 + assignment.fulfill(tmp_states ++ new_states)
16.191 + tmp_states = Map()
16.192 + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
16.193 + }
16.194 +
16.195 + def current_state(cmd: Command): Option[State] =
16.196 + {
16.197 + require(assignment.is_finished)
16.198 + (assignment.join).get(cmd).map(_.current_state)
16.199 + }
16.200 +}
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/Pure/PIDE/event_bus.scala Fri May 07 14:47:09 2010 +0200
17.3 @@ -0,0 +1,35 @@
17.4 +/* Title: Pure/PIDE/event_bus.scala
17.5 + Author: Makarius
17.6 +
17.7 +Generic event bus with multiple receiving actors.
17.8 +*/
17.9 +
17.10 +package isabelle
17.11 +
17.12 +import scala.actors.Actor, Actor._
17.13 +import scala.collection.mutable.ListBuffer
17.14 +
17.15 +
17.16 +class Event_Bus[Event]
17.17 +{
17.18 + /* receivers */
17.19 +
17.20 + private val receivers = new ListBuffer[Actor]
17.21 +
17.22 + def += (r: Actor) { synchronized { receivers += r } }
17.23 + def + (r: Actor): Event_Bus[Event] = { this += r; this }
17.24 +
17.25 + def += (f: Event => Unit) {
17.26 + this += actor { loop { react { case x: Event => f(x) } } }
17.27 + }
17.28 +
17.29 + def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
17.30 +
17.31 + def -= (r: Actor) { synchronized { receivers -= r } }
17.32 + def - (r: Actor) = { this -= r; this }
17.33 +
17.34 +
17.35 + /* event invocation */
17.36 +
17.37 + def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
17.38 +}
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/Pure/PIDE/markup_node.scala Fri May 07 14:47:09 2010 +0200
18.3 @@ -0,0 +1,110 @@
18.4 +/* Title: Pure/PIDE/markup_node.scala
18.5 + Author: Fabian Immler, TU Munich
18.6 + Author: Makarius
18.7 +
18.8 +Document markup nodes, with connection to Swing tree model.
18.9 +*/
18.10 +
18.11 +package isabelle
18.12 +
18.13 +
18.14 +import javax.swing.tree.DefaultMutableTreeNode
18.15 +
18.16 +
18.17 +
18.18 +case class Markup_Node(val start: Int, val stop: Int, val info: Any)
18.19 +{
18.20 + def fits_into(that: Markup_Node): Boolean =
18.21 + that.start <= this.start && this.stop <= that.stop
18.22 +}
18.23 +
18.24 +
18.25 +case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
18.26 +{
18.27 + private def add(branch: Markup_Tree) = // FIXME avoid sort
18.28 + copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
18.29 +
18.30 + private def remove(bs: List[Markup_Tree]) =
18.31 + copy(branches = branches.filterNot(bs.contains(_)))
18.32 +
18.33 + def + (new_tree: Markup_Tree): Markup_Tree =
18.34 + {
18.35 + val new_node = new_tree.node
18.36 + if (new_node fits_into node) {
18.37 + var inserted = false
18.38 + val new_branches =
18.39 + branches.map(branch =>
18.40 + if ((new_node fits_into branch.node) && !inserted) {
18.41 + inserted = true
18.42 + branch + new_tree
18.43 + }
18.44 + else branch)
18.45 + if (!inserted) {
18.46 + // new_tree did not fit into children of this
18.47 + // -> insert between this and its branches
18.48 + val fitting = branches filter(_.node fits_into new_node)
18.49 + (this remove fitting) add ((new_tree /: fitting)(_ + _))
18.50 + }
18.51 + else copy(branches = new_branches)
18.52 + }
18.53 + else {
18.54 + System.err.println("ignored nonfitting markup: " + new_node)
18.55 + this
18.56 + }
18.57 + }
18.58 +
18.59 + def flatten: List[Markup_Node] =
18.60 + {
18.61 + var next_x = node.start
18.62 + if (branches.isEmpty) List(this.node)
18.63 + else {
18.64 + val filled_gaps =
18.65 + for {
18.66 + child <- branches
18.67 + markups =
18.68 + if (next_x < child.node.start)
18.69 + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
18.70 + else child.flatten
18.71 + update = (next_x = child.node.stop)
18.72 + markup <- markups
18.73 + } yield markup
18.74 + if (next_x < node.stop)
18.75 + filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
18.76 + else filled_gaps
18.77 + }
18.78 + }
18.79 +}
18.80 +
18.81 +
18.82 +case class Markup_Text(val markup: List[Markup_Tree], val content: String)
18.83 +{
18.84 + private lazy val root =
18.85 + new Markup_Tree(new Markup_Node(0, content.length, None), markup)
18.86 +
18.87 + def + (new_tree: Markup_Tree): Markup_Text =
18.88 + new Markup_Text((root + new_tree).branches, content)
18.89 +
18.90 + def filter(pred: Markup_Node => Boolean): Markup_Text =
18.91 + {
18.92 + def filt(tree: Markup_Tree): List[Markup_Tree] =
18.93 + {
18.94 + val branches = tree.branches.flatMap(filt(_))
18.95 + if (pred(tree.node)) List(tree.copy(branches = branches))
18.96 + else branches
18.97 + }
18.98 + new Markup_Text(markup.flatMap(filt(_)), content)
18.99 + }
18.100 +
18.101 + def flatten: List[Markup_Node] = markup.flatten(_.flatten)
18.102 +
18.103 + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
18.104 + {
18.105 + def swing(tree: Markup_Tree): DefaultMutableTreeNode =
18.106 + {
18.107 + val node = swing_node(tree.node)
18.108 + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
18.109 + node
18.110 + }
18.111 + swing(root)
18.112 + }
18.113 +}
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/Pure/PIDE/state.scala Fri May 07 14:47:09 2010 +0200
19.3 @@ -0,0 +1,119 @@
19.4 +/* Title: Pure/PIDE/state.scala
19.5 + Author: Fabian Immler, TU Munich
19.6 + Author: Makarius
19.7 +
19.8 +Accumulating results from prover.
19.9 +*/
19.10 +
19.11 +package isabelle
19.12 +
19.13 +
19.14 +class State(
19.15 + val command: Command,
19.16 + val status: Command.Status.Value,
19.17 + val rev_results: List[XML.Tree],
19.18 + val markup_root: Markup_Text)
19.19 +{
19.20 + def this(command: Command) =
19.21 + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
19.22 +
19.23 +
19.24 + /* content */
19.25 +
19.26 + private def set_status(st: Command.Status.Value): State =
19.27 + new State(command, st, rev_results, markup_root)
19.28 +
19.29 + private def add_result(res: XML.Tree): State =
19.30 + new State(command, status, res :: rev_results, markup_root)
19.31 +
19.32 + private def add_markup(node: Markup_Tree): State =
19.33 + new State(command, status, rev_results, markup_root + node)
19.34 +
19.35 + lazy val results = rev_results.reverse
19.36 +
19.37 +
19.38 + /* markup */
19.39 +
19.40 + lazy val highlight: Markup_Text =
19.41 + {
19.42 + markup_root.filter(_.info match {
19.43 + case Command.HighlightInfo(_) => true
19.44 + case _ => false
19.45 + })
19.46 + }
19.47 +
19.48 + private lazy val types: List[Markup_Node] =
19.49 + markup_root.filter(_.info match {
19.50 + case Command.TypeInfo(_) => true
19.51 + case _ => false }).flatten
19.52 +
19.53 + def type_at(pos: Int): Option[String] =
19.54 + {
19.55 + types.find(t => t.start <= pos && pos < t.stop) match {
19.56 + case Some(t) =>
19.57 + t.info match {
19.58 + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
19.59 + case _ => None
19.60 + }
19.61 + case None => None
19.62 + }
19.63 + }
19.64 +
19.65 + private lazy val refs: List[Markup_Node] =
19.66 + markup_root.filter(_.info match {
19.67 + case Command.RefInfo(_, _, _, _) => true
19.68 + case _ => false }).flatten
19.69 +
19.70 + def ref_at(pos: Int): Option[Markup_Node] =
19.71 + refs.find(t => t.start <= pos && pos < t.stop)
19.72 +
19.73 +
19.74 + /* message dispatch */
19.75 +
19.76 + def + (session: Session, message: XML.Tree): State =
19.77 + {
19.78 + val changed: State =
19.79 + message match {
19.80 + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
19.81 + (this /: elems)((state, elem) =>
19.82 + elem match {
19.83 + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
19.84 + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
19.85 + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
19.86 + case XML.Elem(kind, atts, body) =>
19.87 + atts match {
19.88 + case Position.Range(begin, end) =>
19.89 + if (kind == Markup.ML_TYPING) {
19.90 + val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!?
19.91 + state.add_markup(
19.92 + command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
19.93 + }
19.94 + else if (kind == Markup.ML_REF) {
19.95 + body match {
19.96 + case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
19.97 + state.add_markup(command.markup_node(
19.98 + begin - 1, end - 1,
19.99 + Command.RefInfo(
19.100 + Position.get_file(atts),
19.101 + Position.get_line(atts),
19.102 + Position.get_id(atts),
19.103 + Position.get_offset(atts))))
19.104 + case _ => state
19.105 + }
19.106 + }
19.107 + else {
19.108 + state.add_markup(
19.109 + command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
19.110 + }
19.111 + case _ => state
19.112 + }
19.113 + case _ =>
19.114 + System.err.println("ignored status report: " + elem)
19.115 + state
19.116 + })
19.117 + case _ => add_result(message)
19.118 + }
19.119 + if (!(this eq changed)) session.command_change.event(command)
19.120 + changed
19.121 + }
19.122 +}
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/Pure/PIDE/text_edit.scala Fri May 07 14:47:09 2010 +0200
20.3 @@ -0,0 +1,51 @@
20.4 +/* Title: Pure/PIDE/text_edit.scala
20.5 + Author: Fabian Immler, TU Munich
20.6 + Author: Makarius
20.7 +
20.8 +Basic edits on plain text.
20.9 +*/
20.10 +
20.11 +package isabelle
20.12 +
20.13 +
20.14 +class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
20.15 +{
20.16 + override def toString =
20.17 + (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
20.18 +
20.19 +
20.20 + /* transform offsets */
20.21 +
20.22 + private def transform(do_insert: Boolean, offset: Int): Int =
20.23 + if (offset < start) offset
20.24 + else if (is_insert == do_insert) offset + text.length
20.25 + else (offset - text.length) max start
20.26 +
20.27 + def after(offset: Int): Int = transform(true, offset)
20.28 + def before(offset: Int): Int = transform(false, offset)
20.29 +
20.30 +
20.31 + /* edit strings */
20.32 +
20.33 + private def insert(index: Int, string: String): String =
20.34 + string.substring(0, index) + text + string.substring(index)
20.35 +
20.36 + private def remove(index: Int, count: Int, string: String): String =
20.37 + string.substring(0, index) + string.substring(index + count)
20.38 +
20.39 + def can_edit(string: String, shift: Int): Boolean =
20.40 + shift <= start && start < shift + string.length
20.41 +
20.42 + def edit(string: String, shift: Int): (Option[Text_Edit], String) =
20.43 + if (!can_edit(string, shift)) (Some(this), string)
20.44 + else if (is_insert) (None, insert(start - shift, string))
20.45 + else {
20.46 + val index = start - shift
20.47 + val count = text.length min (string.length - index)
20.48 + val rest =
20.49 + if (count == text.length) None
20.50 + else Some(new Text_Edit(false, start, text.substring(count)))
20.51 + (rest, remove(index, count, string))
20.52 + }
20.53 +}
20.54 +
21.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri May 07 09:59:59 2010 +0200
21.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri May 07 14:47:09 2010 +0200
21.3 @@ -115,8 +115,6 @@
21.4 [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
21.5 else if name = Markup.breakN then
21.6 [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
21.7 - else if name = Markup.fbreakN then
21.8 - [Pgml.Break {mandatory = SOME true, indent = NONE}]
21.9 else content
21.10 end
21.11 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/Pure/System/download.scala Fri May 07 14:47:09 2010 +0200
22.3 @@ -0,0 +1,53 @@
22.4 +/* Title: Pure/System/download.scala
22.5 + Author: Makarius
22.6 +
22.7 +Download URLs -- with progress monitor.
22.8 +*/
22.9 +
22.10 +package isabelle
22.11 +
22.12 +
22.13 +import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
22.14 + File, InterruptedIOException}
22.15 +import java.net.{URL, URLConnection}
22.16 +import java.awt.{Component, HeadlessException}
22.17 +import javax.swing.ProgressMonitorInputStream
22.18 +
22.19 +
22.20 +object Download
22.21 +{
22.22 + def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
22.23 + {
22.24 + val connection = url.openConnection
22.25 +
22.26 + val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
22.27 + val monitor = stream.getProgressMonitor
22.28 + monitor.setNote(connection.getURL.toString)
22.29 +
22.30 + val length = connection.getContentLength
22.31 + if (length != -1) monitor.setMaximum(length)
22.32 +
22.33 + (connection, new BufferedInputStream(stream))
22.34 + }
22.35 +
22.36 + def file(parent: Component, url: URL, file: File)
22.37 + {
22.38 + val (connection, instream) = stream(parent, url)
22.39 + val mod_time = connection.getLastModified
22.40 +
22.41 + def read() =
22.42 + try { instream.read }
22.43 + catch { case _ : InterruptedIOException => error("Download canceled!") }
22.44 + try {
22.45 + val outstream = new BufferedOutputStream(new FileOutputStream(file))
22.46 + try {
22.47 + var c: Int = 0
22.48 + while ({ c = read(); c != -1}) outstream.write(c)
22.49 + }
22.50 + finally { outstream.close }
22.51 + if (mod_time > 0) file.setLastModified(mod_time)
22.52 + }
22.53 + finally { instream.close }
22.54 + }
22.55 +}
22.56 +
23.1 --- a/src/Pure/System/gui_setup.scala Fri May 07 09:59:59 2010 +0200
23.2 +++ b/src/Pure/System/gui_setup.scala Fri May 07 14:47:09 2010 +0200
23.3 @@ -12,15 +12,13 @@
23.4 import scala.swing.event._
23.5
23.6
23.7 -object GUI_Setup extends GUIApplication
23.8 +object GUI_Setup extends SwingApplication
23.9 {
23.10 - def main(args: Array[String]) =
23.11 + def startup(args: Array[String]) =
23.12 {
23.13 - Swing_Thread.later {
23.14 - UIManager.setLookAndFeel(Platform.look_and_feel)
23.15 - top.pack()
23.16 - top.visible = true
23.17 - }
23.18 + UIManager.setLookAndFeel(Platform.look_and_feel)
23.19 + top.pack()
23.20 + top.visible = true
23.21 }
23.22
23.23 def top = new MainFrame {
24.1 --- a/src/Pure/System/session.scala Fri May 07 09:59:59 2010 +0200
24.2 +++ b/src/Pure/System/session.scala Fri May 07 14:47:09 2010 +0200
24.3 @@ -1,8 +1,8 @@
24.4 -/*
24.5 - * Isabelle session, potentially with running prover
24.6 - *
24.7 - * @author Makarius
24.8 - */
24.9 +/* Title: Pure/System/session.scala
24.10 + Author: Makarius
24.11 +
24.12 +Isabelle session, potentially with running prover.
24.13 +*/
24.14
24.15 package isabelle
24.16
24.17 @@ -123,12 +123,12 @@
24.18 result.body match {
24.19
24.20 // document state assignment
24.21 - case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
24.22 + case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
24.23 documents.get(target_id.get) match {
24.24 case Some(doc) =>
24.25 val states =
24.26 for {
24.27 - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits
24.28 + Isar_Document.Edit(cmd_id, state_id) <- edits
24.29 cmd <- lookup_command(cmd_id)
24.30 } yield {
24.31 val st = cmd.assign_state(state_id)
24.32 @@ -139,11 +139,9 @@
24.33 case None => bad_result(result)
24.34 }
24.35
24.36 - // command and keyword declarations
24.37 - case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
24.38 - syntax += (name, kind)
24.39 - case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
24.40 - syntax += name
24.41 + // keyword declarations
24.42 + case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
24.43 + case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name
24.44
24.45 case _ => if (!result.is_ready) bad_result(result)
24.46 }
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/src/Pure/System/swing_thread.scala Fri May 07 14:47:09 2010 +0200
25.3 @@ -0,0 +1,63 @@
25.4 +/* Title: Pure/System/swing_thread.scala
25.5 + Author: Makarius
25.6 + Author: Fabian Immler, TU Munich
25.7 +
25.8 +Evaluation within the AWT/Swing thread.
25.9 +*/
25.10 +
25.11 +package isabelle
25.12 +
25.13 +import javax.swing.{SwingUtilities, Timer}
25.14 +import java.awt.event.{ActionListener, ActionEvent}
25.15 +
25.16 +
25.17 +object Swing_Thread
25.18 +{
25.19 + /* checks */
25.20 +
25.21 + def assert() = Predef.assert(SwingUtilities.isEventDispatchThread())
25.22 + def require() = Predef.require(SwingUtilities.isEventDispatchThread())
25.23 +
25.24 +
25.25 + /* main dispatch queue */
25.26 +
25.27 + def now[A](body: => A): A =
25.28 + {
25.29 + var result: Option[A] = None
25.30 + if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
25.31 + else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
25.32 + result.get
25.33 + }
25.34 +
25.35 + def future[A](body: => A): Future[A] =
25.36 + {
25.37 + if (SwingUtilities.isEventDispatchThread()) Future.value(body)
25.38 + else Future.fork { now(body) }
25.39 + }
25.40 +
25.41 + def later(body: => Unit)
25.42 + {
25.43 + if (SwingUtilities.isEventDispatchThread()) body
25.44 + else SwingUtilities.invokeLater(new Runnable { def run = body })
25.45 + }
25.46 +
25.47 +
25.48 + /* delayed actions */
25.49 +
25.50 + private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
25.51 + {
25.52 + val listener =
25.53 + new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
25.54 + val timer = new Timer(time_span, listener)
25.55 + timer.setRepeats(false)
25.56 +
25.57 + def invoke() { if (first) timer.start() else timer.restart() }
25.58 + invoke _
25.59 + }
25.60 +
25.61 + // delayed action after first invocation
25.62 + def delay_first = delayed_action(true) _
25.63 +
25.64 + // delayed action after last invocation
25.65 + def delay_last = delayed_action(false) _
25.66 +}
26.1 --- a/src/Pure/Thy/change.scala Fri May 07 09:59:59 2010 +0200
26.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
26.3 @@ -1,42 +0,0 @@
26.4 -/*
26.5 - * Changes of plain text
26.6 - *
26.7 - * @author Fabian Immler, TU Munich
26.8 - * @author Makarius
26.9 - */
26.10 -
26.11 -package isabelle
26.12 -
26.13 -
26.14 -class Change(
26.15 - val id: Isar_Document.Document_ID,
26.16 - val parent: Option[Change],
26.17 - val edits: List[Text_Edit],
26.18 - val result: Future[(List[Document.Edit], Document)])
26.19 -{
26.20 - def ancestors: Iterator[Change] = new Iterator[Change]
26.21 - {
26.22 - private var state: Option[Change] = Some(Change.this)
26.23 - def hasNext = state.isDefined
26.24 - def next =
26.25 - state match {
26.26 - case Some(change) => state = change.parent; change
26.27 - case None => throw new NoSuchElementException("next on empty iterator")
26.28 - }
26.29 - }
26.30 -
26.31 - def join_document: Document = result.join._2
26.32 - def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
26.33 -
26.34 - def edit(session: Session, edits: List[Text_Edit]): Change =
26.35 - {
26.36 - val new_id = session.create_id()
26.37 - val result: Future[(List[Document.Edit], Document)] =
26.38 - Future.fork {
26.39 - val old_doc = join_document
26.40 - old_doc.await_assignment
26.41 - Document.text_edits(session, old_doc, new_id, edits)
26.42 - }
26.43 - new Change(new_id, Some(this), edits, result)
26.44 - }
26.45 -}
26.46 \ No newline at end of file
27.1 --- a/src/Pure/Thy/command.scala Fri May 07 09:59:59 2010 +0200
27.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
27.3 @@ -1,100 +0,0 @@
27.4 -/*
27.5 - * Prover commands with semantic state
27.6 - *
27.7 - * @author Johannes Hölzl, TU Munich
27.8 - * @author Fabian Immler, TU Munich
27.9 - */
27.10 -
27.11 -package isabelle
27.12 -
27.13 -
27.14 -import scala.actors.Actor, Actor._
27.15 -import scala.collection.mutable
27.16 -
27.17 -
27.18 -object Command
27.19 -{
27.20 - object Status extends Enumeration
27.21 - {
27.22 - val UNPROCESSED = Value("UNPROCESSED")
27.23 - val FINISHED = Value("FINISHED")
27.24 - val FAILED = Value("FAILED")
27.25 - }
27.26 -
27.27 - case class HighlightInfo(highlight: String) { override def toString = highlight }
27.28 - case class TypeInfo(ty: String)
27.29 - case class RefInfo(file: Option[String], line: Option[Int],
27.30 - command_id: Option[String], offset: Option[Int])
27.31 -}
27.32 -
27.33 -
27.34 -class Command(
27.35 - val id: Isar_Document.Command_ID,
27.36 - val span: Thy_Syntax.Span)
27.37 - extends Session.Entity
27.38 -{
27.39 - /* classification */
27.40 -
27.41 - def is_command: Boolean = !span.isEmpty && span.head.is_command
27.42 - def is_ignored: Boolean = span.forall(_.is_ignored)
27.43 - def is_malformed: Boolean = !is_command && !is_ignored
27.44 -
27.45 - def name: String = if (is_command) span.head.content else ""
27.46 - override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
27.47 -
27.48 -
27.49 - /* source text */
27.50 -
27.51 - val source: String = span.map(_.source).mkString
27.52 - def source(i: Int, j: Int): String = source.substring(i, j)
27.53 - def length: Int = source.length
27.54 -
27.55 - lazy val symbol_index = new Symbol.Index(source)
27.56 -
27.57 -
27.58 - /* accumulated messages */
27.59 -
27.60 - @volatile protected var state = new State(this)
27.61 - def current_state: State = state
27.62 -
27.63 - private case class Consume(session: Session, message: XML.Tree)
27.64 - private case object Assign
27.65 -
27.66 - private val accumulator = actor {
27.67 - var assigned = false
27.68 - loop {
27.69 - react {
27.70 - case Consume(session: Session, message: XML.Tree) if !assigned =>
27.71 - state = state.+(session, message)
27.72 -
27.73 - case Assign =>
27.74 - assigned = true // single assignment
27.75 - reply(())
27.76 -
27.77 - case bad => System.err.println("command accumulator: ignoring bad message " + bad)
27.78 - }
27.79 - }
27.80 - }
27.81 -
27.82 - def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
27.83 -
27.84 - def assign_state(state_id: Isar_Document.State_ID): Command =
27.85 - {
27.86 - val cmd = new Command(state_id, span)
27.87 - accumulator !? Assign
27.88 - cmd.state = current_state
27.89 - cmd
27.90 - }
27.91 -
27.92 -
27.93 - /* markup */
27.94 -
27.95 - lazy val empty_markup = new Markup_Text(Nil, source)
27.96 -
27.97 - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
27.98 - {
27.99 - val start = symbol_index.decode(begin)
27.100 - val stop = symbol_index.decode(end)
27.101 - new Markup_Tree(new Markup_Node(start, stop, info), Nil)
27.102 - }
27.103 -}
28.1 --- a/src/Pure/Thy/document.scala Fri May 07 09:59:59 2010 +0200
28.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
28.3 @@ -1,197 +0,0 @@
28.4 -/*
28.5 - * Document as editable list of commands
28.6 - *
28.7 - * @author Makarius
28.8 - */
28.9 -
28.10 -package isabelle
28.11 -
28.12 -
28.13 -object Document
28.14 -{
28.15 - /* command start positions */
28.16 -
28.17 - def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
28.18 - {
28.19 - var offset = 0
28.20 - for (cmd <- commands.iterator) yield {
28.21 - val start = offset
28.22 - offset += cmd.length
28.23 - (cmd, start)
28.24 - }
28.25 - }
28.26 -
28.27 -
28.28 - /* empty document */
28.29 -
28.30 - def empty(id: Isar_Document.Document_ID): Document =
28.31 - {
28.32 - val doc = new Document(id, Linear_Set(), Map())
28.33 - doc.assign_states(Nil)
28.34 - doc
28.35 - }
28.36 -
28.37 -
28.38 - // FIXME
28.39 - var phase0: List[Text_Edit] = null
28.40 - var phase1: Linear_Set[Command] = null
28.41 - var phase2: Linear_Set[Command] = null
28.42 - var phase3: List[Edit] = null
28.43 -
28.44 -
28.45 -
28.46 - /** document edits **/
28.47 -
28.48 - type Edit = (Option[Command], Option[Command])
28.49 -
28.50 - def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
28.51 - edits: List[Text_Edit]): (List[Edit], Document) =
28.52 - {
28.53 - require(old_doc.assignment.is_finished)
28.54 -
28.55 -
28.56 - /* unparsed dummy commands */
28.57 -
28.58 - def unparsed(source: String) =
28.59 - new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
28.60 -
28.61 - def is_unparsed(command: Command) = command.id == null
28.62 -
28.63 - assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
28.64 -
28.65 -
28.66 - /* phase 1: edit individual command source */
28.67 -
28.68 - def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
28.69 - {
28.70 - eds match {
28.71 - case e :: es =>
28.72 - command_starts(commands).find { // FIXME relative search!
28.73 - case (cmd, cmd_start) =>
28.74 - e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
28.75 - } match {
28.76 - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
28.77 - val (rest, text) = e.edit(cmd.source, cmd_start)
28.78 - val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
28.79 - edit_text(rest.toList ::: es, new_commands)
28.80 -
28.81 - case Some((cmd, cmd_start)) =>
28.82 - edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
28.83 -
28.84 - case None =>
28.85 - require(e.is_insert && e.start == 0)
28.86 - edit_text(es, commands.insert_after(None, unparsed(e.text)))
28.87 - }
28.88 - case Nil => commands
28.89 - }
28.90 - }
28.91 -
28.92 -
28.93 - /* phase 2: recover command spans */
28.94 -
28.95 - def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
28.96 - {
28.97 - // FIXME relative search!
28.98 - commands.iterator.find(is_unparsed) match {
28.99 - case Some(first_unparsed) =>
28.100 - val prefix = commands.prev(first_unparsed)
28.101 - val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
28.102 - val suffix = commands.next(body.last)
28.103 -
28.104 - val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
28.105 - val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
28.106 -
28.107 - val (before_edit, spans1) =
28.108 - if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
28.109 - (prefix, spans0.tail)
28.110 - else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
28.111 -
28.112 - val (after_edit, spans2) =
28.113 - if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
28.114 - (suffix, spans1.take(spans1.length - 1))
28.115 - else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
28.116 -
28.117 - val inserted = spans2.map(span => new Command(session.create_id(), span))
28.118 - val new_commands =
28.119 - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
28.120 - parse_spans(new_commands)
28.121 -
28.122 - case None => commands
28.123 - }
28.124 - }
28.125 -
28.126 -
28.127 - /* phase 3: resulting document edits */
28.128 -
28.129 - val result = Library.timeit("text_edits") {
28.130 - val commands0 = old_doc.commands
28.131 - val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
28.132 - val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
28.133 -
28.134 - val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
28.135 - val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
28.136 -
28.137 - val doc_edits =
28.138 - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
28.139 - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
28.140 -
28.141 - val former_states = old_doc.assignment.join -- removed_commands
28.142 -
28.143 - phase0 = edits
28.144 - phase1 = commands1
28.145 - phase2 = commands2
28.146 - phase3 = doc_edits
28.147 -
28.148 - (doc_edits, new Document(new_id, commands2, former_states))
28.149 - }
28.150 - result
28.151 - }
28.152 -}
28.153 -
28.154 -
28.155 -class Document(
28.156 - val id: Isar_Document.Document_ID,
28.157 - val commands: Linear_Set[Command],
28.158 - former_states: Map[Command, Command])
28.159 -{
28.160 - /* command ranges */
28.161 -
28.162 - def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
28.163 -
28.164 - def command_start(cmd: Command): Option[Int] =
28.165 - command_starts.find(_._1 == cmd).map(_._2)
28.166 -
28.167 - def command_range(i: Int): Iterator[(Command, Int)] =
28.168 - command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
28.169 -
28.170 - def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
28.171 - command_range(i) takeWhile { case (_, start) => start < j }
28.172 -
28.173 - def command_at(i: Int): Option[(Command, Int)] =
28.174 - {
28.175 - val range = command_range(i)
28.176 - if (range.hasNext) Some(range.next) else None
28.177 - }
28.178 -
28.179 -
28.180 - /* command state assignment */
28.181 -
28.182 - val assignment = Future.promise[Map[Command, Command]]
28.183 - def await_assignment { assignment.join }
28.184 -
28.185 - @volatile private var tmp_states = former_states
28.186 - private val time0 = System.currentTimeMillis
28.187 -
28.188 - def assign_states(new_states: List[(Command, Command)])
28.189 - {
28.190 - assignment.fulfill(tmp_states ++ new_states)
28.191 - tmp_states = Map()
28.192 - System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
28.193 - }
28.194 -
28.195 - def current_state(cmd: Command): Option[State] =
28.196 - {
28.197 - require(assignment.is_finished)
28.198 - (assignment.join).get(cmd).map(_.current_state)
28.199 - }
28.200 -}
29.1 --- a/src/Pure/Thy/markup_node.scala Fri May 07 09:59:59 2010 +0200
29.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
29.3 @@ -1,111 +0,0 @@
29.4 -/*
29.5 - * Document markup nodes, with connection to Swing tree model
29.6 - *
29.7 - * @author Fabian Immler, TU Munich
29.8 - * @author Makarius
29.9 - */
29.10 -
29.11 -package isabelle
29.12 -
29.13 -
29.14 -import javax.swing.tree.DefaultMutableTreeNode
29.15 -
29.16 -
29.17 -
29.18 -class Markup_Node(val start: Int, val stop: Int, val info: Any)
29.19 -{
29.20 - def fits_into(that: Markup_Node): Boolean =
29.21 - that.start <= this.start && this.stop <= that.stop
29.22 -}
29.23 -
29.24 -
29.25 -class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
29.26 -{
29.27 - def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
29.28 -
29.29 - private def add(branch: Markup_Tree) = // FIXME avoid sort
29.30 - set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
29.31 -
29.32 - private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
29.33 -
29.34 - def + (new_tree: Markup_Tree): Markup_Tree =
29.35 - {
29.36 - val new_node = new_tree.node
29.37 - if (new_node fits_into node) {
29.38 - var inserted = false
29.39 - val new_branches =
29.40 - branches.map(branch =>
29.41 - if ((new_node fits_into branch.node) && !inserted) {
29.42 - inserted = true
29.43 - branch + new_tree
29.44 - }
29.45 - else branch)
29.46 - if (!inserted) {
29.47 - // new_tree did not fit into children of this
29.48 - // -> insert between this and its branches
29.49 - val fitting = branches filter(_.node fits_into new_node)
29.50 - (this remove fitting) add ((new_tree /: fitting)(_ + _))
29.51 - }
29.52 - else set_branches(new_branches)
29.53 - }
29.54 - else {
29.55 - System.err.println("ignored nonfitting markup: " + new_node)
29.56 - this
29.57 - }
29.58 - }
29.59 -
29.60 - def flatten: List[Markup_Node] =
29.61 - {
29.62 - var next_x = node.start
29.63 - if (branches.isEmpty) List(this.node)
29.64 - else {
29.65 - val filled_gaps =
29.66 - for {
29.67 - child <- branches
29.68 - markups =
29.69 - if (next_x < child.node.start)
29.70 - new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
29.71 - else child.flatten
29.72 - update = (next_x = child.node.stop)
29.73 - markup <- markups
29.74 - } yield markup
29.75 - if (next_x < node.stop)
29.76 - filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
29.77 - else filled_gaps
29.78 - }
29.79 - }
29.80 -}
29.81 -
29.82 -
29.83 -class Markup_Text(val markup: List[Markup_Tree], val content: String)
29.84 -{
29.85 - private lazy val root =
29.86 - new Markup_Tree(new Markup_Node(0, content.length, None), markup)
29.87 -
29.88 - def + (new_tree: Markup_Tree): Markup_Text =
29.89 - new Markup_Text((root + new_tree).branches, content)
29.90 -
29.91 - def filter(pred: Markup_Node => Boolean): Markup_Text =
29.92 - {
29.93 - def filt(tree: Markup_Tree): List[Markup_Tree] =
29.94 - {
29.95 - val branches = tree.branches.flatMap(filt(_))
29.96 - if (pred(tree.node)) List(tree.set_branches(branches))
29.97 - else branches
29.98 - }
29.99 - new Markup_Text(markup.flatMap(filt(_)), content)
29.100 - }
29.101 -
29.102 - def flatten: List[Markup_Node] = markup.flatten(_.flatten)
29.103 -
29.104 - def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
29.105 - {
29.106 - def swing(tree: Markup_Tree): DefaultMutableTreeNode =
29.107 - {
29.108 - val node = swing_node(tree.node)
29.109 - tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
29.110 - node
29.111 - }
29.112 - swing(root)
29.113 - }
29.114 -}
30.1 --- a/src/Pure/Thy/state.scala Fri May 07 09:59:59 2010 +0200
30.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
30.3 @@ -1,117 +0,0 @@
30.4 -/*
30.5 - * Accumulating results from prover
30.6 - *
30.7 - * @author Fabian Immler, TU Munich
30.8 - * @author Makarius
30.9 - */
30.10 -
30.11 -package isabelle
30.12 -
30.13 -
30.14 -class State(
30.15 - val command: Command,
30.16 - val status: Command.Status.Value,
30.17 - val rev_results: List[XML.Tree],
30.18 - val markup_root: Markup_Text)
30.19 -{
30.20 - def this(command: Command) =
30.21 - this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
30.22 -
30.23 -
30.24 - /* content */
30.25 -
30.26 - private def set_status(st: Command.Status.Value): State =
30.27 - new State(command, st, rev_results, markup_root)
30.28 -
30.29 - private def add_result(res: XML.Tree): State =
30.30 - new State(command, status, res :: rev_results, markup_root)
30.31 -
30.32 - private def add_markup(node: Markup_Tree): State =
30.33 - new State(command, status, rev_results, markup_root + node)
30.34 -
30.35 - lazy val results = rev_results.reverse
30.36 -
30.37 -
30.38 - /* markup */
30.39 -
30.40 - lazy val highlight: Markup_Text =
30.41 - {
30.42 - markup_root.filter(_.info match {
30.43 - case Command.HighlightInfo(_) => true
30.44 - case _ => false
30.45 - })
30.46 - }
30.47 -
30.48 - private lazy val types: List[Markup_Node] =
30.49 - markup_root.filter(_.info match {
30.50 - case Command.TypeInfo(_) => true
30.51 - case _ => false }).flatten
30.52 -
30.53 - def type_at(pos: Int): Option[String] =
30.54 - {
30.55 - types.find(t => t.start <= pos && pos < t.stop) match {
30.56 - case Some(t) =>
30.57 - t.info match {
30.58 - case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
30.59 - case _ => None
30.60 - }
30.61 - case None => None
30.62 - }
30.63 - }
30.64 -
30.65 - private lazy val refs: List[Markup_Node] =
30.66 - markup_root.filter(_.info match {
30.67 - case Command.RefInfo(_, _, _, _) => true
30.68 - case _ => false }).flatten
30.69 -
30.70 - def ref_at(pos: Int): Option[Markup_Node] =
30.71 - refs.find(t => t.start <= pos && pos < t.stop)
30.72 -
30.73 -
30.74 - /* message dispatch */
30.75 -
30.76 - def + (session: Session, message: XML.Tree): State =
30.77 - {
30.78 - val changed: State =
30.79 - message match {
30.80 - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
30.81 - (this /: elems)((state, elem) =>
30.82 - elem match {
30.83 - case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
30.84 - case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
30.85 - case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
30.86 - case XML.Elem(kind, atts, body) =>
30.87 - val (begin, end) = Position.get_offsets(atts)
30.88 - if (begin.isEmpty || end.isEmpty) state
30.89 - else if (kind == Markup.ML_TYPING) {
30.90 - val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!?
30.91 - state.add_markup(
30.92 - command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
30.93 - }
30.94 - else if (kind == Markup.ML_REF) {
30.95 - body match {
30.96 - case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
30.97 - state.add_markup(command.markup_node(
30.98 - begin.get - 1, end.get - 1,
30.99 - Command.RefInfo(
30.100 - Position.get_file(atts),
30.101 - Position.get_line(atts),
30.102 - Position.get_id(atts),
30.103 - Position.get_offset(atts))))
30.104 - case _ => state
30.105 - }
30.106 - }
30.107 - else {
30.108 - state.add_markup(
30.109 - command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
30.110 - }
30.111 - case _ =>
30.112 - System.err.println("ignored status report: " + elem)
30.113 - state
30.114 - })
30.115 - case _ => add_result(message)
30.116 - }
30.117 - if (!(this eq changed)) session.command_change.event(command)
30.118 - changed
30.119 - }
30.120 -}
31.1 --- a/src/Pure/Thy/text_edit.scala Fri May 07 09:59:59 2010 +0200
31.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
31.3 @@ -1,51 +0,0 @@
31.4 -/* Title: Pure/Thy/text_edit.scala
31.5 - Author: Fabian Immler, TU Munich
31.6 - Author: Makarius
31.7 -
31.8 -Basic edits on plain text.
31.9 -*/
31.10 -
31.11 -package isabelle
31.12 -
31.13 -
31.14 -class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
31.15 -{
31.16 - override def toString =
31.17 - (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
31.18 -
31.19 -
31.20 - /* transform offsets */
31.21 -
31.22 - private def transform(do_insert: Boolean, offset: Int): Int =
31.23 - if (offset < start) offset
31.24 - else if (is_insert == do_insert) offset + text.length
31.25 - else (offset - text.length) max start
31.26 -
31.27 - def after(offset: Int): Int = transform(true, offset)
31.28 - def before(offset: Int): Int = transform(false, offset)
31.29 -
31.30 -
31.31 - /* edit strings */
31.32 -
31.33 - private def insert(index: Int, string: String): String =
31.34 - string.substring(0, index) + text + string.substring(index)
31.35 -
31.36 - private def remove(index: Int, count: Int, string: String): String =
31.37 - string.substring(0, index) + string.substring(index + count)
31.38 -
31.39 - def can_edit(string: String, shift: Int): Boolean =
31.40 - shift <= start && start < shift + string.length
31.41 -
31.42 - def edit(string: String, shift: Int): (Option[Text_Edit], String) =
31.43 - if (!can_edit(string, shift)) (Some(this), string)
31.44 - else if (is_insert) (None, insert(start - shift, string))
31.45 - else {
31.46 - val index = start - shift
31.47 - val count = text.length min (string.length - index)
31.48 - val rest =
31.49 - if (count == text.length) None
31.50 - else Some(new Text_Edit(false, start, text.substring(count)))
31.51 - (rest, remove(index, count, string))
31.52 - }
31.53 -}
31.54 -
32.1 --- a/src/Pure/build-jars Fri May 07 09:59:59 2010 +0200
32.2 +++ b/src/Pure/build-jars Fri May 07 14:47:09 2010 +0200
32.3 @@ -23,14 +23,12 @@
32.4
32.5 declare -a SOURCES=(
32.6 Concurrent/future.scala
32.7 - General/download.scala
32.8 - General/event_bus.scala
32.9 General/exn.scala
32.10 General/linear_set.scala
32.11 General/markup.scala
32.12 General/position.scala
32.13 + General/pretty.scala
32.14 General/scan.scala
32.15 - General/swing_thread.scala
32.16 General/symbol.scala
32.17 General/xml.scala
32.18 General/yxml.scala
32.19 @@ -39,7 +37,15 @@
32.20 Isar/outer_lex.scala
32.21 Isar/outer_parse.scala
32.22 Isar/outer_syntax.scala
32.23 + PIDE/change.scala
32.24 + PIDE/command.scala
32.25 + PIDE/document.scala
32.26 + PIDE/event_bus.scala
32.27 + PIDE/markup_node.scala
32.28 + PIDE/state.scala
32.29 + PIDE/text_edit.scala
32.30 System/cygwin.scala
32.31 + System/download.scala
32.32 System/gui_setup.scala
32.33 System/isabelle_process.scala
32.34 System/isabelle_syntax.scala
32.35 @@ -48,14 +54,9 @@
32.36 System/session.scala
32.37 System/session_manager.scala
32.38 System/standard_system.scala
32.39 - Thy/change.scala
32.40 - Thy/command.scala
32.41 + System/swing_thread.scala
32.42 Thy/completion.scala
32.43 - Thy/document.scala
32.44 Thy/html.scala
32.45 - Thy/markup_node.scala
32.46 - Thy/state.scala
32.47 - Thy/text_edit.scala
32.48 Thy/thy_header.scala
32.49 Thy/thy_syntax.scala
32.50 library.scala
33.1 --- a/src/Pure/library.scala Fri May 07 09:59:59 2010 +0200
33.2 +++ b/src/Pure/library.scala Fri May 07 14:47:09 2010 +0200
33.3 @@ -13,6 +13,15 @@
33.4
33.5 object Library
33.6 {
33.7 + /* separate */
33.8 +
33.9 + def separate[A](s: A, list: List[A]): List[A] =
33.10 + list match {
33.11 + case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
33.12 + case _ => list
33.13 + }
33.14 +
33.15 +
33.16 /* reverse CharSequence */
33.17
33.18 class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
33.19 @@ -38,6 +47,30 @@
33.20 }
33.21
33.22
33.23 + /* iterate over chunks (cf. space_explode/split_lines in ML) */
33.24 +
33.25 + def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
33.26 + {
33.27 + private val end = source.length
33.28 + private def next_chunk(i: Int): Option[(CharSequence, Int)] =
33.29 + {
33.30 + if (i < end) {
33.31 + var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
33.32 + Some((source.subSequence(i + 1, j), j))
33.33 + }
33.34 + else None
33.35 + }
33.36 + private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
33.37 +
33.38 + def hasNext(): Boolean = state.isDefined
33.39 + def next(): CharSequence =
33.40 + state match {
33.41 + case Some((s, i)) => { state = next_chunk(i); s }
33.42 + case None => throw new NoSuchElementException("next on empty iterator")
33.43 + }
33.44 + }
33.45 +
33.46 +
33.47 /* simple dialogs */
33.48
33.49 private def simple_dialog(kind: Int, default_title: String)