equal
deleted
inserted
replaced
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 = |