node-specific syntax, with base_syntax as default;
authorwenzelm
Tue Dec 02 14:16:56 2014 +0100 (2014-12-02)
changeset 590777e0d3da6e6d8
parent 59076 65babcd8b0e6
child 59078 cf255dc2b48f
node-specific syntax, with base_syntax as default;
clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
src/Pure/Isar/outer_syntax.scala
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/document_model.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Dec 01 19:25:20 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 02 14:16:56 2014 +0100
     1.3 @@ -114,12 +114,13 @@
     1.4  
     1.5    /* merge */
     1.6  
     1.7 -  def ++ (other: Outer_Syntax): Outer_Syntax =
     1.8 +  def ++ (other: Prover.Syntax): Prover.Syntax =
     1.9      if (this eq other) this
    1.10      else {
    1.11 -      val keywords1 = keywords ++ other.keywords
    1.12 -      val completion1 = completion ++ other.completion
    1.13 -      new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.14 +      val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
    1.15 +      val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
    1.16 +      if ((keywords eq keywords1) && (completion eq completion1)) this
    1.17 +      else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.18      }
    1.19  
    1.20  
     2.1 --- a/src/Pure/PIDE/document.scala	Mon Dec 01 19:25:20 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Tue Dec 02 14:16:56 2014 +0100
     2.3 @@ -244,6 +244,7 @@
     2.4    final class Node private(
     2.5      val get_blob: Option[Document.Blob] = None,
     2.6      val header: Node.Header = Node.no_header,
     2.7 +    val syntax: Option[Prover.Syntax] = None,
     2.8      val perspective: Node.Perspective_Command = Node.no_perspective_command,
     2.9      _commands: Node.Commands = Node.Commands.empty)
    2.10    {
    2.11 @@ -256,15 +257,18 @@
    2.12      def commands: Linear_Set[Command] = _commands.commands
    2.13      def load_commands: List[Command] = _commands.load_commands
    2.14  
    2.15 -    def clear: Node = new Node(header = header)
    2.16 +    def clear: Node = new Node(header = header, syntax = syntax)
    2.17  
    2.18 -    def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
    2.19 +    def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
    2.20  
    2.21      def update_header(new_header: Node.Header): Node =
    2.22 -      new Node(get_blob, new_header, perspective, _commands)
    2.23 +      new Node(get_blob, new_header, syntax, perspective, _commands)
    2.24 +
    2.25 +    def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
    2.26 +      new Node(get_blob, header, new_syntax, perspective, _commands)
    2.27  
    2.28      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    2.29 -      new Node(get_blob, header, new_perspective, _commands)
    2.30 +      new Node(get_blob, header, syntax, new_perspective, _commands)
    2.31  
    2.32      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    2.33        perspective.required == other_perspective.required &&
    2.34 @@ -273,7 +277,7 @@
    2.35  
    2.36      def update_commands(new_commands: Linear_Set[Command]): Node =
    2.37        if (new_commands eq _commands.commands) this
    2.38 -      else new Node(get_blob, header, perspective, Node.Commands(new_commands))
    2.39 +      else new Node(get_blob, header, syntax, perspective, Node.Commands(new_commands))
    2.40  
    2.41      def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    2.42        _commands.iterator(i)
    2.43 @@ -344,14 +348,11 @@
    2.44    object Version
    2.45    {
    2.46      val init: Version = new Version()
    2.47 -
    2.48 -    def make(syntax: Option[Prover.Syntax], nodes: Nodes): Version =
    2.49 -      new Version(Document_ID.make(), syntax, nodes)
    2.50 +    def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
    2.51    }
    2.52  
    2.53    final class Version private(
    2.54      val id: Document_ID.Version = Document_ID.none,
    2.55 -    val syntax: Option[Prover.Syntax] = None,
    2.56      val nodes: Nodes = Nodes.empty)
    2.57    {
    2.58      override def toString: String = "Version(" + id + ")"
     3.1 --- a/src/Pure/PIDE/prover.scala	Mon Dec 01 19:25:20 2014 +0100
     3.2 +++ b/src/Pure/PIDE/prover.scala	Tue Dec 02 14:16:56 2014 +0100
     3.3 @@ -17,6 +17,7 @@
     3.4  
     3.5    trait Syntax
     3.6    {
     3.7 +    def ++ (other: Syntax): Syntax
     3.8      def add_keywords(keywords: Thy_Header.Keywords): Syntax
     3.9      def parse_spans(input: CharSequence): List[Command_Span.Span]
    3.10      def load_command(name: String): Option[List[String]]
     4.1 --- a/src/Pure/PIDE/session.scala	Mon Dec 01 19:25:20 2014 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Tue Dec 02 14:16:56 2014 +0100
     4.3 @@ -47,7 +47,7 @@
     4.4  
     4.5    sealed case class Change(
     4.6      previous: Document.Version,
     4.7 -    syntax_changed: Boolean,
     4.8 +    syntax_changed: List[Document.Node.Name],
     4.9      deps_changed: Boolean,
    4.10      doc_edits: List[Document.Edit_Command],
    4.11      version: Document.Version)
    4.12 @@ -231,11 +231,9 @@
    4.13    private val global_state = Synchronized(Document.State.init)
    4.14    def current_state(): Document.State = global_state.value
    4.15  
    4.16 -  def recent_syntax(): Prover.Syntax =
    4.17 -  {
    4.18 -    val version = current_state().recent_finished.version.get_finished
    4.19 -    version.syntax getOrElse resources.base_syntax
    4.20 -  }
    4.21 +  def recent_syntax(name: Document.Node.Name): Prover.Syntax =
    4.22 +    current_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
    4.23 +    resources.base_syntax
    4.24  
    4.25  
    4.26    /* protocol handlers */
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Dec 01 19:25:20 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Dec 02 14:16:56 2014 +0100
     5.3 @@ -69,11 +69,9 @@
     5.4      resources: Resources,
     5.5      previous: Document.Version,
     5.6      edits: List[Document.Edit_Text]):
     5.7 -    (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
     5.8 -      List[Document.Edit_Command]) =
     5.9 +    (List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
    5.10    {
    5.11 -    var updated_imports = false
    5.12 -    var updated_keywords = false
    5.13 +    val syntax_changed0 = new mutable.ListBuffer[Document.Node.Name]
    5.14      var nodes = previous.nodes
    5.15      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    5.16  
    5.17 @@ -84,32 +82,28 @@
    5.18            !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
    5.19          if (update_header) {
    5.20            val node1 = node.update_header(header)
    5.21 -          updated_imports = updated_imports || (node.header.imports != node1.header.imports)
    5.22 -          updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
    5.23 +          if (node.header.imports != node1.header.imports ||
    5.24 +              node.header.keywords != node1.header.keywords) syntax_changed0 += name
    5.25            nodes += (name -> node1)
    5.26            doc_edits += (name -> Document.Node.Deps(header))
    5.27          }
    5.28        case _ =>
    5.29      }
    5.30  
    5.31 -    val (syntax, syntax_changed) =
    5.32 -      previous.syntax match {
    5.33 -        case Some(syntax) if !updated_keywords =>
    5.34 -          (syntax, false)
    5.35 -        case _ =>
    5.36 -          val syntax =
    5.37 -            (resources.base_syntax /: nodes.iterator) {
    5.38 -              case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    5.39 -            }
    5.40 -          (syntax, true)
    5.41 -      }
    5.42 +    val syntax_changed = nodes.descendants(syntax_changed0.toList)
    5.43  
    5.44 -    val reparse =
    5.45 -      if (updated_imports || updated_keywords)
    5.46 -        nodes.descendants(doc_edits.iterator.map(_._1).toList)
    5.47 -      else Nil
    5.48 +    for (name <- syntax_changed) {
    5.49 +      val node = nodes(name)
    5.50 +      val syntax =
    5.51 +        if (node.is_empty) None
    5.52 +        else {
    5.53 +          val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax)
    5.54 +          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords))
    5.55 +        }
    5.56 +      nodes += (name -> node.update_syntax(syntax))
    5.57 +    }
    5.58  
    5.59 -    (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList)
    5.60 +    (syntax_changed, nodes, doc_edits.toList)
    5.61    }
    5.62  
    5.63  
    5.64 @@ -311,14 +305,13 @@
    5.65      def get_blob(name: Document.Node.Name) =
    5.66        doc_blobs.get(name) orElse previous.nodes(name).get_blob
    5.67  
    5.68 -    val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
    5.69 -      header_edits(resources, previous, edits)
    5.70 +    val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
    5.71  
    5.72      val (doc_edits, version) =
    5.73 -      if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
    5.74 +      if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
    5.75        else {
    5.76          val reparse =
    5.77 -          (reparse0 /: nodes0.iterator)({
    5.78 +          (syntax_changed /: nodes0.iterator)({
    5.79              case (reparse, (name, node)) =>
    5.80                if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
    5.81                  name :: reparse
    5.82 @@ -336,6 +329,7 @@
    5.83          node_edits foreach {
    5.84            case (name, edits) =>
    5.85              val node = nodes(name)
    5.86 +            val syntax = node.syntax getOrElse resources.base_syntax
    5.87              val commands = node.commands
    5.88  
    5.89              val node1 =
    5.90 @@ -354,9 +348,9 @@
    5.91  
    5.92              nodes += (name -> node2)
    5.93          }
    5.94 -        (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
    5.95 +        (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
    5.96        }
    5.97  
    5.98 -    Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
    5.99 +    Session.Change(previous, syntax_changed, !syntax_changed.isEmpty, doc_edits, version)
   5.100    }
   5.101  }
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 01 19:25:20 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 14:16:56 2014 +0100
     6.3 @@ -13,6 +13,7 @@
     6.4  
     6.5  import scala.collection.mutable
     6.6  
     6.7 +import org.gjt.sp.jedit.jEdit
     6.8  import org.gjt.sp.jedit.Buffer
     6.9  import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
    6.10  
    6.11 @@ -44,15 +45,23 @@
    6.12      }
    6.13    }
    6.14  
    6.15 -  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
    6.16 +  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name,
    6.17 +    old_model: Option[Document_Model]): Document_Model =
    6.18    {
    6.19      GUI_Thread.require {}
    6.20 -    apply(buffer).map(_.deactivate)
    6.21 -    val model = new Document_Model(session, buffer, node_name)
    6.22 -    buffer.setProperty(key, model)
    6.23 -    model.activate()
    6.24 -    buffer.propertiesChanged
    6.25 -    model
    6.26 +
    6.27 +    old_model match {
    6.28 +      case Some(old)
    6.29 +      if old.node_name == node_name && Isabelle.buffer_token_marker(buffer).isEmpty => old
    6.30 +
    6.31 +      case _ =>
    6.32 +        apply(buffer).map(_.deactivate)
    6.33 +        val model = new Document_Model(session, buffer, node_name)
    6.34 +        buffer.setProperty(key, model)
    6.35 +        model.activate()
    6.36 +        buffer.propertiesChanged
    6.37 +        model
    6.38 +    }
    6.39    }
    6.40  }
    6.41  
    6.42 @@ -277,18 +286,26 @@
    6.43  
    6.44    /* activation */
    6.45  
    6.46 +  private def refresh_token_marker()
    6.47 +  {
    6.48 +    Isabelle.buffer_token_marker(buffer) match {
    6.49 +      case Some(marker) if marker != buffer.getTokenMarker =>
    6.50 +        buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
    6.51 +        buffer.setTokenMarker(marker)
    6.52 +      case _ =>
    6.53 +    }
    6.54 +  }
    6.55 +
    6.56    private def activate()
    6.57    {
    6.58      pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
    6.59      buffer.addBufferListener(buffer_listener)
    6.60 -    Isabelle.buffer_token_marker(buffer).foreach(marker =>
    6.61 -      JEdit_Lib.update_token_marker(buffer, marker))
    6.62 +    refresh_token_marker()
    6.63    }
    6.64  
    6.65    private def deactivate()
    6.66    {
    6.67      buffer.removeBufferListener(buffer_listener)
    6.68 -    Isabelle.mode_token_marker(JEdit_Lib.buffer_mode(buffer)).foreach(marker =>
    6.69 -      JEdit_Lib.update_token_marker(buffer, marker))
    6.70 +    refresh_token_marker()
    6.71    }
    6.72  }
     7.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 19:25:20 2014 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Dec 02 14:16:56 2014 +0100
     7.3 @@ -47,18 +47,9 @@
     7.4    private lazy val news_syntax: Outer_Syntax =
     7.5      Outer_Syntax.init().no_tokens
     7.6  
     7.7 -  private lazy val bootstrap_syntax: Outer_Syntax =
     7.8 -    Thy_Header.bootstrap_syntax()
     7.9 -
    7.10 -  def session_syntax(): Option[Outer_Syntax] =
    7.11 -    PIDE.session.recent_syntax match {
    7.12 -      case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
    7.13 -      case _ => None
    7.14 -    }
    7.15 -
    7.16    def mode_syntax(mode: String): Option[Outer_Syntax] =
    7.17      mode match {
    7.18 -      case "isabelle" => Some(bootstrap_syntax)
    7.19 +      case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
    7.20        case "isabelle-options" => Some(Options.options_syntax)
    7.21        case "isabelle-root" => Some(Build.root_syntax)
    7.22        case "isabelle-ml" => Some(ml_syntax)
    7.23 @@ -69,9 +60,10 @@
    7.24      }
    7.25  
    7.26    def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
    7.27 -    JEdit_Lib.buffer_mode(buffer) match {
    7.28 -      case "isabelle" => session_syntax()
    7.29 -      case mode => mode_syntax(mode)
    7.30 +    (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
    7.31 +      case ("isabelle", Some(model)) =>
    7.32 +        Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
    7.33 +      case (mode, _) => mode_syntax(mode)
    7.34      }
    7.35  
    7.36  
    7.37 @@ -86,8 +78,10 @@
    7.38    def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
    7.39    {
    7.40      val mode = JEdit_Lib.buffer_mode(buffer)
    7.41 -    if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
    7.42 -    else mode_token_marker(mode)
    7.43 +    val new_token_marker =
    7.44 +      if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
    7.45 +      else mode_token_marker(mode)
    7.46 +    if (new_token_marker == Some(buffer.getTokenMarker)) None else new_token_marker
    7.47    }
    7.48  
    7.49  
     8.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Dec 01 19:25:20 2014 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Dec 02 14:16:56 2014 +0100
     8.3 @@ -153,7 +153,7 @@
     8.4    {
     8.5      val opt_snapshot =
     8.6        GUI_Thread.now {
     8.7 -        Document_Model(buffer) match {
     8.8 +        PIDE.document_model(buffer) match {
     8.9            case Some(model) if model.is_theory => Some(model.snapshot)
    8.10            case _ => None
    8.11          }
     9.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 01 19:25:20 2014 +0100
     9.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Dec 02 14:16:56 2014 +0100
     9.3 @@ -114,12 +114,6 @@
     9.4  
     9.5    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
     9.6  
     9.7 -  def update_token_marker(buffer: JEditBuffer, marker: TokenMarker)
     9.8 -  {
     9.9 -    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
    9.10 -    buffer.setTokenMarker(marker)
    9.11 -  }
    9.12 -
    9.13  
    9.14    /* main jEdit components */
    9.15  
    10.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 01 19:25:20 2014 +0100
    10.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Dec 02 14:16:56 2014 +0100
    10.3 @@ -114,7 +114,7 @@
    10.4  
    10.5    override def commit(change: Session.Change)
    10.6    {
    10.7 -    if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() }
    10.8 +    if (!change.syntax_changed.isEmpty) GUI_Thread.later { jEdit.propertiesChanged() }
    10.9      if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
   10.10    }
   10.11  }
    11.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Dec 01 19:25:20 2014 +0100
    11.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Dec 02 14:16:56 2014 +0100
    11.3 @@ -17,6 +17,7 @@
    11.4  import org.jedit.options.CombinedOptions
    11.5  import org.gjt.sp.jedit.gui.AboutDialog
    11.6  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    11.7 +import org.gjt.sp.jedit.buffer.JEditBuffer
    11.8  import org.gjt.sp.jedit.syntax.ModeProvider
    11.9  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
   11.10  
   11.11 @@ -64,7 +65,11 @@
   11.12  
   11.13    /* document model and view */
   11.14  
   11.15 -  def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   11.16 +  def document_model(buffer: JEditBuffer): Option[Document_Model] =
   11.17 +    buffer match {
   11.18 +      case b: Buffer => Document_Model(b)
   11.19 +      case _ => None
   11.20 +    }
   11.21  
   11.22    def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
   11.23  
   11.24 @@ -111,11 +116,7 @@
   11.25        } {
   11.26          JEdit_Lib.buffer_lock(buffer) {
   11.27            val node_name = resources.node_name(buffer)
   11.28 -          val model =
   11.29 -            document_model(buffer) match {
   11.30 -              case Some(model) if model.node_name == node_name => model
   11.31 -              case _ => Document_Model.init(session, buffer, node_name)
   11.32 -            }
   11.33 +          val model = Document_Model.init(session, buffer, node_name, document_model(buffer))
   11.34            for {
   11.35              text_area <- JEdit_Lib.jedit_text_areas(buffer)
   11.36              if document_view(text_area).map(_.model) != Some(model)
   11.37 @@ -315,7 +316,6 @@
   11.38                "It is for testing only, not for production use.")
   11.39            }
   11.40  
   11.41 -
   11.42          case msg: BufferUpdate
   11.43          if msg.getWhat == BufferUpdate.LOADED ||
   11.44            msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
    12.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Dec 01 19:25:20 2014 +0100
    12.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Dec 02 14:16:56 2014 +0100
    12.3 @@ -43,7 +43,7 @@
    12.4      val nodes0 = version0.nodes
    12.5  
    12.6      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
    12.7 -    val version1 = Document.Version.make(version0.syntax, nodes1)
    12.8 +    val version1 = Document.Version.make(nodes1)
    12.9      val state1 =
   12.10        state0.continue_history(Future.value(version0), edits, Future.value(version1))
   12.11          .define_version(version1, state0.the_assignment(version0))
    13.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Dec 01 19:25:20 2014 +0100
    13.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Dec 02 14:16:56 2014 +0100
    13.3 @@ -308,8 +308,17 @@
    13.4  
    13.5    /* token marker */
    13.6  
    13.7 -  class Marker(mode: String, opt_buffer: Option[Buffer]) extends TokenMarker
    13.8 +  class Marker(
    13.9 +    protected val mode: String,
   13.10 +    protected val opt_buffer: Option[Buffer]) extends TokenMarker
   13.11    {
   13.12 +    override def hashCode: Int = (mode, opt_buffer).hashCode
   13.13 +    override def equals(that: Any): Boolean =
   13.14 +      that match {
   13.15 +        case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer
   13.16 +        case _ => false
   13.17 +      }
   13.18 +
   13.19      override def toString: String =
   13.20        opt_buffer match {
   13.21          case None => "Marker(" + mode + ")"