src/Pure/Thy/thy_header.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58999 ed09ae4ea2d8
child 59693 d96cb03caf9e
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@22106
     1
(*  Title:      Pure/Thy/thy_header.ML
wenzelm@46939
     2
    Author:     Makarius
wenzelm@22106
     3
wenzelm@46939
     4
Static theory header information.
wenzelm@22106
     5
*)
wenzelm@22106
     6
wenzelm@22106
     7
signature THY_HEADER =
wenzelm@22106
     8
sig
wenzelm@48874
     9
  type keywords = (string * Keyword.spec option) list
wenzelm@46938
    10
  type header =
wenzelm@48927
    11
   {name: string * Position.T,
wenzelm@48927
    12
    imports: (string * Position.T) list,
wenzelm@51294
    13
    keywords: keywords}
wenzelm@51294
    14
  val make: string * Position.T -> (string * Position.T) list -> keywords -> header
wenzelm@58928
    15
  val bootstrap_keywords: Keyword.keywords
wenzelm@58928
    16
  val add_keywords: keywords -> theory -> theory
wenzelm@58928
    17
  val get_keywords: theory -> Keyword.keywords
wenzelm@58928
    18
  val get_keywords': Proof.context -> Keyword.keywords
wenzelm@46938
    19
  val args: header parser
wenzelm@46938
    20
  val read: Position.T -> string -> header
wenzelm@48927
    21
  val read_tokens: Token.T list -> header
wenzelm@22106
    22
end;
wenzelm@22106
    23
wenzelm@32466
    24
structure Thy_Header: THY_HEADER =
wenzelm@22106
    25
struct
wenzelm@22106
    26
wenzelm@58928
    27
(** keyword declarations **)
wenzelm@58928
    28
wenzelm@58928
    29
(* header *)
wenzelm@58928
    30
wenzelm@48874
    31
type keywords = (string * Keyword.spec option) list;
wenzelm@48874
    32
wenzelm@46938
    33
type header =
wenzelm@48927
    34
 {name: string * Position.T,
wenzelm@48927
    35
  imports: (string * Position.T) list,
wenzelm@51294
    36
  keywords: keywords};
wenzelm@46938
    37
wenzelm@51294
    38
fun make name imports keywords : header =
wenzelm@51294
    39
  {name = name, imports = imports, keywords = keywords};
wenzelm@46938
    40
wenzelm@46938
    41
wenzelm@58928
    42
(* bootstrap keywords *)
wenzelm@22106
    43
wenzelm@22106
    44
val headerN = "header";
wenzelm@58868
    45
val chapterN = "chapter";
wenzelm@58868
    46
val sectionN = "section";
wenzelm@58868
    47
val subsectionN = "subsection";
wenzelm@58868
    48
val subsubsectionN = "subsubsection";
wenzelm@58999
    49
val textN = "text";
wenzelm@58999
    50
val txtN = "txt";
wenzelm@58999
    51
val text_rawN = "text_raw";
wenzelm@58868
    52
wenzelm@22106
    53
val theoryN = "theory";
wenzelm@22106
    54
val importsN = "imports";
wenzelm@46938
    55
val keywordsN = "keywords";
wenzelm@22106
    56
val beginN = "begin";
wenzelm@22106
    57
wenzelm@58928
    58
val bootstrap_keywords =
wenzelm@58903
    59
  Keyword.empty_keywords
wenzelm@58928
    60
  |> Keyword.add_keywords
