equal
deleted
inserted
replaced
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.map(_._1) != node1.header.imports.map(_._1) || |
86 node.header.keywords != node1.header.keywords || |
86 node.header.keywords != node1.header.keywords || |
|
87 node.header.abbrevs != node1.header.abbrevs || |
87 node.header.errors != node1.header.errors) syntax_changed0 += name |
88 node.header.errors != node1.header.errors) syntax_changed0 += name |
88 nodes += (name -> node1) |
89 nodes += (name -> node1) |
89 doc_edits += (name -> Document.Node.Deps(header)) |
90 doc_edits += (name -> Document.Node.Deps(header)) |
90 } |
91 } |
91 case _ => |
92 case _ => |
98 val syntax = |
99 val syntax = |
99 if (node.is_empty) None |
100 if (node.is_empty) None |
100 else { |
101 else { |
101 val header = node.header |
102 val header = node.header |
102 val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax) |
103 val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax) |
103 Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords)) |
104 Some((resources.base_syntax /: imports_syntax)(_ ++ _) |
|
105 .add_keywords(header.keywords).add_abbrevs(header.abbrevs)) |
104 } |
106 } |
105 nodes += (name -> node.update_syntax(syntax)) |
107 nodes += (name -> node.update_syntax(syntax)) |
106 } |
108 } |
107 |
109 |
108 (syntax_changed, nodes, doc_edits.toList) |
110 (syntax_changed, nodes, doc_edits.toList) |