src/Pure/Thy/thy_header.ML
author wenzelm
Sat, 13 Nov 2010 19:21:53 +0100
changeset 40523 1050315f6ee2
parent 38149 3c380380beac
child 40530 f814863f3918
permissions -rw-r--r--
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);
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
37978
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    10
  val read: Position.T -> string -> string * string list * (string * 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 split_thy_path: Path.T -> Path.T * string
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    13
  val consistent_name: string -> string -> unit
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    14
end;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    15
32466
a393b7e2a2f8 modernized Thy_Header;
wenzelm
parents: 29606
diff changeset
    16
structure Thy_Header: THY_HEADER =
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    17
struct
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    18
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    19
(* keywords *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    20
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    21
val headerN = "header";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    22
val theoryN = "theory";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    23
val importsN = "imports";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    24
val usesN = "uses";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    25
val beginN = "begin";
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    26
24577
c6acb6d79757 removed redundant OuterLex.make_lexicon;
wenzelm
parents: 23863
diff changeset
    27
val header_lexicon = Scan.make_lexicon
c6acb6d79757 removed redundant OuterLex.make_lexicon;
wenzelm
parents: 23863
diff changeset
    28
  (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
22106
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
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    31
(* header args *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    32
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    33
val file_name = Parse.group "file name" Parse.name;
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    34
val theory_name = Parse.group "theory name" Parse.name;
27890
62ac62e30ab1 args: explicit groups for file_name, theory_name;
wenzelm
parents: 27872
diff changeset
    35
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    36
val file =
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    37
  Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    38
  file_name >> rpair true;
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    39
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    40
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
    41
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    42
val args =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    43
  theory_name -- (Parse.$$$ importsN |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    44
    Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    45
  >> Parse.triple2;
22106
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
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    48
(* read header *)
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    49
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    50
val header =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    51
  (Parse.$$$ headerN -- Parse.tags) |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    52
    (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    53
      (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 34167
diff changeset
    54
  (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    55
37978
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    56
fun read pos str =
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    57
  let val res =
37978
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    58
    str
548f3f165d05 simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents: 37950
diff changeset
    59
    |> 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
    60
    |> 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
    61
    |> 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
    62
    |> 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
    63
    |> 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
    64
    |> Source.get_single;
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    65
  in
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    66
    (case res of SOME (x, _) => x
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 split_thy_path path =
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    76
  (case Path.split_ext path of
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    77
    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
38149
3c380380beac somewhat uniform Thy_Header.split_thy_path in ML and Scala;
wenzelm
parents: 37978
diff changeset
    78
  | _ => error ("Bad theory file specification: " ^ Path.implode path));
37950
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    79
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    80
fun consistent_name name name' =
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    81
  if name = name' then ()
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    82
  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    83
    " does not agree with theory name " ^ quote name');
bc285d91041e moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents: 36959
diff changeset
    84
22106
0886ec05f951 renamed Isar/thy_header.ML to Thy/thy_header.ML;
wenzelm
parents:
diff changeset
    85
end;