some support for outer syntax keyword declarations within theory header;
more uniform Thy_Header.header as argument for begin_theory etc.;

--- a/etc/isar-keywords-ZF.el	Wed Mar 14 22:34:18 2012 +0100
+++ b/etc/isar-keywords-ZF.el	Thu Mar 15 00:10:45 2012 +0100
@@ -229,6 +229,7 @@
     "infixr"
     "intros"
     "is"
+    "keywords"
     "monos"
     "notes"
     "obtains"

--- a/etc/isar-keywords.el	Wed Mar 14 22:34:18 2012 +0100
+++ b/etc/isar-keywords.el	Thu Mar 15 00:10:45 2012 +0100
@@ -305,6 +305,7 @@
     "infixl"
     "infixr"
     "is"
+    "keywords"
     "lazy"
     "module_name"
     "monos"

--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -18,7 +18,7 @@
   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   "advanced", "and", "assumes", "attach", "begin", "binder",
   "constrains", "defines", "fixes", "for", "identifier", "if",
-  "imports", "in", "infix", "infixl", "infixr", "is",
+  "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
   "notes", "obtains", "open", "output", "overloaded", "pervasive",
   "shows", "structure", "unchecked", "uses", "where", "|"];
 
@@ -28,12 +28,10 @@
 
 val _ =
   Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
-    (Thy_Header.args >> (fn (name, imports, uses) =>
+    (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
-          (fn () =>
-            Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
-              name imports (map (apfst Path.explode) uses))));
+          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
 
 val _ =
   Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)

--- a/src/Pure/Isar/keyword.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -37,6 +37,7 @@
   val tag_theory: T -> T
   val tag_proof: T -> T
   val tag_ml: T -> T
+  val make: string * string list -> T
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
   val dest_keywords: unit -> string list
@@ -115,6 +116,39 @@
 val tag_ml = tag "ML";
 
 
+(* external names *)
+
+val name_table = Symtab.make
+  [("control",            control),
+   ("diag",               diag),
+   ("thy_begin",          thy_begin),
+   ("thy_switch",         thy_switch),
+   ("thy_end",            thy_end),
+   ("thy_heading",        thy_heading),
+   ("thy_decl",           thy_decl),
+   ("thy_script",         thy_script),
+   ("thy_goal",           thy_goal),
+   ("thy_schematic_goal", thy_schematic_goal),
+   ("qed",                qed),
+   ("qed_block",          qed_block),
+   ("qed_global",         qed_global),
+   ("prf_heading",        prf_heading),
+   ("prf_goal",           prf_goal),
+   ("prf_block",          prf_block),
+   ("prf_open",           prf_open),
+   ("prf_close",          prf_close),
+   ("prf_chain",          prf_chain),
+   ("prf_decl",           prf_decl),
+   ("prf_asm",            prf_asm),
+   ("prf_asm_goal",       prf_asm_goal),
+   ("prf_script",         prf_script)];
+
+fun make (kind, tags) =
+  (case Symtab.lookup name_table kind of
+    SOME k => k |> fold tag tags
+  | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
+
+
 
 (** global keyword tables **)
 

--- a/src/Pure/PIDE/document.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -15,7 +15,7 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
-  type node_header = ((string * string) * string list * (string * bool) list) Exn.result
+  type node_header = (string * Thy_Header.header) Exn.result
   datatype node_edit =
     Clear |
     Edits of (command_id option * command_id option) list |
@@ -58,7 +58,7 @@
 
 (** document structure **)
 
-type node_header = ((string * string) * string list * (string * bool) list) Exn.result;
+type node_header = (string * Thy_Header.header) Exn.result;
 type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
@@ -212,7 +212,7 @@
         |> touch_node name
     | Header header =>
         let
-          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
+          val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
           val nodes1 = nodes
             |> default_node name
             |> fold default_node imports;
@@ -307,7 +307,6 @@
 end;
 
 
-
 (* toplevel transactions *)
 
 local
@@ -447,16 +446,15 @@
 fun init_theory deps node =
   let
     (* FIXME provide files via Scala layer, not master_dir *)
-    val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node);
-    val files = map (apfst Path.explode) uses;
+    val (master_dir, header) = Exn.release (get_header node);
     val parents =
-      imports |> map (fn import =>
+      #imports header |> map (fn import =>
         (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
           SOME thy => thy
         | NONE =>
             get_theory (Position.file_only import)
               (snd (Future.join (the (AList.lookup (op =) deps import))))));
-  in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end;
+  in Thy_Load.begin_theory (Path.explode master_dir) header parents end;
 
 in
 

--- a/src/Pure/PIDE/document.scala	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 15 00:10:45 2012 +0100
@@ -39,7 +39,10 @@
 
   object Node
   {
-    sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)])
+    sealed case class Deps(
+      imports: List[Name],
+      keywords: List[(String, Option[(String, List[String])])],
+      uses: List[(String, Boolean)])
 
     object Name
     {

--- a/src/Pure/PIDE/protocol.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -46,9 +46,16 @@
                  [fn ([], []) => Document.Clear,
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
-                    Document.Header
-                      (Exn.Res
-                        (triple (pair string string) (list string) (list (pair string bool)) a)),
+                    let
+                      val ((((master, name), imports), keywords), uses) =
+                        pair (pair (pair (pair string string) (list string))
+                          (list (pair string (option (pair string (list string))))))
+                          (list (pair string bool)) a;
+                      val res =
+                        Exn.capture (fn () =>
+                          (master, Thy_Header.make name imports keywords
+                            (map (apfst Path.explode) uses))) ();
+                    in Document.Header res end,
                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;

--- a/src/Pure/PIDE/protocol.scala	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Mar 15 00:10:45 2012 +0100
@@ -225,8 +225,10 @@
               // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
               val uses = deps.uses
               (Nil,
-                triple(pair(symbol_string, symbol_string), list(symbol_string),
-                    list(pair(symbol_string, bool)))((dir, name.theory), imports, uses)) },
+                pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
+                  list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
+                    list(pair(symbol_string, bool)))(
+                (((dir, name.theory), imports), deps.keywords), uses)) },
           { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
           { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
       def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>

--- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -21,7 +21,7 @@
 fun thy_begin text =
   (case try (Thy_Header.read Position.none) text of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
-  | SOME (name, imports, _) =>
+  | SOME {name, imports, ...} =>
        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
   :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
 

--- a/src/Pure/Thy/thy_header.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -6,40 +6,97 @@
 
 signature THY_HEADER =
 sig
-  val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
-  val read: Position.T -> string -> string * string list * (Path.T * bool) list
+  type header =
+   {name: string, imports: string list,
+    keywords: (string * (string * string list) option) list,
+    uses: (Path.T * bool) list}
+  val make: string -> string list -> (string * (string * string list) option) list ->
+    (Path.T * bool) list -> header
+  val declare_keyword: string * (string * string list) option -> theory -> theory
+  val the_keyword: theory -> string -> Keyword.T option
+  val args: header parser
+  val read: Position.T -> string -> header
 end;
 
 structure Thy_Header: THY_HEADER =
 struct
 
-(* keywords *)
+type header =
+ {name: string, imports: string list,
+  keywords: (string * (string * string list) option) list,
+  uses: (Path.T * bool) list};
+
+fun make name imports keywords uses : header =
+  {name = name, imports = imports, keywords = keywords, uses = uses};
+
+
+
+(** keyword declarations **)
+
+fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
+
+structure Data = Theory_Data
+(
+  type T = Keyword.T option Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
+);
+
+fun declare_keyword (name, kind) =
+  Data.map (fn data =>
+    Symtab.update_new (name, Option.map Keyword.make kind) data
+      handle Symtab.DUP name => err_dup name);
+
+fun the_keyword thy name =
+  (case Symtab.lookup (Data.get thy) name of
+    SOME decl => decl
+  | NONE => error ("Unknown outer syntax keyword " ^ quote name));
+
+
+
+(** concrete syntax **)
+
+(* header keywords *)
 
 val headerN = "header";
 val theoryN = "theory";
 val importsN = "imports";
+val keywordsN = "keywords";
 val usesN = "uses";
 val beginN = "begin";
 
-val header_lexicon = Scan.make_lexicon
-  (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
+val header_lexicon =
+  Scan.make_lexicon
+    (map Symbol.explode
+      ["%", "(", ")", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
 
 
 (* header args *)
 
-val file_name = Parse.group (fn () => "file name") Parse.name;
+local
+
+val file_name = Parse.group (fn () => "file name") Parse.path;
 val theory_name = Parse.group (fn () => "theory name") Parse.name;
 
+val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
+val keyword_decl = Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind);
+
 val file =
   Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
   file_name >> rpair true;
 
-val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
+in
 
 val args =
-  theory_name -- (Parse.$$$ importsN |--
-    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
-  >> Parse.triple2;
+  theory_name --
+  (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) --
+  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! (Parse.and_list1 keyword_decl)) [] --
+  Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
+  Parse.$$$ beginN >>
+  (fn (((name, imports), keywords), uses) => make name imports keywords uses);
+
+end;
 
 
 (* read header *)
@@ -61,7 +118,7 @@
     |> Source.get_single;
   in
     (case res of
-      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
+      SOME (h, _) => h
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 

--- a/src/Pure/Thy/thy_header.scala	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 00:10:45 2012 +0100
@@ -20,10 +20,13 @@
   val HEADER = "header"
   val THEORY = "theory"
   val IMPORTS = "imports"
+  val KEYWORDS = "keywords"
+  val AND = "and"
   val USES = "uses"
   val BEGIN = "begin"
 
-  private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
+  private val lexicon =
+    Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
 
 
   /* theory file name */
@@ -45,15 +48,26 @@
     val file_name = atom("file name", _.is_name)
     val theory_name = atom("theory name", _.is_name)
 
+    val keyword_kind =
+      atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
+    val keyword_decl =
+      name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
+      { case x ~ y => (x, y) }
+    val keywords =
+      keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
+      { case x ~ ys => x :: ys }
+
     val file =
       keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
       file_name ^^ (x => (x, true))
 
-    val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
-
     val args =
-      theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
-        { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
+      theory_name ~
+      (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
+      (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
+      keyword(BEGIN) ^^
+      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
 
     (keyword(HEADER) ~ tags) ~!
       ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
@@ -98,9 +112,11 @@
 
 
 sealed case class Thy_Header(
-  val name: String, val imports: List[String], val uses: List[(String, Boolean)])
+  name: String, imports: List[String],
+  keywords: List[(String, Option[(String, List[String])])],
+  uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =
-    Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
+    Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))
 }
 

--- a/src/Pure/Thy/thy_info.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -21,7 +21,7 @@
   val use_thys_wrt: Path.T -> string list -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
-  val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
+  val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
@@ -233,9 +233,10 @@
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
-    val (_, _, uses) = Thy_Header.read pos text;
+    val {uses, keywords, ...} = Thy_Header.read pos text;
+    val header = Thy_Header.make name imports keywords uses;
 
-    val (theory, present) = Thy_Load.load_thy update_time dir name imports uses pos text parents;
+    val (theory, present) = Thy_Load.load_thy update_time dir header pos text parents;
     fun commit () = update_thy deps theory;
   in (theory, present, commit) end;
 
@@ -308,12 +309,13 @@
 
 (* toplevel begin theory -- without maintaining database *)
 
-fun toplevel_begin_theory dir name imports uses =
+fun toplevel_begin_theory dir (header: Thy_Header.header) =
   let
+    val {name, imports, ...} = header;
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
     val parents = map (get_theory o base_name) imports;
-  in Thy_Load.begin_theory dir name imports uses parents end;
+  in Thy_Load.begin_theory dir header parents end;
 
 
 (* register theory *)

--- a/src/Pure/Thy/thy_load.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -19,10 +19,9 @@
   val all_current: theory -> bool
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
-  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list ->
-    theory list -> theory
-  val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list ->
-    Position.T -> string -> theory list -> theory * unit future
+  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
+  val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
+    theory list -> theory * unit future
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
 end;
@@ -85,7 +84,9 @@
     val text = File.read master_file;
     val (name', imports, uses) =
       if name = Context.PureN then (Context.PureN, [], [])
-      else Thy_Header.read (Path.position master_file) text;
+      else
+        let val {name, imports, uses, ...} = Thy_Header.read (Path.position master_file) text
+        in (name, imports, uses) end;
     val _ = name <> name' andalso
       error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
   in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
@@ -159,21 +160,23 @@
 
 (* load_thy *)
 
-fun begin_theory dir name imports uses parents =
+fun begin_theory dir {name, imports, keywords, uses} parents =
   Theory.begin_theory name parents
   |> put_deps dir imports
+  |> fold Thy_Header.declare_keyword keywords
   |> fold (require o fst) uses
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
 
-fun load_thy update_time dir name imports uses pos text parents =
+fun load_thy update_time dir header pos text parents =
   let
     val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
     val time = ! Toplevel.timing;
 
+    val {name, imports, uses, ...} = header;
     val _ = Present.init_theory name;
     fun init () =
-      begin_theory dir name imports uses parents
+      begin_theory dir header parents
       |> Present.begin_theory update_time dir uses;
 
     val toks = Thy_Syntax.parse_tokens lexs pos text;

--- a/src/Pure/Thy/thy_load.scala	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Thu Mar 15 00:10:45 2012 +0100
@@ -61,7 +61,7 @@
     val uses = header.uses
     if (name.theory != name1)
       error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
-    Document.Node.Deps(imports, uses)
+    Document.Node.Deps(imports, header.keywords, uses)
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Deps =