equal
deleted
inserted
replaced
30 doc: Line.Document, |
30 doc: Line.Document, |
31 external_file: Boolean = false, |
31 external_file: Boolean = false, |
32 node_required: Boolean = false, |
32 node_required: Boolean = false, |
33 last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
33 last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
34 pending_edits: Vector[Text.Edit] = Vector.empty, |
34 pending_edits: Vector[Text.Edit] = Vector.empty, |
35 published_diagnostics: List[Text.Info[Command.Results]] = Nil) |
35 published_diagnostics: List[Text.Info[Command.Results]] = Nil) extends Document.Model |
36 { |
36 { |
37 /* name */ |
|
38 |
|
39 override def toString: String = node_name.toString |
|
40 |
|
41 def is_theory: Boolean = node_name.is_theory |
|
42 |
|
43 |
|
44 /* external file */ |
37 /* external file */ |
45 |
38 |
46 def external(b: Boolean): Document_Model = copy(external_file = b) |
39 def external(b: Boolean): Document_Model = copy(external_file = b) |
47 |
40 |
48 def node_visible: Boolean = !external_file |
41 def node_visible: Boolean = !external_file |