tuned signature;
authorwenzelm
Sat Mar 29 10:17:09 2014 +0100 (2014-03-29)
changeset 56315c20053f67093
parent 56314 9a513737a0b2
child 56316 b1cf8ddc2e04
tuned signature;
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 29 09:34:51 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 10:17:09 2014 +0100
     1.3 @@ -93,12 +93,12 @@
     1.4  
     1.5    /* theory text edits */
     1.6  
     1.7 -  def text_edits(
     1.8 -    reparse_limit: Int,
     1.9 -    previous: Document.Version,
    1.10 -    doc_blobs: Document.Blobs,
    1.11 -    edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
    1.12 -    Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
    1.13 +  def parse_edits(
    1.14 +      reparse_limit: Int,
    1.15 +      previous: Document.Version,
    1.16 +      doc_blobs: Document.Blobs,
    1.17 +      edits: List[Document.Edit_Text]): Session.Change =
    1.18 +    Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits)
    1.19  
    1.20    def syntax_changed() { }
    1.21  }
     2.1 --- a/src/Pure/PIDE/session.scala	Sat Mar 29 09:34:51 2014 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Sat Mar 29 10:17:09 2014 +0100
     2.3 @@ -18,6 +18,16 @@
     2.4  
     2.5  object Session
     2.6  {
     2.7 +  /* change */
     2.8 +
     2.9 +  sealed case class Change(
    2.10 +    previous: Document.Version,
    2.11 +    doc_blobs: Document.Blobs,
    2.12 +    syntax_changed: Boolean,
    2.13 +    doc_edits: List[Document.Edit_Command],
    2.14 +    version: Document.Version)
    2.15 +
    2.16 +
    2.17    /* events */
    2.18  
    2.19    //{{{
    2.20 @@ -179,12 +189,12 @@
    2.21  
    2.22          case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    2.23            val prev = previous.get_finished
    2.24 -          val (syntax_changed, doc_edits, version) =
    2.25 -            Timing.timeit("text_edits", timing) {
    2.26 -              resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
    2.27 +          val change =
    2.28 +            Timing.timeit("parse_edits", timing) {
    2.29 +              resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits)
    2.30              }
    2.31 -          version_result.fulfill(version)
    2.32 -          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
    2.33 +          version_result.fulfill(change.version)
    2.34 +          sender ! change
    2.35  
    2.36          case bad => System.err.println("change_parser: ignoring bad message " + bad)
    2.37        }
    2.38 @@ -249,12 +259,6 @@
    2.39  
    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 -    doc_blobs: Document.Blobs,
    2.44 -    syntax_changed: Boolean,
    2.45 -    doc_edits: List[Document.Edit_Command],
    2.46 -    previous: Document.Version,
    2.47 -    version: Document.Version)
    2.48    private case class Protocol_Command(name: String, args: List[String])
    2.49    private case class Messages(msgs: List[Isabelle_Process.Message])
    2.50    private case class Update_Options(options: Options)
    2.51 @@ -367,18 +371,16 @@
    2.52  
    2.53      /* resulting changes */
    2.54  
    2.55 -    def handle_change(change: Change)
    2.56 +    def handle_change(change: Session.Change)
    2.57      //{{{
    2.58      {
    2.59 -      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
    2.60 -
    2.61        def id_command(command: Command)
    2.62        {
    2.63          for {
    2.64            digest <- command.blobs_digests
    2.65            if !global_state().defined_blob(digest)
    2.66          } {
    2.67 -          doc_blobs.get(digest) match {
    2.68 +          change.doc_blobs.get(digest) match {
    2.69              case Some(blob) =>
    2.70                global_state >> (_.define_blob(digest))
    2.71                prover.get.define_blob(blob)
    2.72 @@ -392,16 +394,16 @@
    2.73            prover.get.define_command(command)
    2.74          }
    2.75        }
    2.76 -      doc_edits foreach {
    2.77 +      change.doc_edits foreach {
    2.78          case (_, edit) =>
    2.79            edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
    2.80        }
    2.81  
    2.82 -      val assignment = global_state().the_assignment(previous).check_finished
    2.83 -      global_state >> (_.define_version(version, assignment))
    2.84 -      prover.get.update(previous.id, version.id, doc_edits)
    2.85 +      val assignment = global_state().the_assignment(change.previous).check_finished
    2.86 +      global_state >> (_.define_version(change.version, assignment))
    2.87 +      prover.get.update(change.previous.id, change.version.id, change.doc_edits)
    2.88  
    2.89 -      if (syntax_changed) resources.syntax_changed()
    2.90 +      if (change.syntax_changed) resources.syntax_changed()
    2.91      }
    2.92      //}}}
    2.93  
    2.94 @@ -556,11 +558,11 @@
    2.95                all_messages.event(output)
    2.96            }
    2.97  
    2.98 -        case change: Change
    2.99 +        case change: Session.Change
   2.100          if prover.isDefined && global_state().is_assigned(change.previous) =>
   2.101            handle_change(change)
   2.102  
   2.103 -        case bad if !bad.isInstanceOf[Change] =>
   2.104 +        case bad if !bad.isInstanceOf[Session.Change] =>
   2.105            System.err.println("session_actor: ignoring bad message " + bad)
   2.106        }
   2.107      }
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 09:34:51 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:17:09 2014 +0100
     3.3 @@ -431,19 +431,18 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  def text_edits(
     3.8 +  def parse_edits(
     3.9        resources: Resources,
    3.10        reparse_limit: Int,
    3.11        previous: Document.Version,
    3.12        doc_blobs: Document.Blobs,
    3.13 -      edits: List[Document.Edit_Text])
    3.14 -    : (Boolean, List[Document.Edit_Command], Document.Version) =
    3.15 +      edits: List[Document.Edit_Text]): Session.Change =
    3.16    {
    3.17      val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
    3.18        header_edits(resources.base_syntax, previous, edits)
    3.19  
    3.20      if (edits.isEmpty)
    3.21 -      (false, Nil, Document.Version.make(syntax, previous.nodes))
    3.22 +      Session.Change(previous, doc_blobs, false, Nil, Document.Version.make(syntax, previous.nodes))
    3.23      else {
    3.24        val reparse =
    3.25          (reparse0 /: nodes0.entries)({
    3.26 @@ -482,7 +481,12 @@
    3.27            nodes += (name -> node2)
    3.28        }
    3.29  
    3.30 -      (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
    3.31 +      Session.Change(
    3.32 +        previous,
    3.33 +        doc_blobs,
    3.34 +        syntax_changed,
    3.35 +        doc_edits.toList,
    3.36 +        Document.Version.make(syntax, nodes))
    3.37      }
    3.38    }
    3.39  }