# HG changeset patch
# User wenzelm
# Date 910621922 -3600
# Node ID 3f824514ad88e0946fcf14370a5507f8448646d1
# Parent  262ce90e47369b70cfdb5810197787b89dd37287
Concrete argument syntax (for attributes, methods etc.).

diff -r 262ce90e4736 -r 3f824514ad88 src/Pure/Isar/args.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/args.ML	Mon Nov 09 15:32:02 1998 +0100
@@ -0,0 +1,100 @@
+(*  Title:      Pure/Isar/args.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Concrete argument syntax (for attributes, methods etc.).
+
+TODO:
+  - sectioned: generalize sname to attributed thms;
+*)
+
+signature ARGS =
+sig
+  type T
+  val val_of: T -> string
+  val ident: string -> T
+  val string: string -> T
+  val keyword: string -> T
+  val stopper: T * (T -> bool)
+  val not_eof: T -> bool
+  val $$$ : string -> T list -> string * T list
+  val name: T list -> string * T list
+  val sectioned: string list -> T list -> (string list * (string * string list) list) * T list
+  type src
+  val syntax: string -> (T list -> 'a * T list) -> ('a -> 'b) -> src -> 'b
+end;
+
+structure Args: ARGS =
+struct
+
+
+(** datatype T **)
+
+datatype kind = Ident | String | Keyword | EOF;
+datatype T = Arg of kind * string;
+
+fun val_of (Arg (_, x)) = x;
+
+fun str_of (Arg (Ident, x)) = enclose "'" "'" x
+  | str_of (Arg (String, x)) = quote x
+  | str_of (Arg (Keyword, x)) = x;
+
+fun arg kind x = Arg (kind, x);
+val ident = arg Ident;
+val string = arg String;
+val keyword = arg Keyword;
+
+
+(* eof *)
+
+val eof = arg EOF "";
+
+fun is_eof (Arg (EOF, _)) = true
+  | is_eof _ = false;
+
+val stopper = (eof, is_eof);
+val not_eof = not o is_eof;
+
+
+
+(** scanners **)
+
+(* basic *)
+
+fun $$$ x = Scan.one (fn Arg (k, y) => (k = Ident orelse k = Keyword) andalso x = y) >> val_of;
+val name = Scan.one (fn (Arg (k, x)) => k = Ident orelse k = String) >> val_of;
+
+
+(* sections *)
+
+val no_colon = Scan.one (fn Arg (k, x) => k = String orelse x <> ":");
+val sname = name --| Scan.ahead no_colon;
+
+fun sect s = ($$$ s --| $$$ ":") -- Scan.repeat sname;
+
+fun any_sect [] = Scan.fail
+  | any_sect (s :: ss) = sect s || any_sect ss;
+
+fun sectioned ss =
+  Scan.repeat sname -- Scan.repeat (any_sect ss);
+
+
+
+(** type src **)
+
+type src = (string * T list) * Position.T;
+
+fun err_in_src kind msg ((s, args), pos) =
+  error (space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos ^ ": " ^ msg);
+
+
+(* argument syntax *)
+
+fun syntax kind scan f (src as ((s, args), pos)) =
+  (case handle_error (Scan.error (Scan.finite stopper scan)) args of
+    OK (x, []) => f x
+  | OK (_, args') => err_in_src kind "bad arguments" ((s, args'), pos)
+  | Error msg => err_in_src kind ("\n" ^ msg) src);
+
+
+end;