src/Pure/Thy/thy_header.ML
author wenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431 e0f20a44ff9d
parent 53962 65bca53daf70
child 56801 8dd9df88f647
permissions -rw-r--r--
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
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@46958
    15
  val define_keywords: header -> unit
wenzelm@46961
    16
  val declare_keyword: string * Keyword.spec option -> theory -> theory
wenzelm@46961
    17
  val the_keyword: theory -> string -> Keyword.spec option
wenzelm@46938
    18
  val args: header parser
wenzelm@46938
    19
  val read: Position.T -> string -> header
wenzelm@48927
    20
  val read_tokens: Token.T list -> header
wenzelm@22106
    21
end;
wenzelm@22106
    22
wenzelm@32466
    23
structure Thy_Header: THY_HEADER =
wenzelm@22106
    24
struct
wenzelm@22106
    25
wenzelm@48874
    26
type keywords = (string * Keyword.spec option) list;
wenzelm@48874
    27
wenzelm@46938
    28
type header =
wenzelm@48927
    29
 {name: string * Position.T,
wenzelm@48927
    30
  imports: (string * Position.T) list,
wenzelm@51294
    31
  keywords: keywords};
wenzelm@46938
    32
wenzelm@51294
    33
fun make name imports keywords : header =
wenzelm@51294
    34
  {name = name, imports = imports, keywords = keywords};
wenzelm@46938
    35
wenzelm@46938
    36
wenzelm@46938
    37
wenzelm@46938
    38
(** keyword declarations **)
wenzelm@46938
    39
wenzelm@46958
    40
fun define_keywords ({keywords, ...}: header) =
wenzelm@46961
    41
  List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
wenzelm@46958
    42
wenzelm@48864
    43
fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
wenzelm@46938
    44
wenzelm@46938
    45
structure Data = Theory_Data
wenzelm@46938
    46
(
wenzelm@46961
    47
  type T = Keyword.spec option Symtab.table;
wenzelm@46938
    48
  val empty = Symtab.empty;
wenzelm@46938
    49
  val extend = I;
wenzelm@46938
    50
  fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
wenzelm@46938
    51
);
wenzelm@46938
    52
wenzelm@46961
    53
fun declare_keyword (name, spec) =
wenzelm@46961
    54
  Data.map (fn data =>
wenzelm@46961
    55
    (Option.map Keyword.spec spec;
wenzelm@46961
    56
      Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
wenzelm@46938
    57
wenzelm@46938
    58
fun the_keyword thy name =
wenzelm@46938
    59
  (case Symtab.lookup (Data.get thy) name of
wenzelm@46961
    60
    SOME spec => spec
wenzelm@46961
    61
  | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
wenzelm@46938
    62
wenzelm@46938
    63
wenzelm@46938
    64
wenzelm@46938
    65
(** concrete syntax **)
wenzelm@46938
    66
wenzelm@46938
    67
(* header keywords *)
wenzelm@22106
    68
wenzelm@22106
    69
val headerN = "header";
wenzelm@22106
    70
val theoryN = "theory";
wenzelm@22106
    71
val importsN = "imports";
wenzelm@46938
    72
val keywordsN = "keywords";
wenzelm@22106
    73
val beginN = "begin";
wenzelm@22106
    74
wenzelm@48927
    75
val header_lexicons =
wenzelm@48927
    76
  pairself (Scan.make_lexicon o map Symbol.explode)
wenzelm@51293
    77
   (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN],
wenzelm@48927
    78
    [headerN, theoryN]);
wenzelm@22106
    79
wenzelm@22106
    80
wenzelm@22106
    81
(* header args *)
wenzelm@22106
    82
wenzelm@46938
    83
local
wenzelm@46938
    84
wenzelm@48927
    85
val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
wenzelm@27890
    86
wenzelm@53962
    87
val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name);
wenzelm@53962
    88
wenzelm@48864
    89
val opt_files =
wenzelm@48864
    90
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
wenzelm@50128
    91
wenzelm@48864
    92
val keyword_spec =
wenzelm@48864
    93
  Parse.group (fn () => "outer syntax keyword specification")
wenzelm@48864
    94
    (Parse.name -- opt_files -- Parse.tags);
wenzelm@48864
    95
wenzelm@50128
    96
val keyword_compl =
wenzelm@50128
    97
  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
wenzelm@50128
    98
wenzelm@46939
    99
val keyword_decl =
wenzelm@50128
   100
  Scan.repeat1 Parse.string --
wenzelm@50128
   101
  Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
wenzelm@50128
   102
  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
wenzelm@50128
   103
  >> (fn ((names, spec), _) => map (rpair spec) names);
wenzelm@50128
   104
wenzelm@46939
   105
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
wenzelm@46938
   106
wenzelm@46938
   107
in
wenzelm@22106
   108
wenzelm@22106
   109
val args =
wenzelm@53962
   110
  theory_name :|-- (fn (name, pos) =>
wenzelm@53962
   111
    (if name = Context.PureN then Scan.succeed [] else imports) --
wenzelm@53962
   112
    Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
wenzelm@53962
   113
    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
wenzelm@46938
   114
wenzelm@46938
   115
end;
wenzelm@22106
   116
wenzelm@22106
   117
wenzelm@22106
   118
(* read header *)
wenzelm@22106
   119
wenzelm@22106
   120
val header =
wenzelm@48927
   121
  (Parse.command_name headerN -- Parse.tags) |--
wenzelm@51627
   122
    (Parse.!!! (Parse.document_source -- Scan.repeat Parse.semicolon --
wenzelm@48927
   123
      (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
wenzelm@48927
   124
  (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
wenzelm@22106
   125
wenzelm@48927
   126
fun token_source pos str =
wenzelm@48927
   127
  str
wenzelm@48927
   128
  |> Source.of_string_limited 8000
wenzelm@48927
   129
  |> Symbol.source
wenzelm@48927
   130
  |> Token.source {do_recover = NONE} (K header_lexicons) pos;
wenzelm@48927
   131
wenzelm@48927
   132
fun read_source pos source =
wenzelm@22106
   133
  let val res =
wenzelm@48927
   134
    source
wenzelm@36959
   135
    |> Token.source_proper
wenzelm@36959
   136
    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
wenzelm@22106
   137
    |> Source.get_single;
wenzelm@22106
   138
  in
wenzelm@42003
   139
    (case res of
wenzelm@46938
   140
      SOME (h, _) => h
wenzelm@48992
   141
    | NONE => error ("Unexpected end of input" ^ Position.here pos))
wenzelm@22106
   142
  end;
wenzelm@22106
   143
wenzelm@48927
   144
fun read pos str = read_source pos (token_source pos str);
wenzelm@48927
   145
fun read_tokens toks = read_source Position.none (Source.of_list toks);
wenzelm@48927
   146
wenzelm@22106
   147
end;