equal
deleted
inserted
replaced
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: 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 |
|
21 |
|
22 |
20 /* header */ |
23 /* header */ |
21 |
24 |
22 def is_theory: Boolean = node_name.is_theory |
25 def is_theory: Boolean = node_name.is_theory |
23 |
26 |
24 def node_header(resources: VSCode_Resources): Document.Node.Header = |
27 def node_header(resources: VSCode_Resources): Document.Node.Header = |