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