# HG changeset patch
# User wenzelm
# Date 1464786103 -7200
# Node ID 921a5be5413293388825d402a5e07c97c109c808
# Parent  c1b15830549e374787fc4ded5f7e7a59f9e8f080
support rat numerals via special antiquotation syntax;

diff -r c1b15830549e -r 921a5be54132 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Jun 01 10:59:57 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Jun 01 15:01:43 2016 +0200
@@ -29,7 +29,12 @@
             ML_Syntax.print_position pos ^ "));\n";
           val body =
             "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
-        in (K (env, body), ctxt') end));
+        in (K (env, body), ctxt') end) #>
+
+  ML_Antiquotation.value @{binding rat}
+    (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
+      Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
+        "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))))
 
 
 (* formal entities *)
diff -r c1b15830549e -r 921a5be54132 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Jun 01 10:59:57 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML	Wed Jun 01 15:01:43 2016 +0200
@@ -218,6 +218,8 @@
 
 val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
 
+val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) [];
+
 val scan_real =
   scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
   scan_decint @@@ scan_exp;
@@ -265,6 +267,19 @@
 end;
 
 
+(* rat antiquotation *)
+
+val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none);
+
+val scan_rat_antiq =
+  Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos
+    >> (fn ((pos1, (pos2, body)), pos3) =>
+      {start = Position.range_position (pos1, pos2),
+       stop = Position.none,
+       range = Position.range (pos1, pos3),
+       body = rat_name @ body});
+
+
 (* scan tokens *)
 
 local
@@ -290,6 +305,7 @@
 val scan_ml_antiq =
   Antiquote.scan_control >> Antiquote.Control ||
   Antiquote.scan_antiq >> Antiquote.Antiq ||
+  scan_rat_antiq >> Antiquote.Antiq ||
   scan_ml >> Antiquote.Text;
 
 fun recover msg =
diff -r c1b15830549e -r 921a5be54132 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Wed Jun 01 10:59:57 2016 +0200
+++ b/src/Pure/ML/ml_lex.scala	Wed Jun 01 15:01:43 2016 +0200
@@ -190,6 +190,9 @@
         sign ~ ("0x" ~ hex ^^ { case x ~ y => x + y } | dec) ^^
           { case x ~ y => Token(Kind.INT, x + y) }
 
+      val rat =
+        decint ~ opt("/" ~ dec) ^^ { case x ~ None => x case x ~ Some(y ~ z) => x + y + z }
+
       val real =
         (decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^
           { case x ~ y ~ z ~ w => x + y + z + w } |
@@ -203,7 +206,9 @@
       val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x))
 
       val ml_control = control ^^ (x => Token(Kind.CONTROL, x))
-      val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x))
+      val ml_antiq =
+        "@" ~ rat ^^ { case x ~ y => Token(Kind.ANTIQ, x + y) } |
+        antiq ^^ (x => Token(Kind.ANTIQ, x))
 
       val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x))