# HG changeset patch
# User wenzelm
# Date 1396961976 -7200
# Node ID 8d7d6f17c6a78fc950a1dbc31100074143836ade
# Parent  08982abdcdad7a0b9607b37074e2282074d9bfe5
more uniform ML/document antiquotations;

diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Doc/antiquote_setup.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -201,6 +201,10 @@
       val _ = Context_Position.reports ctxt (map (pair pos) markup);
     in true end;
 
+fun check_system_option ctxt (name, pos) =
+  (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
+    handle ERROR _ => false;
+
 fun check_tool ctxt (name, pos) =
   let
     fun tool dir =
@@ -265,7 +269,7 @@
     entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
     entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
     entity_antiqs no_check "isatt" @{binding setting} #>
-    entity_antiqs no_check "isatt" @{binding system_option} #>
+    entity_antiqs check_system_option "isatt" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>
     entity_antiqs no_check "isatt" @{binding executable} #>
     entity_antiqs check_tool "isatool" @{binding tool} #>
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -124,7 +124,7 @@
             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
           end) ()
   handle TimeLimit.TimeOut =>
-         (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit}))])
+         (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
 
 fun quickcheck_mtd change_options quickcheck_generator =
   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Prolog/prolog.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -2,7 +2,7 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-Options.default_put_bool @{option show_main_goal} true;
+Options.default_put_bool @{system_option show_main_goal} true;
 
 structure Prolog =
 struct
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -285,7 +285,7 @@
 
 type tptp_problem = tptp_line list
 
-fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
 
 fun nameof_tff_atom_type (Atom_type str) = str
   | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Apr 08 14:59:36 2014 +0200
@@ -42,7 +42,7 @@
 ML {*
   if test_all @{context} then ()
   else
-    (Options.default_put_bool @{option ML_exception_trace} true;
+    (Options.default_put_bool @{system_option ML_exception_trace} true;
      default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
      PolyML.Compiler.maxInlineSize := 0)
 *}
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -34,7 +34,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_nitpick}
+    @{system_option auto_nitpick}
     "auto-nitpick"
     "Run Nitpick automatically"
 
@@ -396,6 +396,6 @@
 
 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
 
-val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
+val _ = Try.tool_setup (nitpickN, (50, @{system_option auto_nitpick}, try_nitpick))
 
 end;
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -100,7 +100,7 @@
 
 fun z3_non_commercial () =
   let
-    val flag1 = Options.default_string @{option z3_non_commercial}
+    val flag1 = Options.default_string @{system_option z3_non_commercial}
     val flag2 = getenv "Z3_NON_COMMERCIAL"
   in
     if accepted flag1 then Z3_Non_Commercial_Accepted
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -97,7 +97,7 @@
 
 fun z3_non_commercial () =
   let
-    val flag1 = Options.default_string @{option z3_non_commercial}
+    val flag1 = Options.default_string @{system_option z3_non_commercial}
     val flag2 = getenv "Z3_NON_COMMERCIAL"
   in
     if accepted flag1 then Z3_Non_Commercial_Accepted
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -43,7 +43,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_sledgehammer}
+    @{system_option auto_sledgehammer}
     "auto-sledgehammer"
     "Run Sledgehammer automatically"
 
@@ -72,7 +72,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     NONE
-    @{option sledgehammer_timeout}
+    @{system_option sledgehammer_timeout}
     "Sledgehammer: Time Limit"
     "ATPs will be interrupted after this time (in seconds)"
 
@@ -229,7 +229,7 @@
     |> fold (AList.default (op =))
          [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
           ("timeout",
-           let val timeout = Options.default_int @{option sledgehammer_timeout} in
+           let val timeout = Options.default_int @{system_option sledgehammer_timeout} in
              [if timeout <= 0 then "none" else string_of_int timeout]
            end)]
   end
@@ -472,7 +472,7 @@
       state
   end
 
-val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
 
 val _ =
   Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -25,7 +25,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_methods}
+    @{system_option auto_methods}
     "auto-try0"
     "Try standard proof methods";
 
@@ -193,6 +193,6 @@
 
 fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
 
-val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0));
+val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
 
 end;
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -984,7 +984,7 @@
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
       Toplevel.keep (fn state =>
        (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
-        case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
+        case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -8,17 +8,10 @@
 struct
 
 val _ = Theory.setup
- (ML_Antiquotation.value @{binding option}
+ (ML_Antiquotation.value @{binding system_option}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
-      let
-        val def_pos =
-          Options.default_position name
-            handle ERROR msg => error (msg ^ Position.here pos);
-        val markup =
-          Markup.properties (Position.def_properties_of def_pos)
-            (Markup.entity Markup.system_optionN name);
-        val _ = Context_Position.report ctxt pos markup;
-      in ML_Syntax.print_string name end)) #>
+      (Context_Position.report ctxt pos (Options.default_markup (name, pos));
+        ML_Syntax.print_string name))) #>
 
   ML_Antiquotation.value @{binding theory}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -13,7 +13,7 @@
   val unknownT: string
   type T
   val empty: T
