--- a/src/Pure/PIDE/command.scala Thu Aug 12 13:49:08 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 12 13:59:18 2010 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/PIDE/command.scala
- Author: Johannes Hölzl, TU Munich
Author: Fabian Immler, TU Munich
Author: Makarius
@@ -29,8 +28,128 @@
case class TypeInfo(ty: String)
case class RefInfo(file: Option[String], line: Option[Int],
command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. State_ID !?
+
+
+ /** accumulated results from prover **/
+
+ class State(
+ val command: Command,
+ val status: Command.Status.Value,
+ val forks: Int,
+ val reverse_results: List[XML.Tree],
+ val markup_root: Markup_Text)
+ {
+ def this(command: Command) =
+ this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
+
+
+ /* content */
+
+ private def set_status(st: Command.Status.Value): State =
+ new State(command, st, forks, reverse_results, markup_root)
+
+ private def add_forks(i: Int): State =
+ new State(command, status, forks + i, reverse_results, markup_root)
+
+ private def add_result(res: XML.Tree): State =
+ new State(command, status, forks, res :: reverse_results, markup_root)
+
+ private def add_markup(node: Markup_Tree): State =
+ new State(command, status, forks, reverse_results, markup_root + node)
+
+ lazy val results = reverse_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 accumulate(message: XML.Tree): Command.State =
+ message match {
+ case XML.Elem(Markup(Markup.STATUS, _), elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
+ case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
+ case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
+ case _ => System.err.println("Ignored status message: " + elem); state
+ })
+
+ case XML.Elem(Markup(Markup.REPORT, _), elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
+ atts match {
+ case Position.Range(begin, end) =>
+ if (kind == Markup.ML_TYPING) {
+ val info = Pretty.string_of(body, margin = 40)
+ 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(Markup.ML_DEF, props), _)) =>
+ state.add_markup(command.markup_node(
+ begin - 1, end - 1,
+ Command.RefInfo(
+ Position.get_file(props),
+ Position.get_line(props),
+ Position.get_id(props),
+ Position.get_offset(props))))
+ case _ => state
+ }
+ }
+ else {
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1,
+ Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
+ }
+ case _ => state
+ }
+ case _ => System.err.println("Ignored report message: " + elem); state
+ })
+ case _ => add_result(message)
+ }
+ }
}
+
class Command(
val id: Document.Command_ID,
val span: Thy_Syntax.Span,
@@ -59,8 +178,8 @@
/* accumulated messages */
- @volatile protected var state = new State(this)
- def current_state: State = state
+ @volatile protected var state = new Command.State(this)
+ def current_state: Command.State = state
private case class Consume(message: XML.Tree, forward: Command => Unit)
private case object Assign
--- a/src/Pure/PIDE/document.scala Thu Aug 12 13:49:08 2010 +0200
+++ b/src/Pure/PIDE/document.scala Thu Aug 12 13:59:18 2010 +0200
@@ -101,7 +101,7 @@
val is_outdated: Boolean
def convert(offset: Int): Int
def revert(offset: Int): Int
- def state(command: Command): State
+ def state(command: Command): Command.State
}
object Change
@@ -146,7 +146,7 @@
val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- def state(command: Command): State = document.current_state(command)
+ def state(command: Command): Command.State = document.current_state(command)
}
}
}
@@ -281,12 +281,12 @@
tmp_states = Map()
}
- def current_state(cmd: Command): State =
+ def current_state(cmd: Command): Command.State =
{
require(assignment.is_finished)
(assignment.join).get(cmd) match {
case Some(cmd_state) => cmd_state.current_state
- case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
+ case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
}
}
}
--- a/src/Pure/PIDE/state.scala Thu Aug 12 13:49:08 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-/* Title: Pure/PIDE/state.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Accumulated results from prover.
-*/
-
-package isabelle
-
-
-class State(
- val command: Command,
- val status: Command.Status.Value,
- val forks: Int,
- val reverse_results: List[XML.Tree],
- val markup_root: Markup_Text)
-{
- def this(command: Command) =
- this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
-
-
- /* content */
-
- private def set_status(st: Command.Status.Value): State =
- new State(command, st, forks, reverse_results, markup_root)
-
- private def add_forks(i: Int): State =
- new State(command, status, forks + i, reverse_results, markup_root)
-
- private def add_result(res: XML.Tree): State =
- new State(command, status, forks, res :: reverse_results, markup_root)
-
- private def add_markup(node: Markup_Tree): State =
- new State(command, status, forks, reverse_results, markup_root + node)
-
- lazy val results = reverse_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 accumulate(message: XML.Tree): State =
- message match {
- case XML.Elem(Markup(Markup.STATUS, _), elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
- case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
- case _ => System.err.println("Ignored status message: " + elem); state
- })
-
- case XML.Elem(Markup(Markup.REPORT, _), elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
- atts match {
- case Position.Range(begin, end) =>
- if (kind == Markup.ML_TYPING) {
- val info = Pretty.string_of(body, margin = 40)
- 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(Markup.ML_DEF, props), _)) =>
- state.add_markup(command.markup_node(
- begin - 1, end - 1,
- Command.RefInfo(
- Position.get_file(props),
- Position.get_line(props),
- Position.get_id(props),
- Position.get_offset(props))))
- case _ => state
- }
- }
- else {
- state.add_markup(
- command.markup_node(begin - 1, end - 1,
- Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
- }
- case _ => state
- }
- case _ => System.err.println("Ignored report message: " + elem); state
- })
- case _ => add_result(message)
- }
-}
--- a/src/Pure/build-jars Thu Aug 12 13:49:08 2010 +0200
+++ b/src/Pure/build-jars Thu Aug 12 13:59:18 2010 +0200
@@ -42,7 +42,6 @@
PIDE/document.scala
PIDE/event_bus.scala
PIDE/markup_node.scala
- PIDE/state.scala
PIDE/text_edit.scala
System/cygwin.scala
System/download.scala