# HG changeset patch
# User wenzelm
# Date 1288449238 -7200
# Node ID 012ed4426fda048b34053d516acd5dd2ee4fa321
# Parent  47f572aff50a1a22f0ee17103845820b1d793c93
support for real valued configuration options;

diff -r 47f572aff50a -r 012ed4426fda NEWS
--- a/NEWS	Sat Oct 30 15:26:40 2010 +0200
+++ b/NEWS	Sat Oct 30 16:33:58 2010 +0200
@@ -56,6 +56,10 @@
 
 *** Pure ***
 
+* Support for real valued configuration options, using simplistic
+floating-point notation that coincides with the inner syntax for
+float_token.
+
 * Interpretation command 'interpret' accepts a list of equations like
 'interpretation' does.
 
diff -r 47f572aff50a -r 012ed4426fda doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 30 16:33:58 2010 +0200
@@ -597,6 +597,8 @@
   bool Config.T * (theory -> theory)"} \\
   @{index_ML Attrib.config_int: "string -> (Context.generic -> int) ->
   int Config.T * (theory -> theory)"} \\
+  @{index_ML Attrib.config_real: "string -> (Context.generic -> real) ->
+  real Config.T * (theory -> theory)"} \\
   @{index_ML Attrib.config_string: "string -> (Context.generic -> string) ->
   string Config.T * (theory -> theory)"} \\
   \end{mldecls}
@@ -617,9 +619,9 @@
   needs to be applied to the theory initially, in order to make
   concrete declaration syntax available to the user.
 
-  \item @{ML Attrib.config_int} and @{ML Attrib.config_string} work
-  like @{ML Attrib.config_bool}, but for types @{ML_type int} and
-  @{ML_type string}, respectively.
+  \item @{ML Attrib.config_int}, @{ML Attrib.config_real}, and @{ML
+  Attrib.config_string} work like @{ML Attrib.config_bool}, but for
+  types @{ML_type int} and @{ML_type string}, respectively.
 
   \end{description}
 *}
@@ -652,6 +654,17 @@
   ML_val {* @{assert} (Config.get @{context} my_flag = true) *}
 qed
 
+text {* Here is another example involving ML type @{ML_type real}
+  (floating-point numbers). *}
+
+ML {*
+  val (airspeed_velocity, airspeed_velocity_setup) =
+    Attrib.config_real "airspeed_velocity" (K 0.0)
+*}
+setup airspeed_velocity_setup
+
+declare [[airspeed_velocity = 9.9]]
+
 
 section {* Names \label{sec:names} *}
 
diff -r 47f572aff50a -r 012ed4426fda doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Oct 30 16:33:58 2010 +0200
@@ -794,6 +794,8 @@
 \verb|  bool Config.T * (theory -> theory)| \\
   \indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline%
 \verb|  int Config.T * (theory -> theory)| \\
+  \indexdef{}{ML}{Attrib.config\_real}\verb|Attrib.config_real: string -> (Context.generic -> real) ->|\isasep\isanewline%
+\verb|  real Config.T * (theory -> theory)| \\
   \indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline%
 \verb|  string Config.T * (theory -> theory)| \\
   \end{mldecls}
@@ -813,9 +815,8 @@
   needs to be applied to the theory initially, in order to make
   concrete declaration syntax available to the user.
 
-  \item \verb|Attrib.config_int| and \verb|Attrib.config_string| work
-  like \verb|Attrib.config_bool|, but for types \verb|int| and
-  \verb|string|, respectively.
+  \item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for
+  types \verb|int| and \verb|string|, respectively.
 
   \end{description}%
 \end{isamarkuptext}%
@@ -1019,6 +1020,34 @@
 %
 \endisadelimproof
 %
+\begin{isamarkuptext}%
+Here is another example involving ML type \verb|real|
+  (floating-point numbers).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ {\isacharparenleft}airspeed{\isacharunderscore}velocity{\isacharcomma}\ airspeed{\isacharunderscore}velocity{\isacharunderscore}setup{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ Attrib{\isachardot}config{\isacharunderscore}real\ {\isachardoublequote}airspeed{\isacharunderscore}velocity{\isachardoublequote}\ {\isacharparenleft}K\ {\isadigit{0}}{\isachardot}{\isadigit{0}}{\isacharparenright}\isanewline
+{\isacharverbatimclose}\isanewline
+\isacommand{setup}\isamarkupfalse%
+\ airspeed{\isacharunderscore}velocity{\isacharunderscore}setup%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{9}}{\isachardot}{\isadigit{9}}{\isacharbrackright}{\isacharbrackright}%
 \isamarkupsection{Names \label{sec:names}%
 }
 \isamarkuptrue%
diff -r 47f572aff50a -r 012ed4426fda doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Oct 30 16:33:58 2010 +0200
@@ -6,16 +6,15 @@
 
 section {* Configuration options *}
 
-text {*
-  Isabelle/Pure maintains a record of named configuration options
-  within the theory or proof context, with values of type @{ML_type
-  bool}, @{ML_type int}, or @{ML_type string}.  Tools may declare
-  options in ML, and then refer to these values (relative to the
-  context).  Thus global reference variables are easily avoided.  The
-  user may change the value of a configuration option by means of an
-  associated attribute of the same name.  This form of context
-  declaration works particularly well with commands such as @{command
-  "declare"} or @{command "using"}.
+text {* Isabelle/Pure maintains a record of named configuration
+  options within the theory or proof context, with values of type
+  @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
+  string}.  Tools may declare options in ML, and then refer to these
+  values (relative to the context).  Thus global reference variables
+  are easily avoided.  The user may change the value of a
+  configuration option by means of an associated attribute of the same
+  name.  This form of context declaration works particularly well with
+  commands such as @{command "declare"} or @{command "using"}.
 
   For historical reasons, some tools cannot take the full proof
   context into account and merely refer to the background theory.
@@ -27,7 +26,7 @@
   \end{matharray}
 
   \begin{rail}
-    name ('=' ('true' | 'false' | int | name))?
+    name ('=' ('true' | 'false' | int | float | name))?
   \end{rail}
 
   \begin{description}
diff -r 47f572aff50a -r 012ed4426fda doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 16:33:58 2010 +0200
@@ -366,7 +366,7 @@
 
   \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   \begin{rail}
-    atom: nameref | typefree | typevar | var | nat | keyword
+    atom: nameref | typefree | typevar | var | nat | float | keyword
     ;
     arg: atom | '(' args ')' | '[' args ']'
     ;
diff -r 47f572aff50a -r 012ed4426fda doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Oct 30 16:33:58 2010 +0200
@@ -27,13 +27,14 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Isabelle/Pure maintains a record of named configuration options
-  within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|.  Tools may declare
-  options in ML, and then refer to these values (relative to the
-  context).  Thus global reference variables are easily avoided.  The
-  user may change the value of a configuration option by means of an
-  associated attribute of the same name.  This form of context
-  declaration works particularly well with commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
+Isabelle/Pure maintains a record of named configuration
+  options within the theory or proof context, with values of type
+  \verb|bool|, \verb|int|, \verb|real|, or \verb|string|.  Tools may declare options in ML, and then refer to these
+  values (relative to the context).  Thus global reference variables
+  are easily avoided.  The user may change the value of a
+  configuration option by means of an associated attribute of the same
+  name.  This form of context declaration works particularly well with
+  commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}.
 
   For historical reasons, some tools cannot take the full proof
   context into account and merely refer to the background theory.
@@ -45,7 +46,7 @@
   \end{matharray}
 
   \begin{rail}
-    name ('=' ('true' | 'false' | int | name))?
+    name ('=' ('true' | 'false' | int | float | name))?
   \end{rail}
 
   \begin{description}
diff -r 47f572aff50a -r 012ed4426fda doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Oct 30 16:33:58 2010 +0200
@@ -392,7 +392,7 @@
 
   \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   \begin{rail}
-    atom: nameref | typefree | typevar | var | nat | keyword
+    atom: nameref | typefree | typevar | var | nat | float | keyword
     ;
     arg: atom | '(' args ')' | '[' args ']'
     ;
diff -r 47f572aff50a -r 012ed4426fda src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Oct 30 15:26:40 2010 +0200
+++ b/src/Pure/Isar/args.ML	Sat Oct 30 16:33:58 2010 +0200
@@ -224,7 +224,7 @@
   let
     val keyword_symid = token (Parse.keyword_with is_symid);
     fun atom blk = Parse.group "argument"
-      (ident || keyword_symid || string || alt_string ||
+      (ident || keyword_symid || string || alt_string || token Parse.float_number ||
         (if blk then token (Parse.$$$ ",") else Scan.fail));
 
     fun args blk x = Scan.optional (args1 blk) [] x
diff -r 47f572aff50a -r 012ed4426fda src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Oct 30 15:26:40 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Oct 30 16:33:58 2010 +0200
@@ -38,10 +38,13 @@
   val internal: (morphism -> attribute) -> src
   val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
+  val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
   val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
   val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
-  val config_string_global: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
+  val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
+  val config_string_global:
+    bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
 end;
 
 structure Attrib: ATTRIB =
@@ -353,6 +356,7 @@
       equals -- Args.$$$ "true" >> K (Config.Bool true) ||
       Scan.succeed (Config.Bool true)
   | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
+  | scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real
   | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
 
 fun scan_config thy config =
@@ -380,10 +384,12 @@
 
 val config_bool   = declare_config Config.Bool Config.bool false;
 val config_int    = declare_config Config.Int Config.int false;
+val config_real   = declare_config Config.Real Config.real false;
 val config_string = declare_config Config.String Config.string false;
 
 val config_bool_global   = declare_config Config.Bool Config.bool true;
 val config_int_global    = declare_config Config.Int Config.int true;
+val config_real_global   = declare_config Config.Real Config.real true;
 val config_string_global = declare_config Config.String Config.string true;
 
 end;
diff -r 47f572aff50a -r 012ed4426fda src/Pure/config.ML
--- a/src/Pure/config.ML	Sat Oct 30 15:26:40 2010 +0200
+++ b/src/Pure/config.ML	Sat Oct 30 16:33:58 2010 +0200
@@ -6,13 +6,14 @@
 
 signature CONFIG =
 sig
-  datatype value = Bool of bool | Int of int | String of string
+  datatype value = Bool of bool | Int of int | Real of real | String of string
   val print_value: value -> string
   val print_type: value -> string
   type 'a T
   type raw = value T
   val bool: raw -> bool T
   val int: raw -> int T
+  val real: raw -> real T
   val string: raw -> string T
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
@@ -37,19 +38,23 @@
 datatype value =
   Bool of bool |
   Int of int |
+  Real of real |
   String of string;
 
 fun print_value (Bool true) = "true"
   | print_value (Bool false) = "false"
   | print_value (Int i) = signed_string_of_int i
+  | print_value (Real x) = signed_string_of_real x
   | print_value (String s) = quote s;
 
 fun print_type (Bool _) = "bool"
   | print_type (Int _) = "int"
+  | print_type (Real _) = "real"
   | print_type (String _) = "string";
 
 fun same_type (Bool _) (Bool _) = true
   | same_type (Int _) (Int _) = true
+  | same_type (Real _) (Real _) = true
   | same_type (String _) (String _) = true
   | same_type _ _ = false;
 
@@ -78,6 +83,7 @@
 
 val bool = coerce Bool (fn Bool b => b);
 val int = coerce Int (fn Int i => i);
+val real = coerce Real (fn Real x => x);
 val string = coerce String (fn String s => s);
 
 fun get_generic context (Config {get_value, ...}) = get_value context;
@@ -118,7 +124,8 @@
     fun map_value f (context as Context.Proof _) =
           let val context' = update_value f context in
             if global andalso
-              get_value (Context.Theory (Context.theory_of context')) <> get_value context'
+              print_value (get_value (Context.Theory (Context.theory_of context'))) <>
+                print_value (get_value context')
             then (warning ("Ignoring local change of global option " ^ quote name); context)
             else context'
           end
diff -r 47f572aff50a -r 012ed4426fda src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Oct 30 15:26:40 2010 +0200
+++ b/src/Pure/library.ML	Sat Oct 30 16:33:58 2010 +0200
@@ -130,6 +130,10 @@
   val read_int: string list -> int * string list
   val oct_char: string -> string
 
+  (*reals*)
+  val string_of_real: real -> string
+  val signed_string_of_real: real -> string
+
   (*strings*)
   val nth_string: string -> int -> string
   val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
@@ -668,6 +672,15 @@
 
 
 
+(** reals **)
+
+val string_of_real = Real.fmt (StringCvt.GEN NONE);
+
+fun signed_string_of_real x =
+  if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
+
+
+
 (** strings **)
 
 (* functions tuned for strings, avoiding explode *)