some support for outer syntax keyword declarations within theory header;
authorwenzelm
Thu Mar 15 00:10:45 2012 +0100 (2012-03-15 ago)
changeset 46938cda018294515
parent 46937 efb98d27dc1a
child 46939 5b67ac48b384
some support for outer syntax keyword declarations within theory header;
more uniform Thy_Header.header as argument for begin_theory etc.;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_load.scala
     1.1 --- a/etc/isar-keywords-ZF.el	Wed Mar 14 22:34:18 2012 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Thu Mar 15 00:10:45 2012 +0100
     1.3 @@ -229,6 +229,7 @@
     1.4      "infixr"
     1.5      "intros"
     1.6      "is"
     1.7 +    "keywords"
     1.8      "monos"
     1.9      "notes"
    1.10      "obtains"
     2.1 --- a/etc/isar-keywords.el	Wed Mar 14 22:34:18 2012 +0100
     2.2 +++ b/etc/isar-keywords.el	Thu Mar 15 00:10:45 2012 +0100
     2.3 @@ -305,6 +305,7 @@
     2.4      "infixl"
     2.5      "infixr"
     2.6      "is"
     2.7 +    "keywords"
     2.8      "lazy"
     2.9      "module_name"
    2.10      "monos"
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Mar 14 22:34:18 2012 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 00:10:45 2012 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
     3.5    "advanced", "and", "assumes", "attach", "begin", "binder",
     3.6    "constrains", "defines", "fixes", "for", "identifier", "if",
     3.7 -  "imports", "in", "infix", "infixl", "infixr", "is",
     3.8 +  "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
     3.9    "notes", "obtains", "open", "output", "overloaded", "pervasive",
    3.10    "shows", "structure", "unchecked", "uses", "where", "|"];
    3.11  
    3.12 @@ -28,12 +28,10 @@
    3.13  
    3.14  val _ =
    3.15    Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
    3.16 -    (Thy_Header.args >> (fn (name, imports, uses) =>
    3.17 +    (Thy_Header.args >> (fn header =>
    3.18        Toplevel.print o
    3.19          Toplevel.init_theory
    3.20 -          (fn () =>
    3.21 -            Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
    3.22 -              name imports (map (apfst Path.explode) uses))));
    3.23 +          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    3.24  
    3.25  val _ =
    3.26    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     4.1 --- a/src/Pure/Isar/keyword.ML	Wed Mar 14 22:34:18 2012 +0100
     4.2 +++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 00:10:45 2012 +0100
     4.3 @@ -37,6 +37,7 @@
     4.4    val tag_theory: T -> T
     4.5    val tag_proof: T -> T
     4.6    val tag_ml: T -> T
     4.7 +  val make: string * string list -> T
     4.8    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
     4.9    val is_keyword: string -> bool
    4.10    val dest_keywords: unit -> string list
    4.11 @@ -115,6 +116,39 @@
    4.12  val tag_ml = tag "ML";
    4.13  
    4.14  
    4.15 +(* external names *)
    4.16 +
    4.17 +val name_table = Symtab.make
    4.18 +  [("control",            control),
    4.19 +   ("diag",               diag),
    4.20 +   ("thy_begin",          thy_begin),
    4.21 +   ("thy_switch",         thy_switch),
    4.22 +   ("thy_end",            thy_end),
    4.23 +   ("thy_heading",        thy_heading),
    4.24 +   ("thy_decl",           thy_decl),
    4.25 +   ("thy_script",         thy_script),
    4.26 +   ("thy_goal",           thy_goal),
    4.27 +   ("thy_schematic_goal", thy_schematic_goal),
    4.28 +   ("qed",                qed),
    4.29 +   ("qed_block",          qed_block),
    4.30 +   ("qed_global",         qed_global),
    4.31 +   ("prf_heading",        prf_heading),
    4.32 +   ("prf_goal",           prf_goal),
    4.33 +   ("prf_block",          prf_block),
    4.34 +   ("prf_open",           prf_open),
    4.35 +   ("prf_close",          prf_close),
    4.36 +   ("prf_chain",          prf_chain),
    4.37 +   ("prf_decl",           prf_decl),
    4.38 +   ("prf_asm",            prf_asm),
    4.39 +   ("prf_asm_goal",       prf_asm_goal),
    4.40 +   ("prf_script",         prf_script)];
    4.41 +
    4.42 +fun make (kind, tags) =
    4.43 +  (case Symtab.lookup name_table kind of
    4.44 +    SOME k => k |> fold tag tags
    4.45 +  | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
    4.46 +
    4.47 +
    4.48  
    4.49  (** global keyword tables **)
    4.50  
     5.1 --- a/src/Pure/PIDE/document.ML	Wed Mar 14 22:34:18 2012 +0100
     5.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 15 00:10:45 2012 +0100
     5.3 @@ -15,7 +15,7 @@
     5.4    val new_id: unit -> id
     5.5    val parse_id: string -> id
     5.6    val print_id: id -> string
     5.7 -  type node_header = ((string * string) * string list * (string * bool) list) Exn.result
     5.8 +  type node_header = (string * Thy_Header.header) Exn.result
     5.9    datatype node_edit =
    5.10      Clear |
    5.11      Edits of (command_id option * command_id option) list |
    5.12 @@ -58,7 +58,7 @@
    5.13  
    5.14  (** document structure **)
    5.15  
    5.16 -type node_header = ((string * string) * string list * (string * bool) list) Exn.result;
    5.17 +type node_header = (string * Thy_Header.header) Exn.result;
    5.18  type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
    5.19  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    5.20  
    5.21 @@ -212,7 +212,7 @@
    5.22          |> touch_node name
    5.23      | Header header =>
    5.24          let
    5.25 -          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
    5.26 +          val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
    5.27            val nodes1 = nodes
    5.28              |> default_node name
    5.29              |> fold default_node imports;
    5.30 @@ -307,7 +307,6 @@
    5.31  end;
    5.32  
    5.33  
    5.34 -
    5.35  (* toplevel transactions *)
    5.36  
    5.37  local
    5.38 @@ -447,16 +446,15 @@
    5.39  fun init_theory deps node =
    5.40    let
    5.41      (* FIXME provide files via Scala layer, not master_dir *)
    5.42 -    val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node);
    5.43 -    val files = map (apfst Path.explode) uses;
    5.44 +    val (master_dir, header) = Exn.release (get_header node);
    5.45      val parents =
    5.46 -      imports |> map (fn import =>
    5.47 +      #imports header |> map (fn import =>
    5.48          (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    5.49            SOME thy => thy
    5.50          | NONE =>
    5.51              get_theory (Position.file_only import)
    5.52                (snd (Future.join (the (AList.lookup (op =) deps import))))));
    5.53 -  in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end;
    5.54 +  in Thy_Load.begin_theory (Path.explode master_dir) header parents end;
    5.55  
    5.56  in
    5.57  
     6.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 14 22:34:18 2012 +0100
     6.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 15 00:10:45 2012 +0100
     6.3 @@ -39,7 +39,10 @@
     6.4  
     6.5    object Node
     6.6    {
     6.7 -    sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)])
     6.8 +    sealed case class Deps(
     6.9 +      imports: List[Name],
    6.10 +      keywords: List[(String, Option[(String, List[String])])],
    6.11 +      uses: List[(String, Boolean)])
    6.12  
    6.13      object Name
    6.14      {
     7.1 --- a/src/Pure/PIDE/protocol.ML	Wed Mar 14 22:34:18 2012 +0100
     7.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Mar 15 00:10:45 2012 +0100
     7.3 @@ -46,9 +46,16 @@
     7.4                   [fn ([], []) => Document.Clear,
     7.5                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     7.6                    fn ([], a) =>
     7.7 -                    Document.Header
     7.8 -                      (Exn.Res
     7.9 -                        (triple (pair string string) (list string) (list (pair string bool)) a)),
    7.10 +                    let
    7.11 +                      val ((((master, name), imports), keywords), uses) =
    7.12 +                        pair (pair (pair (pair string string) (list string))
    7.13 +                          (list (pair string (option (pair string (list string))))))
    7.14 +                          (list (pair string bool)) a;
    7.15 +                      val res =
    7.16 +                        Exn.capture (fn () =>
    7.17 +                          (master, Thy_Header.make name imports keywords
    7.18 +                            (map (apfst Path.explode) uses))) ();
    7.19 +                    in Document.Header res end,
    7.20                    fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    7.21                    fn (a, []) => Document.Perspective (map int_atom a)]))
    7.22              end;
     8.1 --- a/src/Pure/PIDE/protocol.scala	Wed Mar 14 22:34:18 2012 +0100
     8.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 15 00:10:45 2012 +0100
     8.3 @@ -225,8 +225,10 @@
     8.4                // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
     8.5                val uses = deps.uses
     8.6                (Nil,
     8.7 -                triple(pair(symbol_string, symbol_string), list(symbol_string),
     8.8 -                    list(pair(symbol_string, bool)))((dir, name.theory), imports, uses)) },
     8.9 +                pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
    8.10 +                  list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
    8.11 +                    list(pair(symbol_string, bool)))(
    8.12 +                (((dir, name.theory), imports), deps.keywords), uses)) },
    8.13            { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
    8.14            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    8.15        def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
     9.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Mar 14 22:34:18 2012 +0100
     9.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Mar 15 00:10:45 2012 +0100
     9.3 @@ -21,7 +21,7 @@
     9.4  fun thy_begin text =
     9.5    (case try (Thy_Header.read Position.none) text of
     9.6      NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
     9.7 -  | SOME (name, imports, _) =>
     9.8 +  | SOME {name, imports, ...} =>
     9.9         D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
    9.10    :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    9.11  
    10.1 --- a/src/Pure/Thy/thy_header.ML	Wed Mar 14 22:34:18 2012 +0100
    10.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 00:10:45 2012 +0100
    10.3 @@ -6,40 +6,97 @@
    10.4  
    10.5  signature THY_HEADER =
    10.6  sig
    10.7 -  val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
    10.8 -  val read: Position.T -> string -> string * string list * (Path.T * bool) list
    10.9 +  type header =
   10.10 +   {name: string, imports: string list,
   10.11 +    keywords: (string * (string * string list) option) list,
   10.12 +    uses: (Path.T * bool) list}
   10.13 +  val make: string -> string list -> (string * (string * string list) option) list ->
   10.14 +    (Path.T * bool) list -> header
   10.15 +  val declare_keyword: string * (string * string list) option -> theory -> theory
   10.16 +  val the_keyword: theory -> string -> Keyword.T option
   10.17 +  val args: header parser
   10.18 +  val read: Position.T -> string -> header
   10.19  end;
   10.20  
   10.21  structure Thy_Header: THY_HEADER =
   10.22  struct
   10.23  
   10.24 -(* keywords *)
   10.25 +type header =
   10.26 + {name: string, imports: string list,
   10.27 +  keywords: (string * (string * string list) option) list,
   10.28 +  uses: (Path.T * bool) list};
   10.29 +
   10.30 +fun make name imports keywords uses : header =
   10.31 +  {name = name, imports = imports, keywords = keywords, uses = uses};
   10.32 +
   10.33 +
   10.34 +
   10.35 +(** keyword declarations **)
   10.36 +
   10.37 +fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
   10.38 +
   10.39 +structure Data = Theory_Data
   10.40 +(
   10.41 +  type T = Keyword.T option Symtab.table;
   10.42 +  val empty = Symtab.empty;
   10.43 +  val extend = I;
   10.44 +  fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
   10.45 +);
   10.46 +
   10.47 +fun declare_keyword (name, kind) =
   10.48 +  Data.map (fn data =>
   10.49 +    Symtab.update_new (name, Option.map Keyword.make kind) data
   10.50 +      handle Symtab.DUP name => err_dup name);
   10.51 +
   10.52 +fun the_keyword thy name =
   10.53 +  (case Symtab.lookup (Data.get thy) name of
   10.54 +    SOME decl => decl
   10.55 +  | NONE => error ("Unknown outer syntax keyword " ^ quote name));
   10.56 +
   10.57 +
   10.58 +
   10.59 +(** concrete syntax **)
   10.60 +
   10.61 +(* header keywords *)
   10.62  
   10.63  val headerN = "header";
   10.64  val theoryN = "theory";
   10.65  val importsN = "imports";
   10.66 +val keywordsN = "keywords";
   10.67  val usesN = "uses";
   10.68  val beginN = "begin";
   10.69  
   10.70 -val header_lexicon = Scan.make_lexicon
   10.71 -  (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
   10.72 +val header_lexicon =
   10.73 +  Scan.make_lexicon
   10.74 +    (map Symbol.explode
   10.75 +      ["%", "(", ")", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
   10.76  
   10.77  
   10.78  (* header args *)
   10.79  
   10.80 -val file_name = Parse.group (fn () => "file name") Parse.name;
   10.81 +local
   10.82 +
   10.83 +val file_name = Parse.group (fn () => "file name") Parse.path;
   10.84  val theory_name = Parse.group (fn () => "theory name") Parse.name;
   10.85  
   10.86 +val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
   10.87 +val keyword_decl = Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind);
   10.88 +
   10.89  val file =
   10.90    Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
   10.91    file_name >> rpair true;
   10.92  
   10.93 -val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
   10.94 +in
   10.95  
   10.96  val args =
   10.97 -  theory_name -- (Parse.$$$ importsN |--
   10.98 -    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
   10.99 -  >> Parse.triple2;
  10.100 +  theory_name --
  10.101 +  (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) --
  10.102 +  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! (Parse.and_list1 keyword_decl)) [] --
  10.103 +  Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
  10.104 +  Parse.$$$ beginN >>
  10.105 +  (fn (((name, imports), keywords), uses) => make name imports keywords uses);
  10.106 +
  10.107 +end;
  10.108  
  10.109  
  10.110  (* read header *)
  10.111 @@ -61,7 +118,7 @@
  10.112      |> Source.get_single;
  10.113    in
  10.114      (case res of
  10.115 -      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
  10.116 +      SOME (h, _) => h
  10.117      | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
  10.118    end;
  10.119  
    11.1 --- a/src/Pure/Thy/thy_header.scala	Wed Mar 14 22:34:18 2012 +0100
    11.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 00:10:45 2012 +0100
    11.3 @@ -20,10 +20,13 @@
    11.4    val HEADER = "header"
    11.5    val THEORY = "theory"
    11.6    val IMPORTS = "imports"
    11.7 +  val KEYWORDS = "keywords"
    11.8 +  val AND = "and"
    11.9    val USES = "uses"
   11.10    val BEGIN = "begin"
   11.11  
   11.12 -  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
   11.13 +  private val lexicon =
   11.14 +    Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
   11.15  
   11.16  
   11.17    /* theory file name */
   11.18 @@ -45,15 +48,26 @@
   11.19      val file_name = atom("file name", _.is_name)
   11.20      val theory_name = atom("theory name", _.is_name)
   11.21  
   11.22 +    val keyword_kind =
   11.23 +      atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
   11.24 +    val keyword_decl =
   11.25 +      name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
   11.26 +      { case x ~ y => (x, y) }
   11.27 +    val keywords =
   11.28 +      keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   11.29 +      { case x ~ ys => x :: ys }
   11.30 +
   11.31      val file =
   11.32        keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
   11.33        file_name ^^ (x => (x, true))
   11.34  
   11.35 -    val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
   11.36 -
   11.37      val args =
   11.38 -      theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
   11.39 -        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
   11.40 +      theory_name ~
   11.41 +      (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
   11.42 +      (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
   11.43 +      (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
   11.44 +      keyword(BEGIN) ^^
   11.45 +      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
   11.46  
   11.47      (keyword(HEADER) ~ tags) ~!
   11.48        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
   11.49 @@ -98,9 +112,11 @@
   11.50  
   11.51  
   11.52  sealed case class Thy_Header(
   11.53 -  val name: String, val imports: List[String], val uses: List[(String, Boolean)])
   11.54 +  name: String, imports: List[String],
   11.55 +  keywords: List[(String, Option[(String, List[String])])],
   11.56 +  uses: List[(String, Boolean)])
   11.57  {
   11.58    def map(f: String => String): Thy_Header =
   11.59 -    Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
   11.60 +    Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))
   11.61  }
   11.62  
    12.1 --- a/src/Pure/Thy/thy_info.ML	Wed Mar 14 22:34:18 2012 +0100
    12.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Mar 15 00:10:45 2012 +0100
    12.3 @@ -21,7 +21,7 @@
    12.4    val use_thys_wrt: Path.T -> string list -> unit
    12.5    val use_thys: string list -> unit
    12.6    val use_thy: string -> unit
    12.7 -  val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
    12.8 +  val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
    12.9    val register_thy: theory -> unit
   12.10    val finish: unit -> unit
   12.11  end;
   12.12 @@ -233,9 +233,10 @@
   12.13      val {master = (thy_path, _), imports} = deps;
   12.14      val dir = Path.dir thy_path;
   12.15      val pos = Path.position thy_path;
   12.16 -    val (_, _, uses) = Thy_Header.read pos text;
   12.17 +    val {uses, keywords, ...} = Thy_Header.read pos text;
   12.18 +    val header = Thy_Header.make name imports keywords uses;
   12.19  
   12.20 -    val (theory, present) = Thy_Load.load_thy update_time dir name imports uses pos text parents;
   12.21 +    val (theory, present) = Thy_Load.load_thy update_time dir header pos text parents;
   12.22      fun commit () = update_thy deps theory;
   12.23    in (theory, present, commit) end;
   12.24  
   12.25 @@ -308,12 +309,13 @@
   12.26  
   12.27  (* toplevel begin theory -- without maintaining database *)
   12.28  
   12.29 -fun toplevel_begin_theory dir name imports uses =
   12.30 +fun toplevel_begin_theory dir (header: Thy_Header.header) =
   12.31    let
   12.32 +    val {name, imports, ...} = header;
   12.33      val _ = kill_thy name;
   12.34      val _ = use_thys_wrt dir imports;
   12.35      val parents = map (get_theory o base_name) imports;
   12.36 -  in Thy_Load.begin_theory dir name imports uses parents end;
   12.37 +  in Thy_Load.begin_theory dir header parents end;
   12.38  
   12.39  
   12.40  (* register theory *)
    13.1 --- a/src/Pure/Thy/thy_load.ML	Wed Mar 14 22:34:18 2012 +0100
    13.2 +++ b/src/Pure/Thy/thy_load.ML	Thu Mar 15 00:10:45 2012 +0100
    13.3 @@ -19,10 +19,9 @@
    13.4    val all_current: theory -> bool
    13.5    val use_ml: Path.T -> unit
    13.6    val exec_ml: Path.T -> generic_theory -> generic_theory
    13.7 -  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list ->
    13.8 -    theory list -> theory
    13.9 -  val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list ->
   13.10 -    Position.T -> string -> theory list -> theory * unit future
   13.11 +  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   13.12 +  val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
   13.13 +    theory list -> theory * unit future
   13.14    val set_master_path: Path.T -> unit
   13.15    val get_master_path: unit -> Path.T
   13.16  end;
   13.17 @@ -85,7 +84,9 @@
   13.18      val text = File.read master_file;
   13.19      val (name', imports, uses) =
   13.20        if name = Context.PureN then (Context.PureN, [], [])
   13.21 -      else Thy_Header.read (Path.position master_file) text;
   13.22 +      else
   13.23 +        let val {name, imports, uses, ...} = Thy_Header.read (Path.position master_file) text
   13.24 +        in (name, imports, uses) end;
   13.25      val _ = name <> name' andalso
   13.26        error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
   13.27    in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
   13.28 @@ -159,21 +160,23 @@
   13.29  
   13.30  (* load_thy *)
   13.31  
   13.32 -fun begin_theory dir name imports uses parents =
   13.33 +fun begin_theory dir {name, imports, keywords, uses} parents =
   13.34    Theory.begin_theory name parents
   13.35    |> put_deps dir imports
   13.36 +  |> fold Thy_Header.declare_keyword keywords
   13.37    |> fold (require o fst) uses
   13.38    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   13.39    |> Theory.checkpoint;
   13.40  
   13.41 -fun load_thy update_time dir name imports uses pos text parents =
   13.42 +fun load_thy update_time dir header pos text parents =
   13.43    let
   13.44      val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
   13.45      val time = ! Toplevel.timing;
   13.46  
   13.47 +    val {name, imports, uses, ...} = header;
   13.48      val _ = Present.init_theory name;
   13.49      fun init () =
   13.50 -      begin_theory dir name imports uses parents
   13.51 +      begin_theory dir header parents
   13.52        |> Present.begin_theory update_time dir uses;
   13.53  
   13.54      val toks = Thy_Syntax.parse_tokens lexs pos text;
    14.1 --- a/src/Pure/Thy/thy_load.scala	Wed Mar 14 22:34:18 2012 +0100
    14.2 +++ b/src/Pure/Thy/thy_load.scala	Thu Mar 15 00:10:45 2012 +0100
    14.3 @@ -61,7 +61,7 @@
    14.4      val uses = header.uses
    14.5      if (name.theory != name1)
    14.6        error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
    14.7 -    Document.Node.Deps(imports, uses)
    14.8 +    Document.Node.Deps(imports, header.keywords, uses)
    14.9    }
   14.10  
   14.11    def check_thy(name: Document.Node.Name): Document.Node.Deps =