src/Pure/Thy/thy_header.ML
author wenzelm
Thu, 06 Nov 2014 11:44:41 +0100
changeset 58918 8d36bc5eaed3
parent 58908 58bedbc18915
child 58920 2f8168dc0eac
permissions -rw-r--r--
simplified keyword kinds; more explicit bootstrap syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_header.ML
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
     2
    Author:     Makarius
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     3
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
     4
Static theory header information.
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     5
*)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     6
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     7
signature THY_HEADER =
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     8
sig
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48864
diff changeset
     9
  type keywords = (string * Keyword.spec option) list
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    10
  type header =
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
    11
   {name: string * Position.T,
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
    12
    imports: (string * Position.T) list,
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    13
    keywords: keywords}
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    14
  val make: string * Position.T -> (string * Position.T) list -> keywords -> header
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58908
diff changeset
    15
  val define_keywords: keywords -> unit
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    16
  val declare_keyword: string * Keyword.spec option -> theory -> theory
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    17
  val the_keyword: theory -> string -> Keyword.spec option
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    18
  val args: header parser
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    19
  val read: Position.T -> string -> header
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
    20
  val read_tokens: Token.T list -> header
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    21
end;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    22
32466
a393b7e2a2f8 modernized Thy_Header;
wenzelm
parents: 29606
diff changeset
    23
structure Thy_Header: THY_HEADER =
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    24
struct
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    25
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48864
diff changeset
    26
type keywords = (string * Keyword.spec option) list;
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48864
diff changeset
    27
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    28
type header =
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
    29
 {name: string * Position.T,
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
    30
  imports: (string * Position.T) list,
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    31
  keywords: keywords};
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    32
51294
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    33
fun make name imports keywords : header =
0850d43cb355 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents: 51293
diff changeset
    34
  {name = name, imports = imports, keywords = keywords};
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    35
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    36
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    37
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    38
(** keyword declarations **)
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    39
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58908
diff changeset
    40
fun define_keywords (keywords: keywords) =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    41
  List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
46958
0ec8f04e753a define keywords early when processing the theory header, before running the body commands;
wenzelm
parents: 46950
diff changeset
    42
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
    43
fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    44
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    45
structure Data = Theory_Data
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    46
(
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    47
  type T = Keyword.spec option Symtab.table;
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    48
  val empty = Symtab.empty;
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    49
  val extend = I;
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    50
  fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    51
);
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    52
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    53
fun declare_keyword (name, spec) =
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    54
  Data.map (fn data =>
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    55
    (Option.map Keyword.spec spec;
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    56
      Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    57
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    58
fun the_keyword thy name =
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    59
  (case Symtab.lookup (Data.get thy) name of
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    60
    SOME spec => spec
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    61
  | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    62
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    63
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    64
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    65
(** concrete syntax **)
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    66
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    67
(* header keywords *)
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    68
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    69
val headerN = "header";
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
    70
val chapterN = "chapter";
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
    71
val sectionN = "section";
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
    72
val subsectionN = "subsection";
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
    73
val subsubsectionN = "subsubsection";
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
    74
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    75
val theoryN = "theory";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    76
val importsN = "imports";
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    77
val keywordsN = "keywords";
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    78
val beginN = "begin";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    79
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58868
diff changeset
    80
val header_keywords =
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58868
diff changeset
    81
  Keyword.empty_keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58868
diff changeset
    82
  |> fold (Keyword.add o rpair NONE)
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58868
diff changeset
    83
    ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
58907
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    84
  |> fold Keyword.add
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    85
    [(headerN, SOME Keyword.heading),
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    86
     (chapterN, SOME Keyword.heading),
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    87
     (sectionN, SOME Keyword.heading),
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    88
     (subsectionN, SOME Keyword.heading),
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    89
     (subsubsectionN, SOME Keyword.heading),
0ee3563803c9 more uniform header_keywords in ML/Scala;
wenzelm
parents: 58904
diff changeset
    90
     (theoryN, SOME Keyword.thy_begin)];
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    91
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    92
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    93
(* header args *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    94
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    95
local
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
    96
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
    97
val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
56801
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 53962
diff changeset
    98
val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
27890
62ac62e30ab1 args: explicit groups for file_name, theory_name;
wenzelm
parents: 27872
diff changeset
    99
56801
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 53962
diff changeset
   100
val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
53962
65bca53daf70 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents: 51627
diff changeset
   101
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
   102
val opt_files =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
   103
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   104
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
   105
val keyword_spec =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
   106
  Parse.group (fn () => "outer syntax keyword specification")
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
   107
    (Parse.name -- opt_files -- Parse.tags);
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48707
diff changeset
   108
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   109
val keyword_compl =
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   110
  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   111
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
   112
val keyword_decl =
50128
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   113
  Scan.repeat1 Parse.string --
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   114
  Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   115
  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   116
  >> (fn ((names, spec), _) => map (rpair spec) names);
599c935aac82 alternative completion for outer syntax keywords;
wenzelm
parents: 48992
diff changeset
   117
46939
5b67ac48b384 allow multiple 'keywords' as in 'fixes';
wenzelm
parents: 46938
diff changeset
   118
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   119
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   120
in
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   121
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   122
val args =
53962
65bca53daf70 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents: 51627
diff changeset
   123
  theory_name :|-- (fn (name, pos) =>
65bca53daf70 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents: 51627
diff changeset
   124
    (if name = Context.PureN then Scan.succeed [] else imports) --
65bca53daf70 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents: 51627
diff changeset
   125
    Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
65bca53daf70 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents: 51627
diff changeset
   126
    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   127
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   128
end;
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   129
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   130
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   131
(* read header *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   132
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
   133
val heading =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   134
  (Parse.command headerN ||
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   135
    Parse.command chapterN ||
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   136
    Parse.command sectionN ||
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   137
    Parse.command subsectionN ||
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   138
    Parse.command subsubsectionN) --
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
   139
  Parse.tags -- Parse.!!! Parse.document_source;
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58864
diff changeset
   140
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   141
val header =
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58907
diff changeset
   142
  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   143
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   144
fun token_source pos str =
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   145
  str
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   146
  |> Source.of_string_limited 8000
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   147
  |> Symbol.source
58904
f49c4f883c58 eliminated pointless dynamic keywords (TTY legacy);
wenzelm
parents: 58903
diff changeset
   148
  |> Token.source_strict header_keywords pos;
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   149
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   150
fun read_source pos source =
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   151
  let val res =
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   152
    source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   153
    |> Token.source_proper
58864
505a8150368a recover via scanner;
wenzelm
parents: 58863
diff changeset
   154
    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header)))
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   155
    |> Source.get_single;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   156
  in
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
   157
    (case res of
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46737
diff changeset
   158
      SOME (h, _) => h
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48927
diff changeset
   159
    | NONE => error ("Unexpected end of input" ^ Position.here pos))
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   160
  end;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   161
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   162
fun read pos str = read_source pos (token_source pos str);
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   163
fun read_tokens toks = read_source Position.none (Source.of_list toks);
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48881
diff changeset
   164
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
   165
end;