--- a/src/Pure/PIDE/document.scala Tue Aug 30 15:49:27 2011 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 30 16:04:26 2011 +0200
@@ -191,11 +191,11 @@
abstract class Snapshot
{
+ val state: State
val version: Version
val node: Node
val is_outdated: Boolean
- def find_command(id: Command_ID): Option[(String, Node, Command)]
- def state(command: Command): Command.State
+ def command_state(command: Command): Command.State
def convert(i: Text.Offset): Text.Offset
def convert(range: Text.Range): Text.Range
def revert(i: Text.Offset): Text.Offset
@@ -269,8 +269,16 @@
copy(commands = commands + (id -> command.empty_state))
}
- def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
- def lookup_exec(id: Exec_ID): Option[Command] = execs.get(id).map(_.command)
+ def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
+
+ def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
+ commands.get(id) orElse execs.get(id) match {
+ case None => None
+ case Some(st) =>
+ val command = st.command
+ version.nodes.find({ case (_, node) => node.commands(command) })
+ .map({ case (name, node) => (name, node, command) })
+ }
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename
@@ -367,19 +375,12 @@
new Snapshot
{
+ val state = State.this
val version = stable.version.get_finished
val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
- def find_command(id: ID): Option[(String, Node, Command)] =
- State.this.lookup_command(id) orElse State.this.lookup_exec(id) match {
- case None => None
- case Some(command) =>
- version.nodes.find({ case (_, node) => node.commands(command) })
- .map({ case (name, node) => (name, node, command) })
- }
-
- def state(command: Command): Command.State =
+ def command_state(command: Command): Command.State =
try {
the_exec(the_assignment(version).check_finished.command_execs
.getOrElse(command.id, fail))
@@ -397,7 +398,7 @@
val former_range = revert(range)
for {
(command, command_start) <- node.command_range(former_range).toStream
- Text.Info(r0, x) <- state(command).markup.
+ Text.Info(r0, x) <- command_state(command).markup.
select((former_range - command_start).restrict(command.range)) {
case Text.Info(r0, info)
if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
--- a/src/Pure/System/session.scala Tue Aug 30 15:49:27 2011 +0200
+++ b/src/Pure/System/session.scala Tue Aug 30 16:04:26 2011 +0200
@@ -243,7 +243,7 @@
def id_command(command: Command)
{
- if (global_state().lookup_command(command.id).isEmpty) {
+ if (!global_state().defined_command(command.id)) {
global_state.change(_.define_command(command))
prover.get.define_command(command.id, Symbol.encode(command.source))
}
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Aug 30 15:49:27 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Aug 30 16:04:26 2011 +0200
@@ -73,7 +73,7 @@
case _ if !snapshot.is_outdated =>
(props, props) match {
case (Position.Id(def_id), Position.Offset(def_offset)) =>
- snapshot.find_command(def_id) match {
+ snapshot.state.find_command(snapshot.version, def_id) match {
case Some((def_name, def_node, def_cmd)) =>
def_node.command_start(def_cmd) match {
case Some(def_cmd_start) =>
--- a/src/Tools/jEdit/src/isabelle_markup.scala Tue Aug 30 15:49:27 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Aug 30 16:04:26 2011 +0200
@@ -52,7 +52,7 @@
def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
{
- val state = snapshot.state(command)
+ val state = snapshot.command_state(command)
if (snapshot.is_outdated) Some(outdated_color)
else
Isar_Document.command_status(state.status) match {
@@ -64,7 +64,7 @@
def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
{
- val state = snapshot.state(command)
+ val state = snapshot.command_state(command)
if (snapshot.is_outdated) None
else
Isar_Document.command_status(state.status) match {
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 30 15:49:27 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 30 16:04:26 2011 +0200
@@ -152,7 +152,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
+ snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
--- a/src/Tools/jEdit/src/output_dockable.scala Tue Aug 30 15:49:27 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Aug 30 16:04:26 2011 +0200
@@ -86,7 +86,7 @@
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
val snapshot = doc_view.update_snapshot()
val filtered_results =
- snapshot.state(cmd).results.iterator.map(_._2) filter {
+ snapshot.command_state(cmd).results.iterator.map(_._2) filter {
case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable
case _ => true
}