1.1 --- a/src/Pure/PIDE/document.scala Tue Aug 30 15:49:27 2011 +0200
1.2 +++ b/src/Pure/PIDE/document.scala Tue Aug 30 16:04:26 2011 +0200
1.3 @@ -191,11 +191,11 @@
1.4
1.5 abstract class Snapshot
1.6 {
1.7 + val state: State
1.8 val version: Version
1.9 val node: Node
1.10 val is_outdated: Boolean
1.11 - def find_command(id: Command_ID): Option[(String, Node, Command)]
1.12 - def state(command: Command): Command.State
1.13 + def command_state(command: Command): Command.State
1.14 def convert(i: Text.Offset): Text.Offset
1.15 def convert(range: Text.Range): Text.Range
1.16 def revert(i: Text.Offset): Text.Offset
1.17 @@ -269,8 +269,16 @@
1.18 copy(commands = commands + (id -> command.empty_state))
1.19 }
1.20
1.21 - def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
1.22 - def lookup_exec(id: Exec_ID): Option[Command] = execs.get(id).map(_.command)
1.23 + def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
1.24 +
1.25 + def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
1.26 + commands.get(id) orElse execs.get(id) match {
1.27 + case None => None
1.28 + case Some(st) =>
1.29 + val command = st.command
1.30 + version.nodes.find({ case (_, node) => node.commands(command) })
1.31 + .map({ case (name, node) => (name, node, command) })
1.32 + }
1.33
1.34 def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
1.35 def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename
1.36 @@ -367,19 +375,12 @@
1.37
1.38 new Snapshot
1.39 {
1.40 + val state = State.this
1.41 val version = stable.version.get_finished
1.42 val node = version.nodes(name)
1.43 val is_outdated = !(pending_edits.isEmpty && latest == stable)
1.44
1.45 - def find_command(id: ID): Option[(String, Node, Command)] =
1.46 - State.this.lookup_command(id) orElse State.this.lookup_exec(id) match {
1.47 - case None => None
1.48 - case Some(command) =>
1.49 - version.nodes.find({ case (_, node) => node.commands(command) })
1.50 - .map({ case (name, node) => (name, node, command) })
1.51 - }
1.52 -
1.53 - def state(command: Command): Command.State =
1.54 + def command_state(command: Command): Command.State =
1.55 try {
1.56 the_exec(the_assignment(version).check_finished.command_execs
1.57 .getOrElse(command.id, fail))
1.58 @@ -397,7 +398,7 @@
1.59 val former_range = revert(range)
1.60 for {
1.61 (command, command_start) <- node.command_range(former_range).toStream
1.62 - Text.Info(r0, x) <- state(command).markup.
1.63 + Text.Info(r0, x) <- command_state(command).markup.
1.64 select((former_range - command_start).restrict(command.range)) {
1.65 case Text.Info(r0, info)
1.66 if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
2.1 --- a/src/Pure/System/session.scala Tue Aug 30 15:49:27 2011 +0200
2.2 +++ b/src/Pure/System/session.scala Tue Aug 30 16:04:26 2011 +0200
2.3 @@ -243,7 +243,7 @@
2.4
2.5 def id_command(command: Command)
2.6 {
2.7 - if (global_state().lookup_command(command.id).isEmpty) {
2.8 + if (!global_state().defined_command(command.id)) {
2.9 global_state.change(_.define_command(command))
2.10 prover.get.define_command(command.id, Symbol.encode(command.source))
2.11 }
3.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Aug 30 15:49:27 2011 +0200
3.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Aug 30 16:04:26 2011 +0200
3.3 @@ -73,7 +73,7 @@
3.4 case _ if !snapshot.is_outdated =>
3.5 (props, props) match {
3.6 case (Position.Id(def_id), Position.Offset(def_offset)) =>
3.7 - snapshot.find_command(def_id) match {
3.8 + snapshot.state.find_command(snapshot.version, def_id) match {
3.9 case Some((def_name, def_node, def_cmd)) =>
3.10 def_node.command_start(def_cmd) match {
3.11 case Some(def_cmd_start) =>
4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala Tue Aug 30 15:49:27 2011 +0200
4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Aug 30 16:04:26 2011 +0200
4.3 @@ -52,7 +52,7 @@
4.4
4.5 def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
4.6 {
4.7 - val state = snapshot.state(command)
4.8 + val state = snapshot.command_state(command)
4.9 if (snapshot.is_outdated) Some(outdated_color)
4.10 else
4.11 Isar_Document.command_status(state.status) match {
4.12 @@ -64,7 +64,7 @@
4.13
4.14 def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
4.15 {
4.16 - val state = snapshot.state(command)
4.17 + val state = snapshot.command_state(command)
4.18 if (snapshot.is_outdated) None
4.19 else
4.20 Isar_Document.command_status(state.status) match {
5.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 30 15:49:27 2011 +0200
5.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 30 16:04:26 2011 +0200
5.3 @@ -152,7 +152,7 @@
5.4 val root = data.root
5.5 val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
5.6 for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
5.7 - snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
5.8 + snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
5.9 {
5.10 val range = info.range + command_start
5.11 val content = command.source(info.range).replace('\n', ' ')
6.1 --- a/src/Tools/jEdit/src/output_dockable.scala Tue Aug 30 15:49:27 2011 +0200
6.2 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Aug 30 16:04:26 2011 +0200
6.3 @@ -86,7 +86,7 @@
6.4 case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
6.5 val snapshot = doc_view.update_snapshot()
6.6 val filtered_results =
6.7 - snapshot.state(cmd).results.iterator.map(_._2) filter {
6.8 + snapshot.command_state(cmd).results.iterator.map(_._2) filter {
6.9 case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable
6.10 case _ => true
6.11 }