equal
deleted
inserted
replaced
80 val node = nodes(name) |
80 val node = nodes(name) |
81 val update_header = |
81 val update_header = |
82 node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header |
82 node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header |
83 if (update_header) { |
83 if (update_header) { |
84 val node1 = node.update_header(header) |
84 val node1 = node.update_header(header) |
85 if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) || |
85 if (node.header.imports != node1.header.imports || |
86 node.header.keywords != node1.header.keywords || |
86 node.header.keywords != node1.header.keywords || |
87 node.header.abbrevs != node1.header.abbrevs || |
87 node.header.abbrevs != node1.header.abbrevs || |
88 node.header.errors != node1.header.errors) syntax_changed0 += name |
88 node.header.errors != node1.header.errors) syntax_changed0 += name |
89 nodes += (name -> node1) |
89 nodes += (name -> node1) |
90 doc_edits += (name -> Document.Node.Deps(header)) |
90 doc_edits += (name -> Document.Node.Deps(header)) |
100 if (node.is_empty) None |
100 if (node.is_empty) None |
101 else { |
101 else { |
102 val header = node.header |
102 val header = node.header |
103 val imports_syntax = |
103 val imports_syntax = |
104 if (header.imports.nonEmpty) { |
104 if (header.imports.nonEmpty) { |
105 Outer_Syntax.merge( |
105 Outer_Syntax.merge(header.imports.map(resources.session_base.node_syntax(nodes, _))) |
106 header.imports.map(p => resources.session_base.node_syntax(nodes, p._1))) |
|
107 } |
106 } |
108 else resources.session_base.overall_syntax |
107 else resources.session_base.overall_syntax |
109 Some(imports_syntax + header) |
108 Some(imports_syntax + header) |
110 } |
109 } |
111 nodes += (name -> node.update_syntax(syntax)) |
110 nodes += (name -> node.update_syntax(syntax)) |