src/Pure/Thy/thy_header.ML
author wenzelm
Sun, 21 Aug 2011 20:42:26 +0200
changeset 44357 5f5649ac8235
parent 44160 8848867501fb
child 46737 09ab89658a5d
permissions -rw-r--r--
tuned Parse.group: delayed failure message;
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
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     3
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
     4
Theory headers -- independent of outer syntax.
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
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
     9
  val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    10
  val read: Position.T -> string -> string * string list * (Path.T * bool) list
37950
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    11
  val thy_path: string -> Path.T
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    12
  val consistent_name: string -> string -> unit
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    13
end;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    14
32466
a393b7e2a2f8 modernized Thy_Header;
wenzelm
parents: 29606
diff changeset
    15
structure Thy_Header: THY_HEADER =
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    16
struct
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    17
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    18
(* keywords *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    19
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    20
val headerN = "header";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    21
val theoryN = "theory";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    22
val importsN = "imports";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    23
val usesN = "uses";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    24
val beginN = "begin";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    25
24577
c6acb6d79757 removed redundant OuterLex.make_lexicon;
wenzelm
parents: 23863
diff changeset
    26
val header_lexicon = Scan.make_lexicon
c6acb6d79757 removed redundant OuterLex.make_lexicon;
wenzelm
parents: 23863
diff changeset
    27
  (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    28
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    29
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    30
(* header args *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    31
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 44160
diff changeset
    32
val file_name = Parse.group (fn () => "file name") Parse.name;
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 44160
diff changeset
    33
val theory_name = Parse.group (fn () => "theory name") Parse.name;
27890
62ac62e30ab1 args: explicit groups for file_name, theory_name;
wenzelm
parents: 27872
diff changeset
    34
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    35
val file =
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    36
  Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    37
  file_name >> rpair true;
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    38
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    39
val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    40
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    41
val args =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    42
  theory_name -- (Parse.$$$ importsN |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    43
    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    44
  >> Parse.triple2;
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    45
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    46
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    47
(* read header *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    48
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    49
val header =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    50
  (Parse.$$$ headerN -- Parse.tags) |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    51
    (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    52
      (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    53
  (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    54
37978
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    55
fun read pos str =
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    56
  let val res =
37978
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    57
    str
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    58
    |> Source.of_string_limited 8000
40523
1050315f6ee2 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents: 38149
diff changeset
    59
    |> Symbol.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
    60
    |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    61
    |> Token.source_proper
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
    62
    |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    63
    |> Source.get_single;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    64
  in
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    65
    (case res of
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    66
      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    67
    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    68
  end;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    69
37950
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    70
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 37978
diff changeset
    71
(* file name *)
37950
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    72
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    73
val thy_path = Path.ext "thy" o Path.basic;
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    74
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    75
fun consistent_name name name' =
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    76
  if name = name' then ()
41944
b97091ae583a Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents: 40530
diff changeset
    77
  else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
37950
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    78
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    79
end;