# HG changeset patch # User wenzelm # Date 1345464549 -7200 # Node ID 3ee314ae1e0abb9bd7a65d3448371ad57e78c385 # Parent 881e8a96e617413e0342fe4e702421122eb16798 added keyword kind "thy_load" (with optional list of file extensions); diff -r 881e8a96e617 -r 3ee314ae1e0a lib/scripts/keywords --- 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", diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/Isar/keyword.ML --- 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, diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/Isar/outer_syntax.ML --- 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 => diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/Isar/outer_syntax.scala --- 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 = diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/ML/ml_antiquote.ML --- 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) => diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/PIDE/protocol.ML --- 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) diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/PIDE/protocol.scala --- 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) })) diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/ProofGeneral/pgip_parser.ML --- 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 diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/System/build.scala --- 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)) diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/Thy/thy_header.ML --- 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 = diff -r 881e8a96e617 -r 3ee314ae1e0a src/Pure/Thy/thy_header.scala --- 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])])] }