equal
deleted
inserted
replaced
213 | Header header => |
213 | Header header => |
214 let |
214 let |
215 val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []); |
215 val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []); |
216 val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []); |
216 val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []); |
217 val header' = |
217 val header' = |
218 (List.app Keyword.declare keywords; header) |
218 (List.app (fn (name, decl) => |
|
219 Keyword.declare name (Option.map Keyword.make decl)) keywords; header) |
219 handle exn as ERROR _ => Exn.Exn exn; |
220 handle exn as ERROR _ => Exn.Exn exn; |
220 val nodes1 = nodes |
221 val nodes1 = nodes |
221 |> default_node name |
222 |> default_node name |
222 |> fold default_node imports; |
223 |> fold default_node imports; |
223 val nodes2 = nodes1 |
224 val nodes2 = nodes1 |