added keyword kind "thy_load" (with optional list of file extensions);
authorwenzelm
Mon Aug 20 14:09:09 2012 +0200 (2012-08-20)
changeset 488643ee314ae1e0a
parent 48863 881e8a96e617
child 48865 9824fd676bf4
added keyword kind "thy_load" (with optional list of file extensions);
lib/scripts/keywords
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/outer_syntax.scala
src/Pure/ML/ml_antiquote.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/System/build.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/lib/scripts/keywords	Mon Aug 20 13:58:06 2012 +0200
     1.2 +++ b/lib/scripts/keywords	Mon Aug 20 14:09:09 2012 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    "thy_heading2" => "theory-heading",
     1.5    "thy_heading3" => "theory-heading",
     1.6    "thy_heading4" => "theory-heading",
     1.7 +  "thy_load" => "theory-decl",
     1.8    "thy_decl" => "theory-decl",
     1.9    "thy_script" => "theory-script",
    1.10    "thy_goal" => "theory-goal",
     2.1 --- a/src/Pure/Isar/keyword.ML	Mon Aug 20 13:58:06 2012 +0200
     2.2 +++ b/src/Pure/Isar/keyword.ML	Mon Aug 20 14:09:09 2012 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4  sig
     2.5    type T
     2.6    val kind_of: T -> string
     2.7 +  val kind_files_of: T -> string * string list
     2.8    val control: T
     2.9    val diag: T
    2.10    val thy_begin: T
    2.11 @@ -17,6 +18,8 @@
    2.12    val thy_heading3: T
    2.13    val thy_heading4: T
    2.14    val thy_decl: T
    2.15 +  val thy_load: T
    2.16 +  val thy_load_files: string list -> T
    2.17    val thy_script: T
    2.18    val thy_goal: T
    2.19    val thy_schematic_goal: T
    2.20 @@ -41,7 +44,7 @@
    2.21    val tag_theory: T -> T
    2.22    val tag_proof: T -> T
    2.23    val tag_ml: T -> T
    2.24 -  type spec = string * string list
    2.25 +  type spec = (string * string list) * string list
    2.26    val spec: spec -> T
    2.27    val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
    2.28    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
    2.29 @@ -70,10 +73,17 @@
    2.30  
    2.31  (** keyword classification **)
    2.32  
    2.33 -datatype T = Keyword of string * string list;  (*kind, tags (in canonical reverse order)*)
    2.34 +datatype T = Keyword of
    2.35 + {kind: string,
    2.36 +  files: string list,  (*extensions of embedded files*)
    2.37 +  tags: string list};  (*tags in canonical reverse order*)
    2.38  
    2.39 -fun kind s = Keyword (s, []);
    2.40 -fun kind_of (Keyword (s, _)) = s;
    2.41 +fun kind s = Keyword {kind = s, files = [], tags = []};
    2.42 +fun kind_of (Keyword {kind, ...}) = kind;
    2.43 +fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);
    2.44 +
    2.45 +fun add_files fs (Keyword {kind, files, tags}) =
    2.46 +  Keyword {kind = kind, files = files @ fs, tags = tags};
    2.47  
    2.48  
    2.49  (* kinds *)
    2.50 @@ -86,6 +96,8 @@
    2.51  val thy_heading2 = kind "thy_heading2";
    2.52  val thy_heading3 = kind "thy_heading3";
    2.53  val thy_heading4 = kind "thy_heading4";
    2.54 +val thy_load = kind "thy_load";
    2.55 +fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
    2.56  val thy_decl = kind "thy_decl";
    2.57  val thy_script = kind "thy_script";
    2.58  val thy_goal = kind "thy_goal";
    2.59 @@ -108,15 +120,16 @@
    2.60  
    2.61  val kinds =
    2.62    [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    2.63 -    thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
    2.64 +    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
    2.65      prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    2.66      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    2.67  
    2.68  
    2.69  (* tags *)
    2.70  
    2.71 -fun tag t (Keyword (s, ts)) = Keyword (s, update (op =) t ts);
    2.72 -fun tags_of (Keyword (_, ts)) = ts;
    2.73 +fun tag t (Keyword {kind, files, tags}) =
    2.74 +  Keyword {kind = kind, files = files, tags = update (op =) t tags};
    2.75 +fun tags_of (Keyword {tags, ...}) = tags;
    2.76  
    2.77  val tag_theory = tag "theory";
    2.78  val tag_proof = tag "proof";
    2.79 @@ -127,12 +140,17 @@
    2.80  
    2.81  val name_table = Symtab.make (map (`kind_of) kinds);
    2.82  
    2.83 -type spec = string * string list;
    2.84 +type spec = (string * string list) * string list;
    2.85  
    2.86 -fun spec (kind, tags) =
    2.87 -  (case Symtab.lookup name_table kind of
    2.88 -    SOME k => k |> fold tag tags
    2.89 -  | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
    2.90 +fun spec ((name, files), tags) =
    2.91 +  (case Symtab.lookup name_table name of
    2.92 +    SOME kind =>
    2.93 +      let val kind' = kind |> fold tag tags in
    2.94 +        if null files then kind'
    2.95 +        else if name = kind_of thy_load then kind' |> add_files files
    2.96 +        else error ("Illegal specification of files for " ^ quote name)
    2.97 +      end
    2.98 +  | NONE => error ("Unknown outer syntax keyword kind " ^ quote name));
    2.99  
   2.100  fun command_spec ((name, s), pos) = ((name, spec s), pos);
   2.101  
   2.102 @@ -226,7 +244,7 @@
   2.103  
   2.104  val is_theory = command_category
   2.105    [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
   2.106 -    thy_decl, thy_script, thy_goal, thy_schematic_goal];
   2.107 +    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal];
   2.108  
   2.109  val is_proof = command_category
   2.110    [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 20 13:58:06 2012 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 20 14:09:09 2012 +0200
     3.3 @@ -139,7 +139,7 @@
     3.4      val _ =
     3.5        (case try (Thy_Header.the_keyword thy) name of
     3.6          SOME spec =>
     3.7 -          if Option.map #1 spec = SOME (Keyword.kind_of kind) then ()
     3.8 +          if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
     3.9            else error ("Inconsistent outer syntax keyword declaration " ^
    3.10              quote name ^ Position.str_of pos)
    3.11        | NONE =>
     4.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 20 13:58:06 2012 +0200
     4.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Aug 20 14:09:09 2012 +0200
     4.3 @@ -39,25 +39,29 @@
     4.4  }
     4.5  
     4.6  final class Outer_Syntax private(
     4.7 -  keywords: Map[String, String] = Map.empty,
     4.8 +  keywords: Map[String, (String, List[String])] = Map.empty,
     4.9    lexicon: Scan.Lexicon = Scan.Lexicon.empty,
    4.10    val completion: Completion = Completion.empty)
    4.11  {
    4.12    override def toString: String =
    4.13 -    (for ((name, kind) <- keywords) yield {
    4.14 +    (for ((name, (kind, files)) <- keywords) yield {
    4.15        if (kind == Keyword.MINOR) quote(name)
    4.16 -      else quote(name) + " :: " + quote(kind)
    4.17 +      else
    4.18 +        quote(name) + " :: " + quote(kind) +
    4.19 +        (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
    4.20      }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
    4.21  
    4.22 -  def keyword_kind(name: String): Option[String] = keywords.get(name)
    4.23 +  def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
    4.24 +  def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
    4.25  
    4.26 -  def + (name: String, kind: String, replace: String): Outer_Syntax =
    4.27 +  def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
    4.28      new Outer_Syntax(
    4.29        keywords + (name -> kind),
    4.30        lexicon + name,
    4.31 -      if (Keyword.control(kind)) completion else completion + (name, replace))
    4.32 +      if (Keyword.control(kind._1)) completion else completion + (name, replace))
    4.33  
    4.34 -  def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    4.35 +  def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, name)
    4.36 +  def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
    4.37    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    4.38  
    4.39    def add_keywords(header: Document.Node.Header): Outer_Syntax =
     5.1 --- a/src/Pure/ML/ml_antiquote.ML	Mon Aug 20 13:58:06 2012 +0200
     5.2 +++ b/src/Pure/ML/ml_antiquote.ML	Mon Aug 20 14:09:09 2012 +0200
     5.3 @@ -210,7 +210,9 @@
     5.4            "Keyword.command_spec " ^ ML_Syntax.atomic
     5.5              ((ML_Syntax.print_pair
     5.6                (ML_Syntax.print_pair ML_Syntax.print_string
     5.7 -                (ML_Syntax.print_pair ML_Syntax.print_string
     5.8 +                (ML_Syntax.print_pair
     5.9 +                  (ML_Syntax.print_pair ML_Syntax.print_string
    5.10 +                    (ML_Syntax.print_list ML_Syntax.print_string))
    5.11                    (ML_Syntax.print_list ML_Syntax.print_string)))
    5.12                ML_Syntax.print_position) ((name, kind), pos))
    5.13          | ((name, NONE), pos) =>
     6.1 --- a/src/Pure/PIDE/protocol.ML	Mon Aug 20 13:58:06 2012 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Aug 20 14:09:09 2012 +0200
     6.3 @@ -39,7 +39,8 @@
     6.4                      let
     6.5                        val (master, (name, (imports, (keywords, (uses, errors))))) =
     6.6                          pair string (pair string (pair (list string)
     6.7 -                          (pair (list (pair string (option (pair string (list string)))))
     6.8 +                          (pair (list (pair string
     6.9 +                            (option (pair (pair string (list string)) (list string)))))
    6.10                              (pair (list (pair string bool)) (list string))))) a;
    6.11                        val (uses', errors') =
    6.12                          (map (apfst Path.explode) uses, errors)
     7.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 20 13:58:06 2012 +0200
     7.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 20 14:09:09 2012 +0200
     7.3 @@ -222,7 +222,8 @@
     7.4                val uses = header.uses
     7.5                (Nil,
     7.6                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
     7.7 -                  pair(list(pair(Encode.string, option(pair(Encode.string, list(Encode.string))))),
     7.8 +                  pair(list(pair(Encode.string,
     7.9 +                    option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
    7.10                    pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
    7.11                  (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
    7.12            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
     8.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Mon Aug 20 13:58:06 2012 +0200
     8.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Mon Aug 20 14:09:09 2012 +0200
     8.3 @@ -61,6 +61,7 @@
     8.4    |> command Keyword.thy_heading2     thy_heading
     8.5    |> command Keyword.thy_heading3     thy_heading
     8.6    |> command Keyword.thy_heading4     thy_heading
     8.7 +  |> command Keyword.thy_load         thy_decl
     8.8    |> command Keyword.thy_decl         thy_decl
     8.9    |> command Keyword.thy_script       thy_decl
    8.10    |> command Keyword.thy_goal         goal
     9.1 --- a/src/Pure/System/build.scala	Mon Aug 20 13:58:06 2012 +0200
     9.2 +++ b/src/Pure/System/build.scala	Mon Aug 20 14:09:09 2012 +0200
     9.3 @@ -341,8 +341,8 @@
     9.4                    Outer_Syntax.init() +
     9.5                      // FIXME avoid hardwired stuff!?
     9.6                      ("theory", Keyword.THY_BEGIN) +
     9.7 -                    ("hence", Keyword.PRF_ASM_GOAL, "then have") +
     9.8 -                    ("thus", Keyword.PRF_ASM_GOAL, "then show")
     9.9 +                    ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
    9.10 +                    ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
    9.11                  (Set.empty[String], init_syntax, Nil)
    9.12              }
    9.13            val thy_info = new Thy_Info(new Thy_Load(preloaded))
    10.1 --- a/src/Pure/Thy/thy_header.ML	Mon Aug 20 13:58:06 2012 +0200
    10.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Aug 20 14:09:09 2012 +0200
    10.3 @@ -39,7 +39,7 @@
    10.4  fun define_keywords ({keywords, ...}: header) =
    10.5    List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
    10.6  
    10.7 -fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
    10.8 +fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
    10.9  
   10.10  structure Data = Theory_Data
   10.11  (
   10.12 @@ -75,7 +75,7 @@
   10.13  val header_lexicon =
   10.14    Scan.make_lexicon
   10.15      (map Symbol.explode
   10.16 -      ["%", "(", ")", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
   10.17 +      ["%", "(", ")", ",", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
   10.18  
   10.19  
   10.20  (* header args *)
   10.21 @@ -85,10 +85,15 @@
   10.22  val file_name = Parse.group (fn () => "file name") Parse.path;
   10.23  val theory_name = Parse.group (fn () => "theory name") Parse.name;
   10.24  
   10.25 -val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
   10.26 +val opt_files =
   10.27 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
   10.28 +val keyword_spec =
   10.29 +  Parse.group (fn () => "outer syntax keyword specification")
   10.30 +    (Parse.name -- opt_files -- Parse.tags);
   10.31 +
   10.32  val keyword_decl =
   10.33 -  Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
   10.34 -  (fn (names, kind) => map (rpair kind) names);
   10.35 +  Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) >>
   10.36 +  (fn (names, spec) => map (rpair spec) names);
   10.37  val keyword_decls = Parse.and_list1 keyword_decl >> flat;
   10.38  
   10.39  val file =
    11.1 --- a/src/Pure/Thy/thy_header.scala	Mon Aug 20 13:58:06 2012 +0200
    11.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Aug 20 14:09:09 2012 +0200
    11.3 @@ -26,7 +26,7 @@
    11.4    val BEGIN = "begin"
    11.5  
    11.6    private val lexicon =
    11.7 -    Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
    11.8 +    Scan.Lexicon("%", "(", ")", ",", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
    11.9  
   11.10  
   11.11    /* theory file name */
   11.12 @@ -47,10 +47,15 @@
   11.13    {
   11.14      val file_name = atom("file name", _.is_name)
   11.15  
   11.16 -    val keyword_kind =
   11.17 -      atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
   11.18 +    val opt_files =
   11.19 +      keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
   11.20 +      success(Nil)
   11.21 +    val keyword_spec =
   11.22 +      atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
   11.23 +      { case x ~ y ~ z => ((x, y), z) }
   11.24 +
   11.25      val keyword_decl =
   11.26 -      rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
   11.27 +      rep1(string) ~ opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
   11.28        { case xs ~ y => xs.map((_, y)) }
   11.29      val keyword_decls =
   11.30        keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   11.31 @@ -111,7 +116,7 @@
   11.32  
   11.33    /* keywords */
   11.34  
   11.35 -  type Keywords = List[(String, Option[(String, List[String])])]
   11.36 +  type Keywords = List[(String, Option[((String, List[String]), List[String])])]
   11.37  }
   11.38  
   11.39