back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
authorwenzelm
Thu Nov 21 21:55:29 2013 +0100 (2013-11-21)
changeset 54640bbd2fa353809
parent 54639 5adc68deb322
child 54641 50169ef2cca3
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);
src/Pure/PIDE/query_operation.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Wed Nov 20 23:00:18 2013 +0100
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Thu Nov 21 21:55:29 2013 +0100
     1.3 @@ -18,7 +18,6 @@
     1.4      val WAITING = Value("waiting")
     1.5      val RUNNING = Value("running")
     1.6      val FINISHED = Value("finished")
     1.7 -    val REMOVED = Value("removed")
     1.8    }
     1.9  }
    1.10  
    1.11 @@ -38,7 +37,7 @@
    1.12    private var current_query: List[String] = Nil
    1.13    private var current_update_pending = false
    1.14    private var current_output: List[XML.Tree] = Nil
    1.15 -  private var current_status = Query_Operation.Status.REMOVED
    1.16 +  private var current_status = Query_Operation.Status.FINISHED
    1.17    private var current_exec_id = Document_ID.none
    1.18  
    1.19    private def reset_state()
    1.20 @@ -47,7 +46,7 @@
    1.21      current_query = Nil
    1.22      current_update_pending = false
    1.23      current_output = Nil
    1.24 -    current_status = Query_Operation.Status.REMOVED
    1.25 +    current_status = Query_Operation.Status.FINISHED
    1.26      current_exec_id = Document_ID.none
    1.27    }
    1.28  
    1.29 @@ -89,13 +88,40 @@
    1.30        } yield elem).toList
    1.31  
    1.32  
    1.33 +    /* resolve sendback: static command id */
    1.34 +
    1.35 +    def resolve_sendback(body: XML.Body): XML.Body =
    1.36 +    {
    1.37 +      current_location match {
    1.38 +        case None => body
    1.39 +        case Some(command) =>
    1.40 +          def resolve(body: XML.Body): XML.Body =
    1.41 +            body map {
    1.42 +              case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
    1.43 +              case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
    1.44 +                val props1 =
    1.45 +                  props.map({
    1.46 +                    case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
    1.47 +                      (Markup.ID, Properties.Value.Long(command.id))
    1.48 +                    case p => p
    1.49 +                  })
    1.50 +                XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
    1.51 +              case XML.Elem(m, b) => XML.Elem(m, resolve(b))
    1.52 +              case t => t
    1.53 +            }
    1.54 +          resolve(body)
    1.55 +      }
    1.56 +    }
    1.57 +
    1.58 +
    1.59      /* output */
    1.60  
    1.61      val new_output =
    1.62        for {
    1.63          XML.Elem(_, List(XML.Elem(markup, body))) <- results
    1.64          if Markup.messages.contains(markup.name)
    1.65 -      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
    1.66 +        body1 = resolve_sendback(body)
    1.67 +      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
    1.68  
    1.69  
    1.70      /* status */
    1.71 @@ -105,7 +131,7 @@
    1.72        results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
    1.73  
    1.74      val new_status =
    1.75 -      if (removed) Query_Operation.Status.REMOVED
    1.76 +      if (removed) Query_Operation.Status.FINISHED
    1.77        else
    1.78          get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
    1.79          get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
    1.80 @@ -133,7 +159,7 @@
    1.81          if (current_status != new_status) {
    1.82            current_status = new_status
    1.83            consume_status(new_status)
    1.84 -          if (new_status == Query_Operation.Status.REMOVED)
    1.85 +          if (new_status == Query_Operation.Status.FINISHED)
    1.86              remove_overlay()
    1.87          }
    1.88        }
    1.89 @@ -192,7 +218,7 @@
    1.90            current_location match {
    1.91              case Some(command)
    1.92              if current_update_pending ||
    1.93 -              (current_status != Query_Operation.Status.REMOVED &&
    1.94 +              (current_status != Query_Operation.Status.FINISHED &&
    1.95                  changed.commands.contains(command)) =>
    1.96                Swing_Thread.later { content_update() }
    1.97              case _ =>
     2.1 --- a/src/Tools/jEdit/src/active.scala	Wed Nov 20 23:00:18 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/active.scala	Thu Nov 21 21:55:29 2013 +0100
     2.3 @@ -52,9 +52,9 @@
     2.4  
     2.5                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
     2.6                  props match {
     2.7 -                  case Position.Id(exec_id) =>
     2.8 +                  case Position.Id(id) =>
     2.9                      Isabelle.edit_command(snapshot, buffer,
    2.10 -                      props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
    2.11 +                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
    2.12                    case _ =>
    2.13                      if (props.exists(_ == Markup.PADDING_LINE))
    2.14                        Isabelle.insert_line_padding(text_area, text)
     3.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Wed Nov 20 23:00:18 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Thu Nov 21 21:55:29 2013 +0100
     3.3 @@ -37,7 +37,7 @@
     3.4          process_indicator.update("Waiting for evaluation of context ...", 5)
     3.5        case Query_Operation.Status.RUNNING =>
     3.6          process_indicator.update("Running find operation ...", 15)
     3.7 -      case _ =>
     3.8 +      case Query_Operation.Status.FINISHED =>
     3.9          process_indicator.update(null, 0)
    3.10      }
    3.11    }
     4.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Nov 20 23:00:18 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Thu Nov 21 21:55:29 2013 +0100
     4.3 @@ -177,26 +177,28 @@
     4.4      snapshot: Document.Snapshot,
     4.5      buffer: Buffer,
     4.6      padding: Boolean,
     4.7 -    exec_id: Document_ID.Exec,
     4.8 +    id: Document_ID.Generic,
     4.9      s: String)
    4.10    {
    4.11 -    snapshot.state.execs.get(exec_id).map(_.command) match {
    4.12 -      case Some(command) =>
    4.13 -        snapshot.node.command_start(command) match {
    4.14 -          case Some(start) =>
    4.15 -            JEdit_Lib.buffer_edit(buffer) {
    4.16 -              val range = command.proper_range + start
    4.17 -              if (padding) {
    4.18 -                buffer.insert(start + range.length, "\n" + s)
    4.19 +    if (!snapshot.is_outdated) {
    4.20 +      snapshot.state.find_command(snapshot.version, id) match {
    4.21 +        case Some((node, command)) =>
    4.22 +          node.command_start(command) match {
    4.23 +            case Some(start) =>
    4.24 +              JEdit_Lib.buffer_edit(buffer) {
    4.25 +                val range = command.proper_range + start
    4.26 +                if (padding) {
    4.27 +                  buffer.insert(start + range.length, "\n" + s)
    4.28 +                }
    4.29 +                else {
    4.30 +                  buffer.remove(start, range.length)
    4.31 +                  buffer.insert(start, s)
    4.32 +                }
    4.33                }
    4.34 -              else {
    4.35 -                buffer.remove(start, range.length)
    4.36 -                buffer.insert(start, s)
    4.37 -              }
    4.38 -            }
    4.39 -          case None =>
    4.40 -        }
    4.41 -      case None =>
    4.42 +            case None =>
    4.43 +          }
    4.44 +        case None =>
    4.45 +      }
    4.46      }
    4.47    }
    4.48  
     5.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Nov 20 23:00:18 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Nov 21 21:55:29 2013 +0100
     5.3 @@ -38,7 +38,7 @@
     5.4          process_indicator.update("Waiting for evaluation of context ...", 5)
     5.5        case Query_Operation.Status.RUNNING =>
     5.6          process_indicator.update("Sledgehammering ...", 15)
     5.7 -      case _ =>
     5.8 +      case Query_Operation.Status.FINISHED =>
     5.9          process_indicator.update(null, 0)
    5.10      }
    5.11    }