wenzelm@58928
    61
    [("%", NONE),
wenzelm@58928
    62
     ("(", NONE),
wenzelm@58928
    63
     (")", NONE),
wenzelm@58928
    64
     (",", NONE),
wenzelm@58928
    65
     ("::", NONE),
wenzelm@58928
    66
     ("==", NONE),
wenzelm@58928
    67
     ("and", NONE),
wenzelm@58928
    68
     (beginN, NONE),
wenzelm@58928
    69
     (importsN, NONE),
wenzelm@58928
    70
     (keywordsN, NONE),
wenzelm@58999
    71
     (headerN, SOME ((Keyword.document_heading, []), [])),
wenzelm@58999
    72
     (chapterN, SOME ((Keyword.document_heading, []), [])),
wenzelm@58999
    73
     (sectionN, SOME ((Keyword.document_heading, []), [])),
wenzelm@58999
    74
     (subsectionN, SOME ((Keyword.document_heading, []), [])),
wenzelm@58999
    75
     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
wenzelm@58999
    76
     (textN, SOME ((Keyword.document_body, []), [])),
wenzelm@58999
    77
     (txtN, SOME ((Keyword.document_body, []), [])),
wenzelm@58999
    78
     (text_rawN, SOME ((Keyword.document_raw, []), [])),
wenzelm@58928
    79
     (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
wenzelm@58928
    80
     ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
wenzelm@58928
    81
wenzelm@58928
    82
wenzelm@58928
    83
(* theory data *)
wenzelm@22106
    84
wenzelm@58928
    85
structure Data = Theory_Data
wenzelm@58928
    86
(
wenzelm@58928
    87
  type T = Keyword.keywords;
wenzelm@58928
    88
  val empty = bootstrap_keywords;
wenzelm@58928
    89
  val extend = I;
wenzelm@58928
    90
  val merge = Keyword.merge_keywords;
wenzelm@58928
    91
);
wenzelm@58928
    92
wenzelm@58928
    93
val add_keywords = Data.map o Keyword.add_keywords;
wenzelm@58928
    94
wenzelm@58928
    95
val get_keywords = Data.get;
wenzelm@58928
    96
val get_keywords' = get_keywords o Proof_Context.theory_of;
wenzelm@58928
    97
wenzelm@58928
    98
wenzelm@58928
    99
wenzelm@58928
   100
(** concrete syntax **)
wenzelm@22106
   101
wenzelm@22106
   102
(* header args *)
wenzelm@22106
   103
wenzelm@46938
   104
local
wenzelm@46938
   105
wenzelm@48927
   106
val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
wenzelm@56801
   107
val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
wenzelm@27890
   108
wenzelm@56801
   109
val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
wenzelm@53962
   110
wenzelm@48864
   111
val opt_files =
wenzelm@48864
   112
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
wenzelm@50128
   113
wenzelm@48864
   114
val keyword_spec =
wenzelm@48864
   115
  Parse.group (fn () => "outer syntax keyword specification")
wenzelm@48864
   116
    (Parse.name -- opt_files -- Parse.tags);
wenzelm@48864
   117
wenzelm@50128
   118
val keyword_compl =
wenzelm@50128
   119
  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
wenzelm@50128
   120
wenzelm@46939
   121
val keyword_decl =
wenzelm@50128
   122
  Scan.repeat1 Parse.string --
wenzelm@50128
   123
  Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
wenzelm@50128
   124
  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
wenzelm@50128
   125
  >> (fn ((names, spec), _) => map (rpair spec) names);
wenzelm@50128
   126
wenzelm@46939
   127
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
wenzelm@46938
   128
wenzelm@46938
   129
in
wenzelm@22106
   130
wenzelm@22106
   131
val args =
wenzelm@53962
   132
  theory_name :|-- (fn (name, pos) =>
wenzelm@53962
   133
    (if name = Context.PureN then Scan.succeed [] else imports) --
wenzelm@53962
   134
    Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
wenzelm@53962
   135
    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
wenzelm@46938
   136
wenzelm@46938
   137
end;
wenzelm@22106
   138
wenzelm@22106
   139
wenzelm@22106
   140
(* read header *)
wenzelm@22106
   141
wenzelm@58868
   142
val heading =
wenzelm@58908
   143
  (Parse.command headerN ||
wenzelm@58908
   144
    Parse.command chapterN ||
wenzelm@58908
   145
    Parse.command sectionN ||
wenzelm@58908
   146
    Parse.command subsectionN ||
wenzelm@58999
   147
    Parse.command subsubsectionN ||
wenzelm@58999
   148
    Parse.command textN ||
wenzelm@58999
   149
    Parse.command txtN ||
wenzelm@58999
   150
    Parse.command text_rawN) --
wenzelm@58868
   151
  Parse.tags -- Parse.!!! Parse.document_source;
wenzelm@58868
   152
wenzelm@22106
   153
val header =
wenzelm@58908
   154
  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
wenzelm@22106
   155
wenzelm@48927
   156
fun token_source pos str =
wenzelm@48927
   157
  str
wenzelm@48927
   158
  |> Source.of_string_limited 8000
wenzelm@48927
   159
  |> Symbol.source
wenzelm@58928
   160
  |> Token.source_strict bootstrap_keywords pos;
wenzelm@48927
   161
wenzelm@48927
   162
fun read_source pos source =
wenzelm@22106
   163
  let val res =
wenzelm@48927
   164
    source
wenzelm@36959
   165
    |> Token.source_proper
wenzelm@58864
   166
    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header)))
wenzelm@22106
   167
    |> Source.get_single;
wenzelm@22106
   168
  in
wenzelm@42003
   169
    (case res of
wenzelm@46938
   170
      SOME (h, _) => h
wenzelm@48992
   171
    | NONE => error ("Unexpected end of input" ^ Position.here pos))
wenzelm@22106
   172
  end;
wenzelm@22106
   173
wenzelm@48927
   174
fun read pos str = read_source pos (token_source pos str);
wenzelm@48927
   175
fun read_tokens toks = read_source Position.none (Source.of_list toks);
wenzelm@48927
   176
wenzelm@22106
   177
end;