src/Pure/Thy/thy_syntax.scala
changeset 59086 94b2690ad494
parent 59077 7e0d3da6e6d8
child 59319 677615cba30d
equal deleted inserted replaced
59085:08a6901eb035 59086:94b2690ad494
    95     for (name <- syntax_changed) {
    95     for (name <- syntax_changed) {
    96       val node = nodes(name)
    96       val node = nodes(name)
    97       val syntax =
    97       val syntax =
    98         if (node.is_empty) None
    98         if (node.is_empty) None
    99         else {
    99         else {
   100           val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax)
   100           val header = node.header
   101           Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords))
   101           val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
       
   102           Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
   102         }
   103         }
   103       nodes += (name -> node.update_syntax(syntax))
   104       nodes += (name -> node.update_syntax(syntax))
   104     }
   105     }
   105 
   106 
   106     (syntax_changed, nodes, doc_edits.toList)
   107     (syntax_changed, nodes, doc_edits.toList)