src/Pure/Thy/thy_header.ML
author wenzelm
Sun Jul 10 11:18:35 2016 +0200 (2016-07-10)
changeset 63429 baedd4724f08
parent 63022 785a59235a15
child 63448 998acd66fbd7
permissions -rw-r--r--
tuned signature: more uniform Keyword.spec;
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@63429
     9
  type keywords = ((string * Position.T) * Keyword.spec) 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@59735
    15
  val theoryN: string
wenzelm@58928
    16
  val bootstrap_keywords: Keyword.keywords
wenzelm@58928
    17
  val add_keywords: keywords -> theory -> theory
wenzelm@58928
    18
  val get_keywords: theory -> Keyword.keywords
wenzelm@58928
    19
  val get_keywords': Proof.context -> Keyword.keywords
wenzelm@62895
    20
  val ml_bootstrapN: string
wenzelm@62932
    21
  val ml_roots: string list
wenzelm@63022
    22
  val bootstrap_thys: string list
wenzelm@46938
    23
  val args: header parser
wenzelm@46938
    24
  val read: Position.T -> string -> header
wenzelm@48927
    25
  val read_tokens: Token.T list -> header
wenzelm@22106
    26
end;
wenzelm@22106
    27
wenzelm@32466
    28
structure Thy_Header: THY_HEADER =
wenzelm@22106
    29
struct
wenzelm@22106
    30
wenzelm@58928
    31
(** keyword declarations **)
wenzelm@58928
    32
wenzelm@58928
    33
(* header *)
wenzelm@58928
    34
wenzelm@63429
    35
type keywords = ((string * Position.T) * Keyword.spec) list;
wenzelm@48874
    36
wenzelm@46938
    37
type header =
wenzelm@48927
    38
 {name: string * Position.T,
wenzelm@48927
    39
  imports: (string * Position.T) list,
wenzelm@51294
    40
  keywords: keywords};
wenzelm@46938
    41
wenzelm@51294
    42
fun make name imports keywords : header =
wenzelm@51294
    43
  {name = name, imports = imports, keywords = keywords};
wenzelm@46938
    44
wenzelm@46938
    45
wenzelm@58928
    46
(* bootstrap keywords *)
wenzelm@22106
    47
wenzelm@58868
    48
val chapterN = "chapter";
wenzelm@58868
    49
val sectionN = "section";
wenzelm@58868
    50
val subsectionN = "subsection";
wenzelm@58868
    51
val subsubsectionN = "subsubsection";
wenzelm@61463
    52
val paragraphN = "paragraph";
wenzelm@61463
    53
val subparagraphN = "subparagraph";
wenzelm@58999
    54
val textN = "text";
wenzelm@58999
    55
val txtN = "txt";
wenzelm@58999
    56
val text_rawN = "text_raw";
wenzelm@58868
    57
wenzelm@22106
    58
val theoryN = "theory";
wenzelm@22106
    59
val importsN = "imports";
wenzelm@46938
    60
val keywordsN = "keywords";
wenzelm@22106
    61
val beginN = "begin";
wenzelm@22106
    62
wenzelm@58928
    63
val bootstrap_keywords =
wenzelm@58903
    64
  Keyword.empty_keywords
wenzelm@58928
    65
  |> Keyword.add_keywords
wenzelm@63429
    66
    [(("%", @{here}), Keyword.no_spec),
wenzelm@63429
    67
     (("(", @{here}), Keyword.no_spec),
wenzelm@63429
    68
     ((")", @{here}), Keyword.no_spec),
wenzelm@63429
    69
     ((",", @{here}), Keyword.no_spec),
wenzelm@63429
    70
     (("::", @{here}), Keyword.no_spec),
wenzelm@63429
    71
     (("==", @{here}), Keyword.no_spec),
wenzelm@63429
    72
     (("and", @{here}), Keyword.no_spec),
wenzelm@63429
    73
     ((beginN, @{here}), Keyword.no_spec),
wenzelm@63429
    74
     ((importsN, @{here}), Keyword.no_spec),
wenzelm@63429
    75
     ((keywordsN, @{here}), Keyword.no_spec),
wenzelm@63429
    76
     ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
wenzelm@63429
    77
     ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
wenzelm@63429
    78
     ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
wenzelm@63429
    79
     ((subsubsectionN, @{here}), ((Keyword.document_heading, []), [])),
wenzelm@63429
    80
     ((paragraphN, @{here}), ((Keyword.document_heading, []), [])),
wenzelm@63429
    81
     ((subparagraphN, @{here}), ((Keyword.document_heading, []), [])),
wenzelm@63429
    82
     ((textN, @{here}), ((Keyword.document_body, []), [])),
wenzelm@63429
    83
     ((txtN, @{here}), ((Keyword.document_body, []), [])),
wenzelm@63429
    84
     ((text_rawN, @{here}), ((Keyword.document_raw, []), [])),
wenzelm@63429
    85
     ((theoryN, @{here}), ((Keyword.thy_begin, []), ["theory"])),
wenzelm@63429
    86
     (("ML", @{here}), ((Keyword.thy_decl, []), ["ML"]))];
wenzelm@58928
    87
wenzelm@58928
    88