-  val position: T -> string -> Position.T
+  val markup: T -> string * Position.T -> Markup.T
   val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
@@ -27,7 +27,7 @@
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
-  val default_position: string -> Position.T
+  val default_markup: string * Position.T -> Markup.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
@@ -75,9 +75,19 @@
   end;
 
 
-(* declaration *)
+(* markup *)
 
-fun position options name = #pos (check_name options name);
+fun markup options (name, pos) =
+  let
+    val opt =
+      check_name options name
+        handle ERROR msg => error (msg ^ Position.here pos);
+    val props = Position.def_properties_of (#pos opt);
+  in Markup.properties props (Markup.entity Markup.system_optionN name) end;
+
+
+(* typ *)
+
 fun typ options name = #typ (check_name options name);
 
 
@@ -173,7 +183,7 @@
     SOME options => options
   | NONE => err_no_default ());
 
-fun default_position name = position (default ()) name;
+fun default_markup arg = markup (default ()) arg;
 fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -206,7 +206,7 @@
     val goal' = Thm.transfer thy' goal;
 
     fun limited_etac thm i =
-      Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
+      Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal'
       else
@@ -405,7 +405,7 @@
           else raw_matches;
 
         val len = length matches;
-        val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
+        val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
 
     val find =
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -17,49 +17,49 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_types}
+    @{system_option show_types}
     "show-types"
     "Include types in display of Isabelle terms";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_sorts}
+    @{system_option show_sorts}
     "show-sorts"
     "Include sorts in display of Isabelle types";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_consts}
+    @{system_option show_consts}
     "show-consts"
     "Show types of consts in Isabelle goal display";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option names_long}
+    @{system_option names_long}
     "long-names"
     "Show fully qualified names in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_brackets}
+    @{system_option show_brackets}
     "show-brackets"
     "Show full bracketing in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_main_goal}
+    @{system_option show_main_goal}
     "show-main-goal"
     "Show main goal in proof state display";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option eta_contract}
+    @{system_option eta_contract}
     "eta-contract"
     "Print terms eta-contracted";
 
@@ -69,7 +69,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
     NONE
-    @{option goals_limit}
+    @{system_option goals_limit}
     "goals-limit"
     "Setting for maximum number of subgoals to be printed";
 
@@ -85,7 +85,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
     NONE
-    @{option show_question_marks}
+    @{system_option show_question_marks}
     "show-question-marks"
     "Show leading question mark of variable name";
 
@@ -123,7 +123,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option ML_exception_trace}
+    @{system_option ML_exception_trace}
     "debugging"
     "Whether to enable exception trace for toplevel command execution";
 
@@ -140,14 +140,14 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     (SOME "true")
-    @{option quick_and_dirty}
+    @{system_option quick_and_dirty}
     "quick-and-dirty"
     "Take a few short cuts";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     NONE
-    @{option skip_proofs}
+    @{system_option skip_proofs}
     "skip-proofs"
     "Skip over proofs";
 
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Tools/quickcheck.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -95,7 +95,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_quickcheck}
+    @{system_option auto_quickcheck}
     "auto-quickcheck"
     "Run Quickcheck automatically";
 
@@ -584,7 +584,7 @@
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN);
 
-val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
+val _ = Try.tool_setup (quickcheckN, (20, @{system_option auto_quickcheck}, try_quickcheck));
 
 end;
 
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Tools/solve_direct.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -37,7 +37,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_solve_direct}
+    @{system_option auto_solve_direct}
     "auto-solve-direct"
     ("Run " ^ quote solve_directN ^ " automatically");
 
@@ -115,6 +115,6 @@
 
 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
 
-val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
+val _ = Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct));
 
 end;
diff -r 08982abdcdad -r 8d7d6f17c6a7 src/Tools/try.ML
--- a/src/Tools/try.ML	Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Tools/try.ML	Tue Apr 08 14:59:36 2014 +0200
@@ -32,7 +32,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     (SOME "4.0")
-    @{option auto_time_limit}
+    @{system_option auto_time_limit}
     "auto-try-time-limit"
     "Time limit for automatically tried tools (in seconds)"
 
@@ -103,7 +103,7 @@
 
 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   let
-    val auto_time_limit = Options.default_real @{option auto_time_limit}
+    val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   in
     if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
       TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
@@ -120,7 +120,7 @@
     (fn {command_name, ...} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME
-         {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
+         {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
           pri = ~ weight,
           persistent = true,
           strict = true,
@@ -128,7 +128,7 @@
             let
               val state = Toplevel.proof_of st
                 |> Proof.map_context (Context_Position.set_visible false)
-              val auto_time_limit = Options.default_real @{option auto_time_limit}
+              val auto_time_limit = Options.default_real @{system_option auto_time_limit}
             in
               if auto_time_limit > 0.0 then
                 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of