added Parse.literal_fact with proper inner_syntax markup (source position);
authorwenzelm
Sun Nov 28 20:03:19 2010 +0100 (2010-11-28 ago)
changeset 40793d21aedaa91e7
parent 40792 1d71a45590e4
child 40798 0562a0a5bb93
added Parse.literal_fact with proper inner_syntax markup (source position);
tuned;
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
     1.1 --- a/src/Pure/Isar/parse.ML	Sun Nov 28 19:35:14 2010 +0100
     1.2 +++ b/src/Pure/Isar/parse.ML	Sun Nov 28 20:03:19 2010 +0100
     1.3 @@ -90,6 +90,7 @@
     1.4    val prop_group: string parser
     1.5    val term: string parser
     1.6    val prop: string parser
     1.7 +  val literal_fact: string parser
     1.8    val propp: (string * string list) parser
     1.9    val termp: (string * string list) parser
    1.10    val target: xstring parser
    1.11 @@ -315,14 +316,16 @@
    1.12  
    1.13  (* terms *)
    1.14  
    1.15 -val trm = short_ident || long_ident || sym_ident || term_var || number || string;
    1.16 +val tm = short_ident || long_ident || sym_ident || term_var || number || string;
    1.17  
    1.18 -val term_group = group "term" trm;
    1.19 -val prop_group = group "proposition" trm;
    1.20 +val term_group = group "term" tm;
    1.21 +val prop_group = group "proposition" tm;
    1.22  
    1.23  val term = inner_syntax term_group;
    1.24  val prop = inner_syntax prop_group;
    1.25  
    1.26 +val literal_fact = inner_syntax (group "literal fact" alt_string);
    1.27 +
    1.28  
    1.29  (* patterns *)
    1.30  
     2.1 --- a/src/Pure/Isar/parse_spec.ML	Sun Nov 28 19:35:14 2010 +0100
     2.2 +++ b/src/Pure/Isar/parse_spec.ML	Sun Nov 28 20:03:19 2010 +0100
     2.3 @@ -61,7 +61,7 @@
     2.4  
     2.5  val xthm =
     2.6    Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
     2.7 -  (Parse.alt_string >> Facts.Fact ||
     2.8 +  (Parse.literal_fact >> Facts.Fact ||
     2.9      Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    2.10  
    2.11  val xthms1 = Scan.repeat1 xthm;