tuned signature;
authorwenzelm
Tue Aug 30 16:04:26 2011 +0200 (2011-08-30)
changeset 44582479c07072992
parent 44581 7daef43592d0
child 44583 022509c908fb
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/output_dockable.scala
     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                  }