--- 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} + )
;
--- 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
--- 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
--- 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(""))) ^^