src/Pure/Isar/args.ML
author wenzelm
Mon Nov 09 15:32:02 1998 +0100 (1998-11-09)
changeset 5822 3f824514ad88
child 5878 769abc29bb8e
permissions -rw-r--r--
Concrete argument syntax (for attributes, methods etc.).
     1 (*  Title:      Pure/Isar/args.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Concrete argument syntax (for attributes, methods etc.).
     6 
     7 TODO:
     8   - sectioned: generalize sname to attributed thms;
     9 *)
    10 
    11 signature ARGS =
    12 sig
    13   type T
    14   val val_of: T -> string
    15   val ident: string -> T
    16   val string: string -> T
    17   val keyword: string -> T
    18   val stopper: T * (T -> bool)
    19   val not_eof: T -> bool
    20   val $$$ : string -> T list -> string * T list
    21   val name: T list -> string * T list
    22   val sectioned: string list -> T list -> (string list * (string * string list) list) * T list
    23   type src
    24   val syntax: string -> (T list -> 'a * T list) -> ('a -> 'b) -> src -> 'b
    25 end;
    26 
    27 structure Args: ARGS =
    28 struct
    29 
    30 
    31 (** datatype T **)
    32 
    33 datatype kind = Ident | String | Keyword | EOF;
    34 datatype T = Arg of kind * string;
    35 
    36 fun val_of (Arg (_, x)) = x;
    37 
    38 fun str_of (Arg (Ident, x)) = enclose "'" "'" x
    39   | str_of (Arg (String, x)) = quote x
    40   | str_of (Arg (Keyword, x)) = x;
    41 
    42 fun arg kind x = Arg (kind, x);
    43 val ident = arg Ident;
    44 val string = arg String;
    45 val keyword = arg Keyword;
    46 
    47 
    48 (* eof *)
    49 
    50 val eof = arg EOF "";
    51 
    52 fun is_eof (Arg (EOF, _)) = true
    53   | is_eof _ = false;
    54 
    55 val stopper = (eof, is_eof);
    56 val not_eof = not o is_eof;
    57 
    58 
    59 
    60 (** scanners **)
    61 
    62 (* basic *)
    63 
    64 fun $$$ x = Scan.one (fn Arg (k, y) => (k = Ident orelse k = Keyword) andalso x = y) >> val_of;
    65 val name = Scan.one (fn (Arg (k, x)) => k = Ident orelse k = String) >> val_of;
    66 
    67 
    68 (* sections *)
    69 
    70 val no_colon = Scan.one (fn Arg (k, x) => k = String orelse x <> ":");
    71 val sname = name --| Scan.ahead no_colon;
    72 
    73 fun sect s = ($$$ s --| $$$ ":") -- Scan.repeat sname;
    74 
    75 fun any_sect [] = Scan.fail
    76   | any_sect (s :: ss) = sect s || any_sect ss;
    77 
    78 fun sectioned ss =
    79   Scan.repeat sname -- Scan.repeat (any_sect ss);
    80 
    81 
    82 
    83 (** type src **)
    84 
    85 type src = (string * T list) * Position.T;
    86 
    87 fun err_in_src kind msg ((s, args), pos) =
    88   error (space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos ^ ": " ^ msg);
    89 
    90 
    91 (* argument syntax *)
    92 
    93 fun syntax kind scan f (src as ((s, args), pos)) =
    94   (case handle_error (Scan.error (Scan.finite stopper scan)) args of
    95     OK (x, []) => f x
    96   | OK (_, args') => err_in_src kind "bad arguments" ((s, args'), pos)
    97   | Error msg => err_in_src kind ("\n" ^ msg) src);
    98 
    99 
   100 end;