equal
deleted
inserted
replaced
67 } |
67 } |
68 |
68 |
69 |
69 |
70 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) |
70 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) |
71 { |
71 { |
|
72 override def toString: String = node_name.toString |
|
73 |
|
74 |
72 /* header */ |
75 /* header */ |
73 |
76 |
74 def is_theory: Boolean = node_name.is_theory |
77 def is_theory: Boolean = node_name.is_theory |
75 |
78 |
76 def node_header(): Document.Node.Header = |
79 def node_header(): Document.Node.Header = |