added numeral, which supercedes num, xnum, float;
authorwenzelm
Fri Jan 02 19:38:13 2009 +0100 (2009-01-02)
changeset 293186337d1cb2ba0
parent 29317 9faf1dfb4e7c
child 29319 592503fd6dad
added numeral, which supercedes num, xnum, float;
renamed xstr to inner_string;
src/Pure/General/markup.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/General/markup.ML	Fri Jan 02 19:30:12 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Fri Jan 02 19:38:13 2009 +0100
     1.3 @@ -52,11 +52,9 @@
     1.4    val skolemN: string val skolem: T
     1.5    val boundN: string val bound: T
     1.6    val varN: string val var: T
     1.7 -  val numN: string val num: T
     1.8 -  val floatN: string val float: T
     1.9 -  val xnumN: string val xnum: T
    1.10 -  val xstrN: string val xstr: T
    1.11 +  val numeralN: string val numeral: T
    1.12    val literalN: string val literal: T
    1.13 +  val inner_stringN: string val inner_string: T
    1.14    val inner_commentN: string val inner_comment: T
    1.15    val sortN: string val sort: T
    1.16    val typN: string val typ: T
    1.17 @@ -203,11 +201,9 @@
    1.18  val (skolemN, skolem) = markup_elem "skolem";
    1.19  val (boundN, bound) = markup_elem "bound";
    1.20  val (varN, var) = markup_elem "var";
    1.21 -val (numN, num) = markup_elem "num";
    1.22 -val (floatN, float) = markup_elem "float";
    1.23 -val (xnumN, xnum) = markup_elem "xnum";
    1.24 -val (xstrN, xstr) = markup_elem "xstr";
    1.25 +val (numeralN, numeral) = markup_elem "numeral";
    1.26  val (literalN, literal) = markup_elem "literal";
    1.27 +val (inner_stringN, inner_string) = markup_elem "inner_string";
    1.28  val (inner_commentN, inner_comment) = markup_elem "inner_comment";
    1.29  
    1.30  val (sortN, sort) = markup_elem "sort";
     2.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jan 02 19:30:12 2009 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jan 02 19:38:13 2009 +0100
     2.3 @@ -408,9 +408,8 @@
     2.4     ("free", free_or_skolem),
     2.5     ("bound", plain_markup Markup.bound),
     2.6     ("var", var_or_skolem),
     2.7 -   ("num", plain_markup Markup.num),
     2.8 -   ("xnum", plain_markup Markup.xnum),
     2.9 -   ("xstr", plain_markup Markup.xstr)];
    2.10 +   ("numeral", plain_markup Markup.numeral),
    2.11 +   ("inner_string", plain_markup Markup.inner_string)];
    2.12  
    2.13  in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
    2.14  
     3.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Jan 02 19:30:12 2009 +0100
     3.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Jan 02 19:38:13 2009 +0100
     3.3 @@ -169,10 +169,10 @@
     3.4    | VarSy       => Markup.var
     3.5    | TFreeSy     => Markup.tfree
     3.6    | TVarSy      => Markup.tvar
     3.7 -  | NumSy       => Markup.num
     3.8 -  | FloatSy     => Markup.float
     3.9 -  | XNumSy      => Markup.xnum
    3.10 -  | StrSy       => Markup.xstr
    3.11 +  | NumSy       => Markup.numeral
    3.12 +  | FloatSy     => Markup.numeral
    3.13 +  | XNumSy      => Markup.numeral
    3.14 +  | StrSy       => Markup.inner_string
    3.15    | Space       => Markup.none
    3.16    | Comment     => Markup.inner_comment
    3.17    | EOF         => Markup.none;
     4.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 19:30:12 2009 +0100
     4.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Jan 02 19:38:13 2009 +0100
     4.3 @@ -379,7 +379,7 @@
     4.4  
     4.5  fun stamp_trfun s (c, f) = (c, (f, s));
     4.6  fun mk_trfun tr = stamp_trfun (stamp ()) tr;
     4.7 -fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
     4.8 +fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
     4.9  
    4.10  
    4.11  (* token translations *)
    4.12 @@ -387,7 +387,7 @@
    4.13  fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
    4.14  
    4.15  val standard_token_classes =
    4.16 -  ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
    4.17 +  ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
    4.18  
    4.19  val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
    4.20