# HG changeset patch
# User wenzelm
# Date 1343655060 -7200
# Node ID e777363440d6f7735d55ad4b75175a81d412fdbd
# Parent  f651323139f03a8c7a8328abf7cd664c14f0c648
allow negative int values as well, according to real = int | float;

diff -r f651323139f0 -r e777363440d6 doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Mon Jul 30 14:38:45 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Mon Jul 30 15:31:00 2012 +0200
@@ -60,7 +60,9 @@
     ;
     options: @'options' opts
     ;
-    opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']'
+    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
+    ;
+    value: @{syntax name} | @{syntax real}
     ;
     theories: @'theories' opts? ( @{syntax name} + )
     ;
diff -r f651323139f0 -r e777363440d6 doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Mon Jul 30 14:38:45 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Mon Jul 30 15:31:00 2012 +0200
@@ -139,7 +139,7 @@
 \rail@bar
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nont{\isa{value}}[]
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@endbar
@@ -148,6 +148,13 @@
 \rail@endplus
 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
 \rail@end
+\rail@begin{2}{\isa{value}}
+\rail@bar
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.real}{\mbox{\isa{real}}}}[]
+\rail@endbar
+\rail@end
 \rail@begin{2}{\isa{theories}}
 \rail@term{\isa{\isakeyword{theories}}}[]
 \rail@bar
diff -r f651323139f0 -r e777363440d6 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Jul 30 14:38:45 2012 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 30 15:31:00 2012 +0200
@@ -74,6 +74,7 @@
     kind == Token.Kind.VERBATIM ||
     kind == Token.Kind.COMMENT
   def is_ident: Boolean = kind == Token.Kind.IDENT
+  def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
   def is_string: Boolean = kind == Token.Kind.STRING
   def is_nat: Boolean = kind == Token.Kind.NAT
   def is_float: Boolean = kind == Token.Kind.FLOAT
diff -r f651323139f0 -r e777363440d6 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Jul 30 14:38:45 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Jul 30 15:31:00 2012 +0200
@@ -41,7 +41,11 @@
     {
       val option_name = atom("option name", _.is_xname)
       val option_type = atom("option type", _.is_ident)
-      val option_value = atom("option value", tok => tok.is_name || tok.is_float)
+
+      val option_value =
+        opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
+          { case s ~ n => if (s.isDefined) "-" + n else n } |
+        atom("option value", tok => tok.is_name || tok.is_float)
 
       keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^