src/Pure/PIDE/document.ML
changeset 46950 d0181abdbdac
parent 46945 26007caf6e9c
child 46958 0ec8f04e753a
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 15 20:07:00 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 15 22:08:53 2012 +0100
     1.3 @@ -215,7 +215,8 @@
     1.4            val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
     1.5            val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
     1.6            val header' =
     1.7 -            (List.app Keyword.declare keywords; header)
     1.8 +            (List.app (fn (name, decl) =>
     1.9 +                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
    1.10                handle exn as ERROR _ => Exn.Exn exn;
    1.11            val nodes1 = nodes
    1.12              |> default_node name