clarified Version.syntax -- avoid guessing initial situation;
authorwenzelm
Thu Apr 03 21:08:00 2014 +0200 (2014-04-03)
changeset 56394bbf4d512f395
parent 56393 22f533e6a049
child 56395 0546e036d1c0
clarified Version.syntax -- avoid guessing initial situation;
src/Pure/PIDE/document.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Apr 03 20:53:35 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Apr 03 21:08:00 2014 +0200
     1.3 @@ -317,17 +317,15 @@
     1.4    {
     1.5      val init: Version = new Version()
     1.6  
     1.7 -    def make(syntax: Prover.Syntax, nodes: Nodes): Version =
     1.8 +    def make(syntax: Option[Prover.Syntax], nodes: Nodes): Version =
     1.9        new Version(Document_ID.make(), syntax, nodes)
    1.10    }
    1.11  
    1.12    final class Version private(
    1.13      val id: Document_ID.Version = Document_ID.none,
    1.14 -    val syntax: Prover.Syntax = Prover.Syntax.empty,
    1.15 +    val syntax: Option[Prover.Syntax] = None,
    1.16      val nodes: Nodes = Nodes.empty)
    1.17    {
    1.18 -    def is_init: Boolean = id == Document_ID.none
    1.19 -
    1.20      override def toString: String = "Version(" + id + ")"
    1.21    }
    1.22  
     2.1 --- a/src/Pure/PIDE/prover.scala	Thu Apr 03 20:53:35 2014 +0200
     2.2 +++ b/src/Pure/PIDE/prover.scala	Thu Apr 03 21:08:00 2014 +0200
     2.3 @@ -11,11 +11,6 @@
     2.4  {
     2.5    /* syntax */
     2.6  
     2.7 -  object Syntax
     2.8 -  {
     2.9 -    val empty: Syntax = Outer_Syntax.empty
    2.10 -  }
    2.11 -
    2.12    trait Syntax
    2.13    {
    2.14      def add_keywords(keywords: Thy_Header.Keywords): Syntax
     3.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 03 20:53:35 2014 +0200
     3.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 03 21:08:00 2014 +0200
     3.3 @@ -225,8 +225,7 @@
     3.4    def recent_syntax(): Prover.Syntax =
     3.5    {
     3.6      val version = current_state().recent_finished.version.get_finished
     3.7 -    if (version.is_init) resources.base_syntax  // FIXME
     3.8 -    else version.syntax
     3.9 +    version.syntax getOrElse resources.base_syntax
    3.10    }
    3.11  
    3.12    def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 20:53:35 2014 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 21:08:00 2014 +0200
     4.3 @@ -153,7 +153,7 @@
     4.4    /** header edits: structure and outer syntax **/
     4.5  
     4.6    private def header_edits(
     4.7 -    base_syntax: Prover.Syntax,
     4.8 +    resources: Resources,
     4.9      previous: Document.Version,
    4.10      edits: List[Document.Edit_Text]):
    4.11      (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
    4.12 @@ -180,14 +180,16 @@
    4.13      }
    4.14  
    4.15      val (syntax, syntax_changed) =
    4.16 -      if (previous.is_init || updated_keywords) {
    4.17 -        val syntax =
    4.18 -          (base_syntax /: nodes.iterator) {
    4.19 -            case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    4.20 -          }
    4.21 -        (syntax, true)
    4.22 +      previous.syntax match {
    4.23 +        case Some(syntax) if !updated_keywords =>
    4.24 +          (syntax, false)
    4.25 +        case _ =>
    4.26 +          val syntax =
    4.27 +            (resources.base_syntax /: nodes.iterator) {
    4.28 +              case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    4.29 +            }
    4.30 +          (syntax, true)
    4.31        }
    4.32 -      else (previous.syntax, false)
    4.33  
    4.34      val reparse =
    4.35        if (updated_imports || updated_keywords)
    4.36 @@ -443,10 +445,10 @@
    4.37        doc_blobs.get(name) orElse previous.nodes(name).get_blob
    4.38  
    4.39      val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
    4.40 -      header_edits(resources.base_syntax, previous, edits)
    4.41 +      header_edits(resources, previous, edits)
    4.42  
    4.43      val (doc_edits, version) =
    4.44 -      if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
    4.45 +      if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
    4.46        else {
    4.47          val reparse =
    4.48            (reparse0 /: nodes0.iterator)({
    4.49 @@ -485,7 +487,7 @@
    4.50  
    4.51              nodes += (name -> node2)
    4.52          }
    4.53 -        (doc_edits.toList, Document.Version.make(syntax, nodes))
    4.54 +        (doc_edits.toList, Document.Version.make(Some(syntax), nodes))
    4.55        }
    4.56  
    4.57      Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
     5.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu Apr 03 20:53:35 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Thu Apr 03 21:08:00 2014 +0200
     5.3 @@ -47,7 +47,7 @@
     5.4      name match {
     5.5        case "isabelle" | "isabelle-markup" =>
     5.6          PIDE.session.recent_syntax match {
     5.7 -          case syntax : Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
     5.8 +          case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
     5.9            case _ => None
    5.10          }
    5.11        case "isabelle-options" => Some(Options.options_syntax)