src/Pure/PIDE/document.ML
changeset 46950 d0181abdbdac
parent 46945 26007caf6e9c
child 46958 0ec8f04e753a
equal deleted inserted replaced
46949:94aa7b81bcf6 46950:d0181abdbdac
   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