src/Pure/PIDE/document.ML
changeset 46958 0ec8f04e753a
parent 46950 d0181abdbdac
child 47051 b32e6de4a39b
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Mar 16 11:26:55 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Mar 16 13:05:30 2012 +0100
     1.3 @@ -213,10 +213,8 @@
     1.4      | Header header =>
     1.5          let
     1.6            val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
     1.7 -          val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
     1.8            val header' =
     1.9 -            (List.app (fn (name, decl) =>
    1.10 -                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
    1.11 +            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
    1.12                handle exn as ERROR _ => Exn.Exn exn;
    1.13            val nodes1 = nodes
    1.14              |> default_node name