src/Pure/Isar/args.ML
changeset 5822 3f824514ad88
child 5878 769abc29bb8e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Nov 09 15:32:02 1998 +0100
     1.3 @@ -0,0 +1,100 @@
     1.4 +(*  Title:      Pure/Isar/args.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Concrete argument syntax (for attributes, methods etc.).
     1.9 +
    1.10 +TODO:
    1.11 +  - sectioned: generalize sname to attributed thms;
    1.12 +*)
    1.13 +
    1.14 +signature ARGS =
    1.15 +sig
    1.16 +  type T
    1.17 +  val val_of: T -> string
    1.18 +  val ident: string -> T
    1.19 +  val string: string -> T
    1.20 +  val keyword: string -> T
    1.21 +  val stopper: T * (T -> bool)
    1.22 +  val not_eof: T -> bool
    1.23 +  val $$$ : string -> T list -> string * T list
    1.24 +  val name: T list -> string * T list
    1.25 +  val sectioned: string list -> T list -> (string list * (string * string list) list) * T list
    1.26 +  type src
    1.27 +  val syntax: string -> (T list -> 'a * T list) -> ('a -> 'b) -> src -> 'b
    1.28 +end;
    1.29 +
    1.30 +structure Args: ARGS =
    1.31 +struct
    1.32 +
    1.33 +
    1.34 +(** datatype T **)
    1.35 +
    1.36 +datatype kind = Ident | String | Keyword | EOF;
    1.37 +datatype T = Arg of kind * string;
    1.38 +
    1.39 +fun val_of (Arg (_, x)) = x;
    1.40 +
    1.41 +fun str_of (Arg (Ident, x)) = enclose "'" "'" x
    1.42 +  | str_of (Arg (String, x)) = quote x
    1.43 +  | str_of (Arg (Keyword, x)) = x;
    1.44 +
    1.45 +fun arg kind x = Arg (kind, x);
    1.46 +val ident = arg Ident;
    1.47 +val string = arg String;
    1.48 +val keyword = arg Keyword;
    1.49 +
    1.50 +
    1.51 +(* eof *)
    1.52 +
    1.53 +val eof = arg EOF "";
    1.54 +
    1.55 +fun is_eof (Arg (EOF, _)) = true
    1.56 +  | is_eof _ = false;
    1.57 +
    1.58 +val stopper = (eof, is_eof);
    1.59 +val not_eof = not o is_eof;
    1.60 +
    1.61 +
    1.62 +
    1.63 +(** scanners **)
    1.64 +
    1.65 +(* basic *)
    1.66 +
    1.67 +fun $$$ x = Scan.one (fn Arg (k, y) => (k = Ident orelse k = Keyword) andalso x = y) >> val_of;
    1.68 +val name = Scan.one (fn (Arg (k, x)) => k = Ident orelse k = String) >> val_of;
    1.69 +
    1.70 +
    1.71 +(* sections *)
    1.72 +
    1.73 +val no_colon = Scan.one (fn Arg (k, x) => k = String orelse x <> ":");
    1.74 +val sname = name --| Scan.ahead no_colon;
    1.75 +
    1.76 +fun sect s = ($$$ s --| $$$ ":") -- Scan.repeat sname;
    1.77 +
    1.78 +fun any_sect [] = Scan.fail
    1.79 +  | any_sect (s :: ss) = sect s || any_sect ss;
    1.80 +
    1.81 +fun sectioned ss =
    1.82 +  Scan.repeat sname -- Scan.repeat (any_sect ss);
    1.83 +
    1.84 +
    1.85 +
    1.86 +(** type src **)
    1.87 +
    1.88 +type src = (string * T list) * Position.T;
    1.89 +
    1.90 +fun err_in_src kind msg ((s, args), pos) =
    1.91 +  error (space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos ^ ": " ^ msg);
    1.92 +
    1.93 +
    1.94 +(* argument syntax *)
    1.95 +
    1.96 +fun syntax kind scan f (src as ((s, args), pos)) =
    1.97 +  (case handle_error (Scan.error (Scan.finite stopper scan)) args of
    1.98 +    OK (x, []) => f x
    1.99 +  | OK (_, args') => err_in_src kind "bad arguments" ((s, args'), pos)
   1.100 +  | Error msg => err_in_src kind ("\n" ^ msg) src);
   1.101 +
   1.102 +
   1.103 +end;