# HG changeset patch
# User wenzelm
# Date 1368527471 -7200
# Node ID 4f3a5f4c1169fd0e39a1c49174a68ac5ca4da868
# Parent  237ee582d66386613be80025ca5907cddbaff6e8
more antiquotations;

diff -r 237ee582d663 -r 4f3a5f4c1169 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue May 14 12:22:18 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue May 14 12:31:11 2013 +0200
@@ -975,7 +975,7 @@
   Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
       Toplevel.keep (fn state =>
-       (case limit of NONE => () | SOME n => Options.default_put_int "goals_limit" n;
+       (case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 
diff -r 237ee582d663 -r 4f3a5f4c1169 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Tue May 14 12:22:18 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Tue May 14 12:31:11 2013 +0200
@@ -67,9 +67,9 @@
 
   inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
 
-  value (Binding.name "option_default") (Scan.lift Args.name >> (fn name =>
-    let val typ = Options.default_typ name
-    in "fn () => Options.default_" ^ typ ^ " " ^ ML_Syntax.print_string name end)) #>
+  value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
+    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
+     ML_Syntax.print_string name))) #>
 
   value (Binding.name "binding")
     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
diff -r 237ee582d663 -r 4f3a5f4c1169 src/Tools/WWW_Find/Start_WWW_Find.thy
--- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Tue May 14 12:22:18 2013 +0200
+++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Tue May 14 12:31:11 2013 +0200
@@ -5,7 +5,7 @@
 theory Start_WWW_Find imports WWW_Find begin
 
 ML {*
-  Options.default_put_bool "show_question_marks" false;
+  Options.default_put_bool @{option show_question_marks} false;
   YXML_Find_Theorems.init ();
   val port = Markup.parse_int (getenv "SCGIPORT");
   ScgiServer.server' 10 "/" port;