1.1 --- a/src/Pure/Isar/thy_header.ML	Fri Jan 19 22:08:13 2007 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,65 +0,0 @@
     1.4 -(*  Title:      Pure/Isar/thy_header.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Markus Wenzel, TU Muenchen
     1.7 -
     1.8 -Theory headers -- processed separately with minimal outer syntax.
     1.9 -*)
    1.10 -
    1.11 -signature THY_HEADER =
    1.12 -sig
    1.13 -  val args: OuterLex.token list ->
    1.14 -    (string * string list * (string * bool) list) * OuterLex.token list
    1.15 -  val read: (string, 'a) Source.source * Position.T ->
    1.16 -    string * string list * (string * bool) list
    1.17 -end;
    1.18 -
    1.19 -structure ThyHeader: THY_HEADER =
    1.20 -struct
    1.21 -
    1.22 -structure T = OuterLex;
    1.23 -structure P = OuterParse;
    1.24 -
    1.25 -
    1.26 -(* keywords *)
    1.27 -
    1.28 -val headerN = "header";
    1.29 -val theoryN = "theory";
    1.30 -val importsN = "imports";
    1.31 -val usesN = "uses";
    1.32 -val beginN = "begin";
    1.33 -
    1.34 -val header_lexicon = T.make_lexicon
    1.35 -  ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
    1.36 -
    1.37 -
    1.38 -(* header args *)
    1.39 -
    1.40 -val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
    1.41 -val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
    1.42 -
    1.43 -val args =
    1.44 -  P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
    1.45 -  >> P.triple2;
    1.46 -
    1.47 -
    1.48 -(* read header *)
    1.49 -
    1.50 -val header =
    1.51 -  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
    1.52 -    (P.$$$ theoryN -- P.tags) |-- args)) ||
    1.53 -  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
    1.54 -
    1.55 -fun read (src, pos) =
    1.56 -  let val res =
    1.57 -    src
    1.58 -    |> Symbol.source false
    1.59 -    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
    1.60 -    |> T.source_proper
    1.61 -    |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
    1.62 -    |> Source.get_single;
    1.63 -  in
    1.64 -    (case res of SOME (x, _) => x
    1.65 -    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
    1.66 -  end;
    1.67 -
    1.68 -end;

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Jan 19 22:08:14 2007 +0100
     2.3 @@ -0,0 +1,65 @@
     2.4 +(*  Title:      Pure/Thy/thy_header.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Markus Wenzel, TU Muenchen
     2.7 +
     2.8 +Theory headers -- independent of outer syntax.
     2.9 +*)
    2.10 +
    2.11 +signature THY_HEADER =
    2.12 +sig
    2.13 +  val args: OuterLex.token list ->
    2.14 +    (string * string list * (string * bool) list) * OuterLex.token list
    2.15 +  val read: (string, 'a) Source.source * Position.T ->
    2.16 +    string * string list * (string * bool) list
    2.17 +end;
    2.18 +
    2.19 +structure ThyHeader: THY_HEADER =
    2.20 +struct
    2.21 +
    2.22 +structure T = OuterLex;
    2.23 +structure P = OuterParse;
    2.24 +
    2.25 +
    2.26 +(* keywords *)
    2.27 +
    2.28 +val headerN = "header";
    2.29 +val theoryN = "theory";
    2.30 +val importsN = "imports";
    2.31 +val usesN = "uses";
    2.32 +val beginN = "begin";
    2.33 +
    2.34 +val header_lexicon = T.make_lexicon
    2.35 +  ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
    2.36 +
    2.37 +
    2.38 +(* header args *)
    2.39 +
    2.40 +val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
    2.41 +val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
    2.42 +
    2.43 +val args =
    2.44 +  P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
    2.45 +  >> P.triple2;
    2.46 +
    2.47 +
    2.48 +(* read header *)
    2.49 +
    2.50 +val header =
    2.51 +  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
    2.52 +    (P.$$$ theoryN -- P.tags) |-- args)) ||
    2.53 +  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
    2.54 +
    2.55 +fun read (src, pos) =
    2.56 +  let val res =
    2.57 +    src
    2.58 +    |> Symbol.source false
    2.59 +    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
    2.60 +    |> T.source_proper
    2.61 +    |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
    2.62 +    |> Source.get_single;
    2.63 +  in
    2.64 +    (case res of SOME (x, _) => x
    2.65 +    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
    2.66 +  end;
    2.67 +
    2.68 +end;