src/Tools/VSCode/src/document_model.scala
changeset 64682 7e119f32276a
parent 64680 7f87c1aa0ffa
child 64683 c0c09b6dfbe0
equal deleted inserted replaced
64681:642b6105e6f4 64682:7e119f32276a
    11 
    11 
    12 import scala.util.parsing.input.CharSequenceReader
    12 import scala.util.parsing.input.CharSequenceReader
    13 
    13 
    14 
    14 
    15 case class Document_Model(
    15 case class Document_Model(
    16   session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length,
    16   session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Text.Length,
    17   changed: Boolean = true,
    17   changed: Boolean = true,
    18   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    18   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    19 {
    19 {
    20   override def toString: String = node_name.toString
    20   override def toString: String = node_name.toString
    21 
    21