equal
deleted
inserted
replaced
41 |
41 |
42 /* header */ |
42 /* header */ |
43 |
43 |
44 def node_header: Document.Node.Header = |
44 def node_header: Document.Node.Header = |
45 resources.special_header(node_name) getOrElse |
45 resources.special_header(node_name) getOrElse |
46 { |
46 resources.check_thy_reader("", node_name, Scan.char_reader(doc.text)) |
47 if (is_theory) |
|
48 resources.check_thy_reader("", node_name, Scan.char_reader(doc.text)) |
|
49 else Document.Node.no_header |
|
50 } |
|
51 |
47 |
52 |
48 |
53 /* perspective */ |
49 /* perspective */ |
54 |
50 |
55 def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |
51 def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |