--- a/lib/scripts/keywords Mon Aug 20 13:58:06 2012 +0200
+++ b/lib/scripts/keywords Mon Aug 20 14:09:09 2012 +0200
@@ -37,6 +37,7 @@
"thy_heading2" => "theory-heading",
"thy_heading3" => "theory-heading",
"thy_heading4" => "theory-heading",
+ "thy_load" => "theory-decl",
"thy_decl" => "theory-decl",
"thy_script" => "theory-script",
"thy_goal" => "theory-goal",
--- a/src/Pure/Isar/keyword.ML Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Aug 20 14:09:09 2012 +0200
@@ -8,6 +8,7 @@
sig
type T
val kind_of: T -> string
+ val kind_files_of: T -> string * string list
val control: T
val diag: T
val thy_begin: T
@@ -17,6 +18,8 @@
val thy_heading3: T
val thy_heading4: T
val thy_decl: T
+ val thy_load: T
+ val thy_load_files: string list -> T
val thy_script: T
val thy_goal: T
val thy_schematic_goal: T
@@ -41,7 +44,7 @@
val tag_theory: T -> T
val tag_proof: T -> T
val tag_ml: T -> T
- type spec = string * string list
+ type spec = (string * string list) * string list
val spec: spec -> T
val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
@@ -70,10 +73,17 @@
(** keyword classification **)
-datatype T = Keyword of string * string list; (*kind, tags (in canonical reverse order)*)
+datatype T = Keyword of
+ {kind: string,
+ files: string list, (*extensions of embedded files*)
+ tags: string list}; (*tags in canonical reverse order*)
-fun kind s = Keyword (s, []);
-fun kind_of (Keyword (s, _)) = s;
+fun kind s = Keyword {kind = s, files = [], tags = []};
+fun kind_of (Keyword {kind, ...}) = kind;
+fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);
+
+fun add_files fs (Keyword {kind, files, tags}) =
+ Keyword {kind = kind, files = files @ fs, tags = tags};
(* kinds *)
@@ -86,6 +96,8 @@
val thy_heading2 = kind "thy_heading2";
val thy_heading3 = kind "thy_heading3";
val thy_heading4 = kind "thy_heading4";
+val thy_load = kind "thy_load";
+fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
val thy_decl = kind "thy_decl";
val thy_script = kind "thy_script";
val thy_goal = kind "thy_goal";
@@ -108,15 +120,16 @@
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
+ thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
(* tags *)
-fun tag t (Keyword (s, ts)) = Keyword (s, update (op =) t ts);
-fun tags_of (Keyword (_, ts)) = ts;
+fun tag t (Keyword {kind, files, tags}) =
+ Keyword {kind = kind, files = files, tags = update (op =) t tags};
+fun tags_of (Keyword {tags, ...}) = tags;
val tag_theory = tag "theory";
val tag_proof = tag "proof";
@@ -127,12 +140,17 @@
val name_table = Symtab.make (map (`kind_of) kinds);
-type spec = string * string list;
+type spec = (string * string list) * string list;
-fun spec (kind, tags) =
- (case Symtab.lookup name_table kind of
- SOME k => k |> fold tag tags
- | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
+fun spec ((name, files), tags) =
+ (case Symtab.lookup name_table name of
+ SOME kind =>
+ let val kind' = kind |> fold tag tags in
+ if null files then kind'
+ else if name = kind_of thy_load then kind' |> add_files files
+ else error ("Illegal specification of files for " ^ quote name)
+ end
+ | NONE => error ("Unknown outer syntax keyword kind " ^ quote name));
fun command_spec ((name, s), pos) = ((name, spec s), pos);
@@ -226,7 +244,7 @@
val is_theory = command_category
[thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_decl, thy_script, thy_goal, thy_schematic_goal];
+ thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal];
val is_proof = command_category
[qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
--- a/src/Pure/Isar/outer_syntax.ML Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Aug 20 14:09:09 2012 +0200
@@ -139,7 +139,7 @@
val _ =
(case try (Thy_Header.the_keyword thy) name of
SOME spec =>
- if Option.map #1 spec = SOME (Keyword.kind_of kind) then ()
+ if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
else error ("Inconsistent outer syntax keyword declaration " ^
quote name ^ Position.str_of pos)
| NONE =>
--- a/src/Pure/Isar/outer_syntax.scala Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Mon Aug 20 14:09:09 2012 +0200
@@ -39,25 +39,29 @@
}
final class Outer_Syntax private(
- keywords: Map[String, String] = Map.empty,
+ keywords: Map[String, (String, List[String])] = Map.empty,
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.empty)
{
override def toString: String =
- (for ((name, kind) <- keywords) yield {
+ (for ((name, (kind, files)) <- keywords) yield {
if (kind == Keyword.MINOR) quote(name)
- else quote(name) + " :: " + quote(kind)
+ else
+ quote(name) + " :: " + quote(kind) +
+ (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
}).toList.sorted.mkString("keywords\n ", " and\n ", "")
- def keyword_kind(name: String): Option[String] = keywords.get(name)
+ def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
+ def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
- def + (name: String, kind: String, replace: String): Outer_Syntax =
+ def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
new Outer_Syntax(
keywords + (name -> kind),
lexicon + name,
- if (Keyword.control(kind)) completion else completion + (name, replace))
+ if (Keyword.control(kind._1)) completion else completion + (name, replace))
- def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
+ def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, name)
+ def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
def add_keywords(header: Document.Node.Header): Outer_Syntax =
--- a/src/Pure/ML/ml_antiquote.ML Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Mon Aug 20 14:09:09 2012 +0200
@@ -210,7 +210,9 @@
"Keyword.command_spec " ^ ML_Syntax.atomic
((ML_Syntax.print_pair
(ML_Syntax.print_pair ML_Syntax.print_string
- (ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_pair
+ (ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_list ML_Syntax.print_string))
(ML_Syntax.print_list ML_Syntax.print_string)))
ML_Syntax.print_position) ((name, kind), pos))
| ((name, NONE), pos) =>
--- a/src/Pure/PIDE/protocol.ML Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Aug 20 14:09:09 2012 +0200
@@ -39,7 +39,8 @@
let
val (master, (name, (imports, (keywords, (uses, errors))))) =
pair string (pair string (pair (list string)
- (pair (list (pair string (option (pair string (list string)))))
+ (pair (list (pair string
+ (option (pair (pair string (list string)) (list string)))))
(pair (list (pair string bool)) (list string))))) a;
val (uses', errors') =
(map (apfst Path.explode) uses, errors)
--- a/src/Pure/PIDE/protocol.scala Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Aug 20 14:09:09 2012 +0200
@@ -222,7 +222,8 @@
val uses = header.uses
(Nil,
pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
- pair(list(pair(Encode.string, option(pair(Encode.string, list(Encode.string))))),
+ pair(list(pair(Encode.string,
+ option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
(dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
--- a/src/Pure/ProofGeneral/pgip_parser.ML Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Mon Aug 20 14:09:09 2012 +0200
@@ -61,6 +61,7 @@
|> command Keyword.thy_heading2 thy_heading
|> command Keyword.thy_heading3 thy_heading
|> command Keyword.thy_heading4 thy_heading
+ |> command Keyword.thy_load thy_decl
|> command Keyword.thy_decl thy_decl
|> command Keyword.thy_script thy_decl
|> command Keyword.thy_goal goal
--- a/src/Pure/System/build.scala Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/System/build.scala Mon Aug 20 14:09:09 2012 +0200
@@ -341,8 +341,8 @@
Outer_Syntax.init() +
// FIXME avoid hardwired stuff!?
("theory", Keyword.THY_BEGIN) +
- ("hence", Keyword.PRF_ASM_GOAL, "then have") +
- ("thus", Keyword.PRF_ASM_GOAL, "then show")
+ ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
+ ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
(Set.empty[String], init_syntax, Nil)
}
val thy_info = new Thy_Info(new Thy_Load(preloaded))
--- a/src/Pure/Thy/thy_header.ML Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Aug 20 14:09:09 2012 +0200
@@ -39,7 +39,7 @@
fun define_keywords ({keywords, ...}: header) =
List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
-fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
+fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
structure Data = Theory_Data
(
@@ -75,7 +75,7 @@
val header_lexicon =
Scan.make_lexicon
(map Symbol.explode
- ["%", "(", ")", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
+ ["%", "(", ")", ",", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
(* header args *)
@@ -85,10 +85,15 @@
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 opt_files =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
+val keyword_spec =
+ Parse.group (fn () => "outer syntax keyword specification")
+ (Parse.name -- opt_files -- Parse.tags);
+
val keyword_decl =
- Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
- (fn (names, kind) => map (rpair kind) names);
+ Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) >>
+ (fn (names, spec) => map (rpair spec) names);
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
val file =
--- a/src/Pure/Thy/thy_header.scala Mon Aug 20 13:58:06 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Aug 20 14:09:09 2012 +0200
@@ -26,7 +26,7 @@
val BEGIN = "begin"
private val lexicon =
- Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
+ Scan.Lexicon("%", "(", ")", ",", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
/* theory file name */
@@ -47,10 +47,15 @@
{
val file_name = atom("file name", _.is_name)
- val keyword_kind =
- atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
+ val opt_files =
+ keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
+ success(Nil)
+ val keyword_spec =
+ atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
+ { case x ~ y ~ z => ((x, y), z) }
+
val keyword_decl =
- rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
+ rep1(string) ~ opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
{ case xs ~ y => xs.map((_, y)) }
val keyword_decls =
keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
@@ -111,7 +116,7 @@
/* keywords */
- type Keywords = List[(String, Option[(String, List[String])])]
+ type Keywords = List[(String, Option[((String, List[String]), List[String])])]
}