equal
deleted
inserted
replaced
71 |
71 |
72 /* header */ |
72 /* header */ |
73 |
73 |
74 def node_header: Document.Node.Header = |
74 def node_header: Document.Node.Header = |
75 resources.special_header(node_name) getOrElse |
75 resources.special_header(node_name) getOrElse |
76 resources.check_thy_reader("", node_name, Scan.char_reader(content.text)) |
76 resources.check_thy_reader(node_name, Scan.char_reader(content.text)) |
77 |
77 |
78 |
78 |
79 /* perspective */ |
79 /* perspective */ |
80 |
80 |
81 def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |
81 def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |