# HG changeset patch # User wenzelm # Date 1314713066 -7200 # Node ID 479c070729921b5bf6c7d7284dad71cb4671633d # Parent 7daef43592d02271c61915d16829be17a947a308 tuned signature; diff -r 7daef43592d0 -r 479c07072992 src/Pure/PIDE/document.scala --- 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)) => diff -r 7daef43592d0 -r 479c07072992 src/Pure/System/session.scala --- 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)) } diff -r 7daef43592d0 -r 479c07072992 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- 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) => diff -r 7daef43592d0 -r 479c07072992 src/Tools/jEdit/src/isabelle_markup.scala --- 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 { diff -r 7daef43592d0 -r 479c07072992 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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', ' ') diff -r 7daef43592d0 -r 479c07072992 src/Tools/jEdit/src/output_dockable.scala --- 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 }