--- a/src/Pure/Isar/args.ML Fri Oct 28 22:28:06 2005 +0200
+++ b/src/Pure/Isar/args.ML Fri Oct 28 22:28:07 2005 +0200
@@ -14,6 +14,7 @@
val string_of: T -> string
val mk_ident: string * Position.T -> T
val mk_string: string * Position.T -> T
+ val mk_alt_string: string * Position.T -> T
val mk_keyword: string * Position.T -> T
val mk_name: string -> T
val mk_typ: typ -> T
@@ -46,6 +47,7 @@
val mode: string -> 'a * T list -> bool * ('a * T list)
val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
val name: T list -> string * T list
+ val alt_name: T list -> string * T list
val symbol: T list -> string * T list
val liberal_name: T list -> string * T list
val nat: T list -> int * T list
@@ -102,7 +104,7 @@
designates an intermediate state of internalization -- it is NOT
meant to persist.*)
-datatype kind = Ident | String | Keyword | EOF;
+datatype kind = Ident | String | AltString | Keyword | EOF;
type symbol = kind * string * Position.T;
@@ -121,7 +123,8 @@
datatype T = Arg of symbol * slot;
fun string_of (Arg ((Ident, x, _), _)) = x
- | string_of (Arg ((String, x, _), _)) = Library.quote x
+ | string_of (Arg ((String, x, _), _)) = quote x
+ | string_of (Arg ((AltString, x, _), _)) = enclose "`" "`" x
| string_of (Arg ((Keyword, x, _), _)) = x
| string_of (Arg ((EOF, _, _), _)) = "";
@@ -136,6 +139,7 @@
val mk_ident = mk_symbol Ident;
val mk_string = mk_symbol String;
+val mk_alt_string = mk_symbol AltString;
val mk_keyword = mk_symbol Keyword;
val mk_name = mk_value "<name>" o Name;
val mk_typ = mk_value "<typ>" o Typ;
@@ -227,6 +231,9 @@
val named =
touch (Scan.one (fn Arg ((k, _, _), _) => k = Ident orelse k = String));
+val alt_string =
+ touch (Scan.one (fn Arg ((k, _, _), _) => k = AltString));
+
val symbolic =
touch (Scan.one (fn Arg ((k, x, _), _) => k = Keyword andalso OuterLex.is_sid x));
@@ -251,6 +258,7 @@
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
val name = named >> sym_of;
+val alt_name = alt_string >> sym_of;
val symbol = symbolic >> sym_of;
val liberal_name = symbol || name;
@@ -289,7 +297,7 @@
fun named_name intern = internal_name || named >> evaluate Name intern;
fun named_typ readT = internal_typ || named >> evaluate Typ readT;
fun named_term read = internal_term || named >> evaluate Term read;
-fun named_fact get = internal_fact || named >> evaluate Fact get;
+fun named_fact get = internal_fact || (alt_string || named) >> evaluate Fact get;
(* terms and types *)
--- a/src/Pure/Isar/attrib.ML Fri Oct 28 22:28:06 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Oct 28 22:28:07 2005 +0200
@@ -169,11 +169,15 @@
(* theorems *)
fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
- Scan.ahead Args.name -- Args.named_fact (fn name => get st (Name name)) --
- Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
- >> (fn (((name, fact), sel), srcs) =>
+ (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
+ >> (fn (s, fact) => ("", Fact s, fact)) ||
+ Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel
+ >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
+ Scan.ahead Args.name -- Args.named_fact (get st o Name)
+ >> (fn (name, fact) => (name, Name name, fact))) --
+ Args.opt_attribs (intern (theory_of st))
+ >> (fn ((name, thmref, fact), srcs) =>
let
- val thmref = (case sel of NONE => Name name | SOME is => NameSelection (name, is));
val ths = PureThy.select_thm thmref fact;
val atts = map (attrib (theory_of st)) srcs;
val (st', ths') = Thm.applys_attributes ((st, ths), atts);
--- a/src/Pure/Isar/outer_parse.ML Fri Oct 28 22:28:06 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML Fri Oct 28 22:28:07 2005 +0200
@@ -280,6 +280,7 @@
type_ident || type_var || number) >> Args.mk_ident ||
position (keyword_symid is_symid) >> Args.mk_keyword ||
position (string || verbatim) >> Args.mk_string ||
+ position alt_string >> Args.mk_alt_string ||
position (if blk then $$$ "," else Scan.fail) >> Args.mk_keyword);
fun paren_args l r scan = position ($$$ l) -- !!! (scan true -- position ($$$ r))
@@ -313,7 +314,8 @@
nat --| minus >> PureThy.From ||
nat >> PureThy.Single) --| $$$ ")";
-val xthm = (xname -- thm_sel >> NameSelection || xname >> Name) -- opt_attribs;
+val xthm = (alt_string >> Fact || xname -- thm_sel >> NameSelection || xname >> Name)
+ -- opt_attribs;
val xthms1 = Scan.repeat1 xthm;
val name_facts = and_list1 (opt_thm_name "=" -- xthms1);