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;
     1 (*  Title:      Pure/Thy/thy_header.ML
     2     Author:     Makarius
     3 
     4 Static theory header information.
     5 *)
     6 
     7 signature THY_HEADER =
     8 sig
     9   type keywords = (string * Keyword.spec option) list
    10   type header =
    11    {name: string * Position.T,
    12     imports: (string * Position.T) list,
    13     keywords: keywords}
    14   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
    15   val define_keywords: header -> unit
    16   val declare_keyword: string * Keyword.spec option -> theory -> theory
    17   val the_keyword: theory -> string -> Keyword.spec option
    18   val args: header parser
    19   val read: Position.T -> string -> header
    20   val read_tokens: Token.T list -> header
    21 end;
    22 
    23 structure Thy_Header: THY_HEADER =
    24 struct
    25 
    26 type keywords = (string * Keyword.spec option) list;
    27 
    28 type header =
    29  {name: string * Position.T,
    30   imports: (string * Position.T) list,
    31   keywords: keywords};
    32 
    33 fun make name imports keywords : header =
    34   {name = name, imports = imports, keywords = keywords};
    35 
    36 
    37 
    38 (** keyword declarations **)
    39 
    40 fun define_keywords ({keywords, ...}: header) =
    41   List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
    42 
    43 fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
    44 
    45 structure Data = Theory_Data
    46 (
    47   type T = Keyword.spec option Symtab.table;
    48   val empty = Symtab.empty;
    49   val extend = I;
    50   fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
    51 );
    52 
    53 fun declare_keyword (name, spec) =
    54   Data.map (fn data =>
    55     (Option.map Keyword.spec spec;
    56       Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
    57 
    58 fun the_keyword thy name =
    59   (case Symtab.lookup (Data.get thy) name of
    60     SOME spec => spec
    61   | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
    62 
    63 
    64 
    65 (** concrete syntax **)
    66 
    67 (* header keywords *)
    68 
    69 val headerN = "header";
    70 val theoryN = "theory";
    71 val importsN = "imports";
    72 val keywordsN = "keywords";
    73 val beginN = "begin";
    74 
    75 val header_lexicons =
    76   pairself (Scan.make_lexicon o map Symbol.explode)
    77    (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN],
    78     [headerN, theoryN]);
    79 
    80 
    81 (* header args *)
    82 
    83 local
    84 
    85 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
    86 
    87 val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name);
    88 
    89 val opt_files =
    90   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
    91 
    92 val keyword_spec =
    93   Parse.group (fn () => "outer syntax keyword specification")
    94     (Parse.name -- opt_files -- Parse.tags);
    95 
    96 val keyword_compl =
    97   Parse.group (fn () => "outer syntax keyword completion") Parse.name;
    98 
    99 val keyword_decl =
   100   Scan.repeat1 Parse.string --
   101   Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
   102   Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
   103   >> (fn ((names, spec), _) => map (rpair spec) names);
   104 
   105 val keyword_decls = Parse.and_list1 keyword_decl >> flat;
   106 
   107 in
   108 
   109 val args =
   110   theory_name :|-- (fn (name, pos) =>
   111     (if name = Context.PureN then Scan.succeed [] else imports) --
   112     Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   113     Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
   114 
   115 end;
   116 
   117 
   118 (* read header *)
   119 
   120 val header =
   121   (Parse.command_name headerN -- Parse.tags) |--
   122     (Parse.!!! (Parse.document_source -- Scan.repeat Parse.semicolon --
   123       (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
   124   (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
   125 
   126 fun token_source pos str =
   127   str
   128   |> Source.of_string_limited 8000
   129   |> Symbol.source
   130   |> Token.source {do_recover = NONE} (K header_lexicons) pos;
   131 
   132 fun read_source pos source =
   133   let val res =
   134     source
   135     |> Token.source_proper
   136     |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
   137     |> Source.get_single;
   138   in
   139     (case res of
   140       SOME (h, _) => h
   141     | NONE => error ("Unexpected end of input" ^ Position.here pos))
   142   end;
   143 
   144 fun read pos str = read_source pos (token_source pos str);
   145 fun read_tokens toks = read_source Position.none (Source.of_list toks);
   146 
   147 end;