src/Tools/VSCode/src/document_model.scala
changeset 64679 b2bf280b7e13
parent 64673 b5965890e54d
child 64680 7f87c1aa0ffa
equal deleted inserted replaced
64678:914dffe59cc5 64679:b2bf280b7e13
    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,
    16   session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length,
    17   changed: Boolean = true)
    17   changed: Boolean = true,
       
    18   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    18 {
    19 {
    19   /* header */
    20   /* header */
    20 
    21 
    21   def is_theory: Boolean = node_name.is_theory
    22   def is_theory: Boolean = node_name.is_theory
    22 
    23 
    46     else Nil
    47     else Nil
    47 
    48 
    48   def unchanged: Document_Model = if (changed) copy(changed = false) else this
    49   def unchanged: Document_Model = if (changed) copy(changed = false) else this
    49 
    50 
    50 
    51 
       
    52   /* diagnostics */
       
    53 
       
    54   def publish_diagnostics(rendering: VSCode_Rendering)
       
    55     : Option[(List[Text.Info[Command.Results]], Document_Model)] =
       
    56   {
       
    57     val diagnostics = rendering.diagnostics
       
    58     if (diagnostics == published_diagnostics) None
       
    59     else Some(diagnostics, copy(published_diagnostics = diagnostics))
       
    60   }
       
    61 
       
    62 
    51   /* snapshot and rendering */
    63   /* snapshot and rendering */
    52 
    64 
    53   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    65   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    54 
    66 
    55   def rendering(options: Options, text_length: Length): VSCode_Rendering =
    67   def rendering(options: Options): VSCode_Rendering =
    56     new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
    68     new VSCode_Rendering(this, snapshot(), options, session.resources)
    57 }
    69 }