100 if null errors then (master, header) |
100 if null errors then (master, header) |
101 else error (cat_lines errors); |
101 else error (cat_lines errors); |
102 |
102 |
103 fun read_header node span = |
103 fun read_header node span = |
104 let |
104 let |
105 val (dir, {name = (name, _), imports, keywords, uses}) = get_header node; |
105 val (dir, {name = (name, _), imports, keywords, files}) = get_header node; |
106 val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span; |
106 val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span; |
107 in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end; |
107 in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end; |
108 |
108 |
109 fun get_perspective (Node {perspective, ...}) = perspective; |
109 fun get_perspective (Node {perspective, ...}) = perspective; |
110 fun set_perspective ids = |
110 fun set_perspective ids = |
111 map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result)); |
111 map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result)); |
112 |
112 |