clarified Document.Blobs environment vs. actual edits of auxiliary files;
authorwenzelm
Tue Nov 19 20:53:43 2013 +0100 (2013-11-19)
changeset 54521744ea0025e11
parent 54520 cee77d2e9582
child 54522 761be40990f1
clarified Document.Blobs environment vs. actual edits of auxiliary files;
more robust handling of vacuous edits;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Nov 19 19:43:26 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Nov 19 20:53:43 2013 +0100
     1.3 @@ -47,6 +47,8 @@
     1.4    type Edit_Text = Edit[Text.Edit, Text.Perspective]
     1.5    type Edit_Command = Edit[Command.Edit, Command.Perspective]
     1.6  
     1.7 +  type Blobs = Map[Node.Name, Bytes]
     1.8 +
     1.9    object Node
    1.10    {
    1.11      val empty: Node = new Node()
    1.12 @@ -125,7 +127,7 @@
    1.13      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    1.14      case class Deps[A, B](header: Header) extends Edit[A, B]
    1.15      case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
    1.16 -    case class Blob[A, B](blob: Bytes) extends Edit[A, B]
    1.17 +    case class Blob[A, B]() extends Edit[A, B]
    1.18      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    1.19      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    1.20  
     2.1 --- a/src/Pure/System/session.scala	Tue Nov 19 19:43:26 2013 +0100
     2.2 +++ b/src/Pure/System/session.scala	Tue Nov 19 20:53:43 2013 +0100
     2.3 @@ -25,7 +25,7 @@
     2.4    case class Statistics(props: Properties.T)
     2.5    case class Global_Options(options: Options)
     2.6    case object Caret_Focus
     2.7 -  case class Raw_Edits(edits: List[Document.Edit_Text])
     2.8 +  case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     2.9    case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
    2.10    case class Commands_Changed(
    2.11      assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    2.12 @@ -167,6 +167,7 @@
    2.13    //{{{
    2.14    private case class Text_Edits(
    2.15      previous: Future[Document.Version],
    2.16 +    doc_blobs: Document.Blobs,
    2.17      text_edits: List[Document.Edit_Text],
    2.18      version_result: Promise[Document.Version])
    2.19  
    2.20 @@ -177,14 +178,14 @@
    2.21        receive {
    2.22          case Stop => finished = true; reply(())
    2.23  
    2.24 -        case Text_Edits(previous, text_edits, version_result) =>
    2.25 +        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    2.26            val prev = previous.get_finished
    2.27 -          val (all_blobs, doc_edits, version) =
    2.28 +          val (doc_edits, version) =
    2.29              Timing.timeit("Thy_Load.text_edits", timing) {
    2.30 -              thy_load.text_edits(reparse_limit, prev, text_edits)
    2.31 +              thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
    2.32              }
    2.33            version_result.fulfill(version)
    2.34 -          sender ! Change(all_blobs, doc_edits, prev, version)
    2.35 +          sender ! Change(doc_blobs, doc_edits, prev, version)
    2.36  
    2.37          case bad => System.err.println("change_parser: ignoring bad message " + bad)
    2.38        }
    2.39 @@ -250,7 +251,7 @@
    2.40    private case class Start(args: List[String])
    2.41    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    2.42    private case class Change(
    2.43 -    all_blobs: Map[Document.Node.Name, Bytes],
    2.44 +    doc_blobs: Document.Blobs,
    2.45      doc_edits: List[Document.Edit_Command],
    2.46      previous: Document.Version,
    2.47      version: Document.Version)
    2.48 @@ -349,7 +350,7 @@
    2.49  
    2.50      /* raw edits */
    2.51  
    2.52 -    def handle_raw_edits(edits: List[Document.Edit_Text])
    2.53 +    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
    2.54      //{{{
    2.55      {
    2.56        prover.get.discontinue_execution()
    2.57 @@ -358,8 +359,8 @@
    2.58        val version = Future.promise[Document.Version]
    2.59        val change = global_state >>> (_.continue_history(previous, edits, version))
    2.60  
    2.61 -      raw_edits.event(Session.Raw_Edits(edits))
    2.62 -      change_parser ! Text_Edits(previous, edits, version)
    2.63 +      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
    2.64 +      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
    2.65      }
    2.66      //}}}
    2.67  
    2.68 @@ -379,7 +380,7 @@
    2.69            digest <- command.blobs_digests
    2.70            if !global_state().defined_blob(digest)
    2.71          } {
    2.72 -          change.all_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    2.73 +          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    2.74              case Some(blob) =>
    2.75                global_state >> (_.define_blob(digest))
    2.76                prover.get.define_blob(blob)
    2.77 @@ -523,7 +524,7 @@
    2.78          case Update_Options(options) if prover.isDefined =>
    2.79            if (is_ready) {
    2.80              prover.get.options(options)
    2.81 -            handle_raw_edits(Nil)
    2.82 +            handle_raw_edits(Map.empty, Nil)
    2.83            }
    2.84            global_options.event(Session.Global_Options(options))
    2.85            reply(())
    2.86 @@ -531,8 +532,8 @@
    2.87          case Cancel_Exec(exec_id) if prover.isDefined =>
    2.88            prover.get.cancel_exec(exec_id)
    2.89  
    2.90 -        case Session.Raw_Edits(edits) if prover.isDefined =>
    2.91 -          handle_raw_edits(edits)
    2.92 +        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
    2.93 +          handle_raw_edits(doc_blobs, edits)
    2.94            reply(())
    2.95  
    2.96          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
    2.97 @@ -585,8 +586,8 @@
    2.98  
    2.99    def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
   2.100  
   2.101 -  def update(edits: List[Document.Edit_Text])
   2.102 -  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
   2.103 +  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   2.104 +  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
   2.105  
   2.106    def update_options(options: Options)
   2.107    { session_actor !? Update_Options(options) }
     3.1 --- a/src/Pure/Thy/thy_load.scala	Tue Nov 19 19:43:26 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Nov 19 20:53:43 2013 +0100
     3.3 @@ -99,8 +99,11 @@
     3.4  
     3.5    /* theory text edits */
     3.6  
     3.7 -  def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
     3.8 -      : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) =
     3.9 -    Thy_Syntax.text_edits(this, reparse_limit, previous, edits)
    3.10 +  def text_edits(
    3.11 +    reparse_limit: Int,
    3.12 +    previous: Document.Version,
    3.13 +    doc_blobs: Document.Blobs,
    3.14 +    edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
    3.15 +    Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
    3.16  }
    3.17  
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 19:43:26 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 20:53:43 2013 +0100
     4.3 @@ -256,14 +256,14 @@
     4.4        syntax: Outer_Syntax,
     4.5        node_name: Document.Node.Name,
     4.6        span: List[Token],
     4.7 -      all_blobs: Map[Document.Node.Name, Bytes])
     4.8 +      doc_blobs: Document.Blobs)
     4.9      : List[Command.Blob] =
    4.10    {
    4.11      span_files(syntax, span).map(file =>
    4.12        Exn.capture {
    4.13          val name =
    4.14            Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
    4.15 -        all_blobs.get(name) match {
    4.16 +        doc_blobs.get(name) match {
    4.17            case Some(blob) => (name, blob.sha1_digest)
    4.18            case None => error("No such file: " + quote(name.toString))
    4.19          }
    4.20 @@ -286,7 +286,7 @@
    4.21    private def reparse_spans(
    4.22      thy_load: Thy_Load,
    4.23      syntax: Outer_Syntax,
    4.24 -    all_blobs: Map[Document.Node.Name, Bytes],
    4.25 +    doc_blobs: Document.Blobs,
    4.26      name: Document.Node.Name,
    4.27      commands: Linear_Set[Command],
    4.28      first: Command, last: Command): Linear_Set[Command] =
    4.29 @@ -294,7 +294,7 @@
    4.30      val cmds0 = commands.iterator(first, last).toList
    4.31      val spans0 =
    4.32        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    4.33 -        map(span => (resolve_files(thy_load, syntax, name, span, all_blobs), span))
    4.34 +        map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
    4.35  
    4.36      val (cmds1, spans1) = chop_common(cmds0, spans0)
    4.37  
    4.38 @@ -321,7 +321,7 @@
    4.39    private def recover_spans(
    4.40      thy_load: Thy_Load,
    4.41      syntax: Outer_Syntax,
    4.42 -    all_blobs: Map[Document.Node.Name, Bytes],
    4.43 +    doc_blobs: Document.Blobs,
    4.44      name: Document.Node.Name,
    4.45      perspective: Command.Perspective,
    4.46      commands: Linear_Set[Command]): Linear_Set[Command] =
    4.47 @@ -337,7 +337,7 @@
    4.48          case Some(first_unparsed) =>
    4.49            val first = next_invisible_command(cmds.reverse, first_unparsed)
    4.50            val last = next_invisible_command(cmds, first_unparsed)
    4.51 -          recover(reparse_spans(thy_load, syntax, all_blobs, name, cmds, first, last))
    4.52 +          recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last))
    4.53          case None => cmds
    4.54        }
    4.55      recover(commands)
    4.56 @@ -349,7 +349,7 @@
    4.57    private def consolidate_spans(
    4.58      thy_load: Thy_Load,
    4.59      syntax: Outer_Syntax,
    4.60 -    all_blobs: Map[Document.Node.Name, Bytes],
    4.61 +    doc_blobs: Document.Blobs,
    4.62      reparse_limit: Int,
    4.63      name: Document.Node.Name,
    4.64      perspective: Command.Perspective,
    4.65 @@ -369,7 +369,7 @@
    4.66                  last = it.next
    4.67                  i += last.length
    4.68                }
    4.69 -              reparse_spans(thy_load, syntax, all_blobs, name, commands, first_unfinished, last)
    4.70 +              reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last)
    4.71              case None => commands
    4.72            }
    4.73          case None => commands
    4.74 @@ -393,7 +393,7 @@
    4.75    private def text_edit(
    4.76      thy_load: Thy_Load,
    4.77      syntax: Outer_Syntax,
    4.78 -    all_blobs: Map[Document.Node.Name, Bytes],
    4.79 +    doc_blobs: Document.Blobs,
    4.80      reparse_limit: Int,
    4.81      node: Document.Node, edit: Document.Edit_Text): Document.Node =
    4.82    {
    4.83 @@ -404,7 +404,7 @@
    4.84          val commands0 = node.commands
    4.85          val commands1 = edit_text(text_edits, commands0)
    4.86          val commands2 =
    4.87 -          recover_spans(thy_load, syntax, all_blobs, name, node.perspective.visible, commands1)
    4.88 +          recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
    4.89          node.update_commands(commands2)
    4.90  
    4.91        case (_, Document.Node.Deps(_)) => node
    4.92 @@ -416,10 +416,10 @@
    4.93          if (node.same_perspective(perspective)) node
    4.94          else
    4.95            node.update_perspective(perspective).update_commands(
    4.96 -            consolidate_spans(thy_load, syntax, all_blobs, reparse_limit,
    4.97 +            consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
    4.98                name, visible, node.commands))
    4.99  
   4.100 -      case (_, Document.Node.Blob(_)) => node
   4.101 +      case (_, Document.Node.Blob()) => node
   4.102      }
   4.103    }
   4.104  
   4.105 @@ -427,56 +427,53 @@
   4.106        thy_load: Thy_Load,
   4.107        reparse_limit: Int,
   4.108        previous: Document.Version,
   4.109 +      doc_blobs: Document.Blobs,
   4.110        edits: List[Document.Edit_Text])
   4.111 -    : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) =
   4.112 +    : (List[Document.Edit_Command], Document.Version) =
   4.113    {
   4.114      val (syntax, reparse0, nodes0, doc_edits0) =
   4.115        header_edits(thy_load.base_syntax, previous, edits)
   4.116  
   4.117 -    val reparse =
   4.118 -      (reparse0 /: nodes0.entries)({
   4.119 -        case (reparse, (name, node)) =>
   4.120 -          if (node.thy_load_commands.isEmpty) reparse
   4.121 -          else name :: reparse
   4.122 -        })
   4.123 -    val reparse_set = reparse.toSet
   4.124 +    if (edits.isEmpty)
   4.125 +      (Nil, Document.Version.make(syntax, previous.nodes))
   4.126 +    else {
   4.127 +      val reparse =
   4.128 +        (reparse0 /: nodes0.entries)({
   4.129 +          case (reparse, (name, node)) =>
   4.130 +            if (node.thy_load_commands.isEmpty) reparse
   4.131 +            else name :: reparse
   4.132 +          })
   4.133 +      val reparse_set = reparse.toSet
   4.134  
   4.135 -    var nodes = nodes0
   4.136 -    val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
   4.137 +      var nodes = nodes0
   4.138 +      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
   4.139 +
   4.140 +      val node_edits =
   4.141 +        (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
   4.142 +          .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   4.143  
   4.144 -    val node_edits =
   4.145 -      (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
   4.146 -        .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   4.147 +      node_edits foreach {
   4.148 +        case (name, edits) =>
   4.149 +          val node = nodes(name)
   4.150 +          val commands = node.commands
   4.151  
   4.152 -    val all_blobs: Map[Document.Node.Name, Bytes] =
   4.153 -      (Map.empty[Document.Node.Name, Bytes] /: node_edits) {
   4.154 -        case (bs1, (_, es)) => (bs1 /: es) {
   4.155 -          case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob)
   4.156 -          case (bs, _) => bs
   4.157 -        }
   4.158 +          val node1 =
   4.159 +            if (reparse_set(name) && !commands.isEmpty)
   4.160 +              node.update_commands(
   4.161 +                reparse_spans(thy_load, syntax, doc_blobs,
   4.162 +                  name, commands, commands.head, commands.last))
   4.163 +            else node
   4.164 +          val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _))
   4.165 +
   4.166 +          if (!(node.same_perspective(node2.perspective)))
   4.167 +            doc_edits += (name -> node2.perspective)
   4.168 +
   4.169 +          doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   4.170 +
   4.171 +          nodes += (name -> node2)
   4.172        }
   4.173  
   4.174 -    node_edits foreach {
   4.175 -      case (name, edits) =>
   4.176 -        val node = nodes(name)
   4.177 -        val commands = node.commands
   4.178 -
   4.179 -        val node1 =
   4.180 -          if (reparse_set(name) && !commands.isEmpty)
   4.181 -            node.update_commands(
   4.182 -              reparse_spans(thy_load, syntax, all_blobs,
   4.183 -                name, commands, commands.head, commands.last))
   4.184 -          else node
   4.185 -        val node2 = (node1 /: edits)(text_edit(thy_load, syntax, all_blobs, reparse_limit, _, _))
   4.186 -
   4.187 -        if (!(node.same_perspective(node2.perspective)))
   4.188 -          doc_edits += (name -> node2.perspective)
   4.189 -
   4.190 -        doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
   4.191 -
   4.192 -        nodes += (name -> node2)
   4.193 +      (doc_edits.toList, Document.Version.make(syntax, nodes))
   4.194      }
   4.195 -
   4.196 -    (all_blobs, doc_edits.toList, Document.Version.make(syntax, nodes))
   4.197    }
   4.198  }
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Nov 19 19:43:26 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Nov 19 20:53:43 2013 +0100
     5.3 @@ -148,7 +148,7 @@
     5.4          node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
     5.5          node_name -> perspective)
     5.6      else
     5.7 -      List(node_name -> Document.Node.Blob(blob()))
     5.8 +      List(node_name -> Document.Node.Blob())
     5.9    }
    5.10  
    5.11    def node_edits(
    5.12 @@ -171,7 +171,7 @@
    5.13            node_name -> perspective)
    5.14      }
    5.15      else
    5.16 -      List(node_name -> Document.Node.Blob(blob()))
    5.17 +      List(node_name -> Document.Node.Blob())
    5.18    }
    5.19  
    5.20  
    5.21 @@ -190,7 +190,7 @@
    5.22        val clear = pending_clear
    5.23        val edits = snapshot()
    5.24        val perspective = node_perspective()
    5.25 -      if (!is_theory || clear || !edits.isEmpty || last_perspective != perspective) {
    5.26 +      if (clear || !edits.isEmpty || last_perspective != perspective) {
    5.27          pending_clear = false
    5.28          pending.clear
    5.29          last_perspective = perspective
     6.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 19:43:26 2013 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:53:43 2013 +0100
     6.3 @@ -19,21 +19,21 @@
     6.4  
     6.5    override def session: Session = PIDE.session
     6.6  
     6.7 +  def document_models(): List[Document_Model] =
     6.8 +    for {
     6.9 +      buffer <- JEdit_Lib.jedit_buffers().toList
    6.10 +      model <- PIDE.document_model(buffer)
    6.11 +    } yield model
    6.12 +
    6.13 +  def document_blobs(): Document.Blobs =
    6.14 +    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
    6.15 +
    6.16    override def flush()
    6.17    {
    6.18      Swing_Thread.require()
    6.19  
    6.20 -    session.update(
    6.21 -      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    6.22 -        case (edits, buffer) =>
    6.23 -          JEdit_Lib.buffer_lock(buffer) {
    6.24 -            PIDE.document_model(buffer) match {
    6.25 -              case Some(model) => model.flushed_edits() ::: edits
    6.26 -              case None => edits
    6.27 -            }
    6.28 -          }
    6.29 -      }
    6.30 -    )
    6.31 +    val edits = document_models().flatMap(_.flushed_edits())
    6.32 +    if (!edits.isEmpty) session.update(document_blobs(), edits)
    6.33    }
    6.34  
    6.35    private val delay_flush =
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Nov 19 19:43:26 2013 +0100
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Nov 19 20:53:43 2013 +0100
     7.3 @@ -113,7 +113,7 @@
     7.4              model_edits ::: edits
     7.5            }
     7.6          }
     7.7 -      session.update(init_edits)
     7.8 +      session.update(PIDE.editor.document_blobs(), init_edits)
     7.9      }
    7.10    }
    7.11