src/Tools/VSCode/src/document_model.scala
changeset 64723 65bcb1fbaa73
parent 64710 72ca4e5f976e
child 64725 38305f56c769
equal deleted inserted replaced
64722:6df73de0d3c7 64723:65bcb1fbaa73
    28 sealed case class Document_Model(
    28 sealed case class Document_Model(
    29   session: Session,
    29   session: Session,
    30   node_name: Document.Node.Name,
    30   node_name: Document.Node.Name,
    31   doc: Line.Document,
    31   doc: Line.Document,
    32   external: Boolean = false,
    32   external: Boolean = false,
    33   node_visible: Boolean = true,
       
    34   node_required: Boolean = false,
    33   node_required: Boolean = false,
    35   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    34   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    36   pending_edits: Vector[Text.Edit] = Vector.empty,
    35   pending_edits: Vector[Text.Edit] = Vector.empty,
    37   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    36   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    38 {
    37 {
    66       else Document.Node.no_header
    65       else Document.Node.no_header
    67     }
    66     }
    68 
    67 
    69 
    68 
    70   /* perspective */
    69   /* perspective */
       
    70 
       
    71   def node_visible: Boolean = !external
    71 
    72 
    72   def text_perspective: Text.Perspective =
    73   def text_perspective: Text.Perspective =
    73     if (node_visible) Text.Perspective.full else Text.Perspective.empty
    74     if (node_visible) Text.Perspective.full else Text.Perspective.empty
    74 
    75 
    75   def node_perspective: Document.Node.Perspective_Text =
    76   def node_perspective: Document.Node.Perspective_Text =