# HG changeset patch
# User wenzelm
# Date 1130531287 -7200
# Node ID 1095d2213b9ddc24b794b2357399247649646bcc
# Parent  d5d5ad4b78c5b0bcb161caef33f93f39673c6019
syntax for literal facts;

diff -r d5d5ad4b78c5 -r 1095d2213b9d src/Pure/Isar/args.ML
--- 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 *)
diff -r d5d5ad4b78c5 -r 1095d2213b9d src/Pure/Isar/attrib.ML
--- 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);
diff -r d5d5ad4b78c5 -r 1095d2213b9d src/Pure/Isar/outer_parse.ML
--- 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);