wenzelm@58928
    89
(* theory data *)
wenzelm@22106
    90
wenzelm@58928
    91
structure Data = Theory_Data
wenzelm@58928
    92
(
wenzelm@58928
    93
  type T = Keyword.keywords;
wenzelm@58928
    94
  val empty = bootstrap_keywords;
wenzelm@58928
    95
  val extend = I;
wenzelm@58928
    96
  val merge = Keyword.merge_keywords;
wenzelm@58928
    97
);
wenzelm@58928
    98
wenzelm@58928
    99
val add_keywords = Data.map o Keyword.add_keywords;
wenzelm@58928
   100
wenzelm@58928
   101
val get_keywords = Data.get;
wenzelm@58928
   102
val get_keywords' = get_keywords o Proof_Context.theory_of;
wenzelm@58928
   103
wenzelm@58928
   104
wenzelm@58928
   105
wenzelm@58928
   106
(** concrete syntax **)
wenzelm@22106
   107
wenzelm@62895
   108
(* names *)
wenzelm@62895
   109
wenzelm@62895
   110
val ml_bootstrapN = "ML_Bootstrap";
wenzelm@62932
   111
val ml_roots = ["ML_Root0", "ML_Root"];
wenzelm@63022
   112
val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
wenzelm@62932
   113
wenzelm@62895
   114
wenzelm@62895
   115
wenzelm@22106
   116
(* header args *)
wenzelm@22106
   117
wenzelm@46938
   118
local
wenzelm@46938
   119
wenzelm@59694
   120
fun imports name =
wenzelm@59694
   121
  if name = Context.PureN then Scan.succeed []
wenzelm@62969
   122
  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
wenzelm@53962
   123
wenzelm@48864
   124
val opt_files =
wenzelm@48864
   125
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
wenzelm@50128
   126
wenzelm@48864
   127
val keyword_spec =
wenzelm@48864
   128
  Parse.group (fn () => "outer syntax keyword specification")
wenzelm@48864
   129
    (Parse.name -- opt_files -- Parse.tags);
wenzelm@48864
   130
wenzelm@50128
   131
val keyword_compl =
wenzelm@50128
   132
  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
wenzelm@50128
   133
wenzelm@46939
   134
val keyword_decl =
wenzelm@59934
   135
  Scan.repeat1 (Parse.position Parse.string) --
wenzelm@63429
   136
  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
wenzelm@50128
   137
  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
wenzelm@50128
   138
  >> (fn ((names, spec), _) => map (rpair spec) names);
wenzelm@50128
   139
wenzelm@46939
   140
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
wenzelm@46938
   141
wenzelm@46938
   142
in
wenzelm@22106
   143
wenzelm@22106
   144
val args =
wenzelm@59693
   145
  Parse.position Parse.theory_name :|-- (fn (name, pos) =>
wenzelm@59694
   146
    imports name --
wenzelm@53962
   147
    Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
wenzelm@53962
   148
    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
wenzelm@46938
   149
wenzelm@46938
   150
end;
wenzelm@22106
   151
wenzelm@22106
   152
wenzelm@22106
   153
(* read header *)
wenzelm@22106
   154
wenzelm@58868
   155
val heading =
wenzelm@62453
   156
  (Parse.command chapterN ||
wenzelm@58908
   157
    Parse.command sectionN ||
wenzelm@58908
   158
    Parse.command subsectionN ||
wenzelm@58999
   159
    Parse.command subsubsectionN ||
wenzelm@61463
   160
    Parse.command paragraphN ||
wenzelm@61463
   161
    Parse.command subparagraphN ||
wenzelm@58999
   162
    Parse.command textN ||
wenzelm@58999
   163
    Parse.command txtN ||
wenzelm@58999
   164
    Parse.command text_rawN) --
wenzelm@58868
   165
  Parse.tags -- Parse.!!! Parse.document_source;
wenzelm@58868
   166
wenzelm@22106
   167
val header =
wenzelm@58908
   168
  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
wenzelm@22106
   169
wenzelm@48927
   170
fun token_source pos str =
wenzelm@48927
   171
  str
wenzelm@48927
   172
  |> Source.of_string_limited 8000
wenzelm@48927
   173
  |> Symbol.source
wenzelm@58928
   174
  |> Token.source_strict bootstrap_keywords pos;
wenzelm@48927
   175
wenzelm@48927
   176
fun read_source pos source =
wenzelm@22106
   177
  let val res =
wenzelm@48927
   178
    source
wenzelm@36959
   179
    |> Token.source_proper
wenzelm@58864
   180
    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header)))
wenzelm@22106
   181
    |> Source.get_single;
wenzelm@22106
   182
  in
wenzelm@42003
   183
    (case res of
wenzelm@46938
   184
      SOME (h, _) => h
wenzelm@48992
   185
    | NONE => error ("Unexpected end of input" ^ Position.here pos))
wenzelm@22106
   186
  end;
wenzelm@22106
   187
wenzelm@48927
   188
fun read pos str = read_source pos (token_source pos str);
wenzelm@48927
   189
fun read_tokens toks = read_source Position.none (Source.of_list toks);
wenzelm@48927
   190
wenzelm@22106
   191
end;