src/Pure/Thy/thy_header.ML
author wenzelm
Sun Aug 21 20:42:26 2011 +0200 (2011-08-21)
changeset 44357 5f5649ac8235
parent 44160 8848867501fb
child 46737 09ab89658a5d
permissions -rw-r--r--
tuned Parse.group: delayed failure message;
wenzelm@22106
     1
(*  Title:      Pure/Thy/thy_header.ML
wenzelm@22106
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@22106
     3
wenzelm@22106
     4
Theory headers -- independent of outer syntax.
wenzelm@22106
     5
*)
wenzelm@22106
     6
wenzelm@22106
     7
signature THY_HEADER =
wenzelm@22106
     8
sig
wenzelm@36959
     9
  val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
wenzelm@42003
    10
  val read: Position.T -> string -> string * string list * (Path.T * bool) list
wenzelm@37950
    11
  val thy_path: string -> Path.T
wenzelm@37950
    12
  val consistent_name: string -> string -> unit
wenzelm@22106
    13
end;
wenzelm@22106
    14
wenzelm@32466
    15
structure Thy_Header: THY_HEADER =
wenzelm@22106
    16
struct
wenzelm@22106
    17
wenzelm@22106
    18
(* keywords *)
wenzelm@22106
    19
wenzelm@22106
    20
val headerN = "header";
wenzelm@22106
    21
val theoryN = "theory";
wenzelm@22106
    22
val importsN = "imports";
wenzelm@22106
    23
val usesN = "uses";
wenzelm@22106
    24
val beginN = "begin";
wenzelm@22106
    25
wenzelm@24577
    26
val header_lexicon = Scan.make_lexicon
wenzelm@24577
    27
  (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
wenzelm@22106
    28
wenzelm@22106
    29
wenzelm@22106
    30
(* header args *)
wenzelm@22106
    31
wenzelm@44357
    32
val file_name = Parse.group (fn () => "file name") Parse.name;
wenzelm@44357
    33
val theory_name = Parse.group (fn () => "theory name") Parse.name;
wenzelm@27890
    34
wenzelm@36950
    35
val file =
wenzelm@36950
    36
  Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
wenzelm@36950
    37
  file_name >> rpair true;
wenzelm@36950
    38
wenzelm@36950
    39
val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
wenzelm@22106
    40
wenzelm@22106
    41
val args =
wenzelm@36950
    42
  theory_name -- (Parse.$$$ importsN |--
wenzelm@36950
    43
    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
wenzelm@36950
    44
  >> Parse.triple2;
wenzelm@22106
    45
wenzelm@22106
    46
wenzelm@22106
    47
(* read header *)
wenzelm@22106
    48
wenzelm@22106
    49
val header =
wenzelm@36950
    50
  (Parse.$$$ headerN -- Parse.tags) |--
wenzelm@36950
    51
    (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
wenzelm@36950
    52
      (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
wenzelm@36950
    53
  (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
wenzelm@22106
    54
wenzelm@37978
    55
fun read pos str =
wenzelm@22106
    56
  let val res =
wenzelm@37978
    57
    str
wenzelm@37978
    58
    |> Source.of_string_limited 8000
wenzelm@40523
    59
    |> Symbol.source
wenzelm@36959
    60
    |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
wenzelm@36959
    61
    |> Token.source_proper
wenzelm@36959
    62
    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
wenzelm@22106
    63
    |> Source.get_single;
wenzelm@22106
    64
  in
wenzelm@42003
    65
    (case res of
wenzelm@42003
    66
      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
wenzelm@22106
    67
    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
wenzelm@22106
    68
  end;
wenzelm@22106
    69
wenzelm@37950
    70
wenzelm@38149
    71
(* file name *)
wenzelm@37950
    72
wenzelm@37950
    73
val thy_path = Path.ext "thy" o Path.basic;
wenzelm@37950
    74
wenzelm@37950
    75
fun consistent_name name name' =
wenzelm@37950
    76
  if name = name' then ()
wenzelm@41944
    77
  else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
wenzelm@37950
    78
wenzelm@22106
    79
end;