# HG changeset patch
# User nipkow
# Date 1227962233 -3600
# Node ID 3ef9489eeef525f256defef7c6b3c6f372b11ba0
# Parent  b3fc3a62247a7416b7f162d6339cd08c3107682b
New lexical item "float".

diff -r b3fc3a62247a -r 3ef9489eeef5 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/General/markup.ML	Sat Nov 29 13:37:13 2008 +0100
@@ -53,6 +53,7 @@
   val boundN: string val bound: T
   val varN: string val var: T
   val numN: string val num: T
+  val floatN: string val float: T
   val xnumN: string val xnum: T
   val xstrN: string val xstr: T
   val literalN: string val literal: T
@@ -203,6 +204,7 @@
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
 val (numN, num) = markup_elem "num";
+val (floatN, float) = markup_elem "float";
 val (xnumN, xnum) = markup_elem "xnum";
 val (xstrN, xstr) = markup_elem "xstr";
 val (literalN, literal) = markup_elem "literal";
diff -r b3fc3a62247a -r 3ef9489eeef5 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sat Nov 29 13:37:13 2008 +0100
@@ -30,6 +30,7 @@
   val read_nat: string -> int option
   val read_int: string -> int option
   val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
+  val read_float: string -> {mant: int, exp: int}
   val fixedN: string
   val constN: string
 end;
@@ -40,7 +41,7 @@
   val is_xid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
-    NumSy | XNumSy | StrSy | Space | Comment | EOF
+    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
   datatype token = Token of token_kind * string * Position.range
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
@@ -98,6 +99,8 @@
 
 val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
 val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
+val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
+val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
 val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
 
@@ -111,7 +114,7 @@
 
 datatype token_kind =
   Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
-  NumSy | XNumSy | StrSy | Space | Comment | EOF;
+  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
 
 datatype token = Token of token_kind * string * Position.range;
 
@@ -142,7 +145,8 @@
 val tidT = Type ("tid", []);
 val tvarT = Type ("tvar", []);
 
-val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
+val terminals =
+  ["id", "longid", "var", "tid", "tvar", "num", "float", "xnum", "xstr"];
 val is_terminal = member (op =) terminals;
 
 
@@ -156,6 +160,7 @@
   | TFreeSy     => Markup.tfree
   | TVarSy      => Markup.tvar
   | NumSy       => Markup.num
+  | FloatSy     => Markup.float
   | XNumSy      => Markup.xnum
   | StrSy       => Markup.xstr
   | Space       => Markup.none
@@ -187,6 +192,7 @@
   | predef_term "tid" = SOME (Token (TFreeSy, "tid", Position.no_range))
   | predef_term "tvar" = SOME (Token (TVarSy, "tvar", Position.no_range))
   | predef_term "num" = SOME (Token (NumSy, "num", Position.no_range))
+  | predef_term "float" = SOME (Token (FloatSy, "float", Position.no_range))
   | predef_term "xnum" = SOME (Token (XNumSy, "xnum", Position.no_range))
   | predef_term "xstr" = SOME (Token (StrSy, "xstr", Position.no_range))
   | predef_term _ = NONE;
@@ -234,6 +240,7 @@
       scan_tvar >> token TVarSy ||
       scan_var >> token VarSy ||
       scan_tid >> token TFreeSy ||
+      scan_float >> token FloatSy ||
       scan_num >> token NumSy ||
       $$$ "#" @@@ scan_num >> token XNumSy ||
       scan_longid >> token LongIdentSy ||
@@ -380,4 +387,16 @@
 
 end;
 
+fun read_float str =
+  let
+    val (sign, cs) =
+      (case Symbol.explode str of  "-" :: cs => (~1, cs) | cs => (1, cs));
+    val (intpart,fracpart) =
+      (case take_prefix Symbol.is_digit cs of
+        (intpart, "." :: fracpart) => (intpart,fracpart)
+      | _ =>  sys_error "read_float")
+  in {mant = sign * #1 (Library.read_int (intpart@fracpart)),
+      exp = length fracpart}
+  end
+
 end;
diff -r b3fc3a62247a -r 3ef9489eeef5 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Sat Nov 29 13:37:13 2008 +0100
@@ -387,7 +387,7 @@
 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
 val standard_token_classes =
-  ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];
+  ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
 
 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
 
diff -r b3fc3a62247a -r 3ef9489eeef5 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Nov 29 13:37:13 2008 +0100
@@ -391,7 +391,8 @@
 val basic_nonterms =
   (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
     SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
-    "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]);
+    "asms", SynExt.any_, SynExt.sprop, "num_const", "float_const",
+    "index", "struct"]);
 
 
 
diff -r b3fc3a62247a -r 3ef9489eeef5 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Nov 28 17:43:06 2008 +0100
+++ b/src/Pure/pure_thy.ML	Sat Nov 29 13:37:13 2008 +0100
@@ -321,6 +321,7 @@
     ("",            typ "var => logic",                Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
+    ("_constify",   typ "float => float_const",        Delimfix "_"),
     ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),