src/Pure/Isar/attrib.ML
author wenzelm
Sat Mar 08 21:08:10 2014 +0100 (2014-03-08)
changeset 55997 9dc5ce83202c
parent 55914 c5b752d549e3
child 55998 f5f9fad3321c
permissions -rw-r--r--
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
tuned signature;
wenzelm@5823
     1
(*  Title:      Pure/Isar/attrib.ML
wenzelm@5823
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5823
     3
wenzelm@18734
     4
Symbolic representation of attributes -- with name and syntax.
wenzelm@5823
     5
*)
wenzelm@5823
     6
wenzelm@5823
     7
signature ATTRIB =
wenzelm@5823
     8
sig
wenzelm@27729
     9
  type src = Args.src
haftmann@29581
    10
  type binding = binding * src list
haftmann@28965
    11
  val empty_binding: binding
wenzelm@45584
    12
  val is_empty_binding: binding -> bool
wenzelm@55997
    13
  val print_attributes: Proof.context -> unit
wenzelm@55997
    14
  val check_name_generic: Context.generic -> xstring * Position.T -> string
wenzelm@55997
    15
  val check_src_generic: Context.generic -> src -> src
wenzelm@55997
    16
  val check_name: Proof.context -> xstring * Position.T -> string
wenzelm@55997
    17
  val check_src: Proof.context -> src -> src
wenzelm@21031
    18
  val pretty_attribs: Proof.context -> src list -> Pretty.T list
wenzelm@47815
    19
  val attribute: Proof.context -> src -> attribute
wenzelm@47815
    20
  val attribute_global: theory -> src -> attribute
wenzelm@47815
    21
  val attribute_cmd: Proof.context -> src -> attribute
wenzelm@47815
    22
  val attribute_cmd_global: theory -> src -> attribute
wenzelm@45390
    23
  val map_specs: ('a list -> 'att list) ->
wenzelm@30759
    24
    (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
wenzelm@45390
    25
  val map_facts: ('a list -> 'att list) ->
wenzelm@17105
    26
    (('c * 'a list) * ('d * 'a list) list) list ->
wenzelm@18905
    27
    (('c * 'att list) * ('d * 'att list) list) list
wenzelm@45390
    28
  val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
wenzelm@30759
    29
    (('c * 'a list) * ('b * 'a list) list) list ->
wenzelm@30759
    30
    (('c * 'att list) * ('fact * 'att list) list) list
wenzelm@47249
    31
  val global_notes: string -> (binding * (thm list * src list) list) list ->
wenzelm@47249
    32
    theory -> (string * thm list) list * theory
wenzelm@47249
    33
  val local_notes: string -> (binding * (thm list * src list) list) list ->
wenzelm@47249
    34
    Proof.context -> (string * thm list) list * Proof.context
wenzelm@47249
    35
  val generic_notes: string -> (binding * (thm list * src list) list) list ->
wenzelm@47249
    36
    Context.generic -> (string * thm list) list * Context.generic
wenzelm@38330
    37
  val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
wenzelm@30525
    38
  val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
wenzelm@55828
    39
  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
wenzelm@55140
    40
  val internal: (morphism -> attribute) -> src
wenzelm@30525
    41
  val add_del: attribute -> attribute -> attribute context_parser
wenzelm@30513
    42
  val thm_sel: Facts.interval list parser
wenzelm@30513
    43
  val thm: thm context_parser
wenzelm@30513
    44
  val thms: thm list context_parser
wenzelm@30513
    45
  val multi_thm: thm list context_parser
wenzelm@45493
    46
  val partial_evaluation: Proof.context ->
wenzelm@45493
    47
    (binding * (thm list * Args.src list) list) list ->
wenzelm@45493
    48
    (binding * (thm list * Args.src list) list) list
wenzelm@52060
    49
  val print_options: Proof.context -> unit
wenzelm@42616
    50
  val config_bool: Binding.binding ->
wenzelm@42616
    51
    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
wenzelm@42616
    52
  val config_int: Binding.binding ->
wenzelm@42616
    53
    (Context.generic -> int) -> int Config.T * (theory -> theory)
wenzelm@42616
    54
  val config_real: Binding.binding ->
wenzelm@42616
    55
    (Context.generic -> real) -> real Config.T * (theory -> theory)
wenzelm@42616
    56
  val config_string: Binding.binding ->
wenzelm@42616
    57
    (Context.generic -> string) -> string Config.T * (theory -> theory)
wenzelm@42616
    58
  val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
wenzelm@42616
    59
  val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
wenzelm@52040
    60
  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
wenzelm@42616
    61
  val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
wenzelm@52040
    62
  val option_bool: string -> bool Config.T * (theory -> theory)
wenzelm@52040
    63
  val option_int: string -> int Config.T * (theory -> theory)
wenzelm@52040
    64
  val option_real: string -> real Config.T * (theory -> theory)
wenzelm@52040
    65
  val option_string: string -> string Config.T * (theory -> theory)
wenzelm@52040
    66
  val setup_option_bool: string -> bool Config.T
wenzelm@52040
    67
  val setup_option_int: string -> int Config.T
wenzelm@52040
    68
  val setup_option_real: string -> real Config.T
wenzelm@52040
    69
  val setup_option_string: string -> string Config.T
wenzelm@5823
    70
end;
wenzelm@5823
    71
wenzelm@5823
    72
structure Attrib: ATTRIB =
wenzelm@5823
    73
struct
wenzelm@5823
    74
wenzelm@28084
    75
(* source and bindings *)
wenzelm@28084
    76
wenzelm@15703
    77
type src = Args.src;
wenzelm@15703
    78
haftmann@29581
    79
type binding = binding * src list;
wenzelm@45584
    80
haftmann@28965
    81
val empty_binding: binding = (Binding.empty, []);
wenzelm@45584
    82
fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
wenzelm@28084
    83
wenzelm@28084
    84
wenzelm@27729
    85
wenzelm@18734
    86
(** named attributes **)
wenzelm@18636
    87
wenzelm@18734
    88
(* theory data *)
wenzelm@5823
    89
wenzelm@33522
    90
structure Attributes = Theory_Data
wenzelm@22846
    91
(
wenzelm@33095
    92
  type T = ((src -> attribute) * string) Name_Space.table;
wenzelm@33159
    93
  val empty : T = Name_Space.empty_table "attribute";
wenzelm@16458
    94
  val extend = I;
wenzelm@33522
    95
  fun merge data : T = Name_Space.merge_tables data;
wenzelm@22846
    96
);
wenzelm@5823
    97
wenzelm@55997
    98
val get_attributes = Attributes.get o Context.theory_of;
wenzelm@55997
    99
wenzelm@55997
   100
fun print_attributes ctxt =
wenzelm@22846
   101
  let
wenzelm@55997
   102
    val attribs = get_attributes (Context.Proof ctxt);
wenzelm@50301
   103
    fun prt_attr (name, (_, "")) = Pretty.mark_str name
wenzelm@42813
   104
      | prt_attr (name, (_, comment)) =
wenzelm@50301
   105
          Pretty.block
wenzelm@50301
   106
            (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
wenzelm@22846
   107
  in
wenzelm@42358
   108
    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
wenzelm@22846
   109
    |> Pretty.chunks |> Pretty.writeln
wenzelm@22846
   110
  end;
wenzelm@7611
   111
wenzelm@33092
   112
fun add_attribute name att comment thy = thy
wenzelm@47005
   113
  |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
wenzelm@31306
   114
wenzelm@5823
   115
wenzelm@55997
   116
(* check *)
wenzelm@15703
   117
wenzelm@55997
   118
fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
wenzelm@53044
   119
wenzelm@55997
   120
fun check_src_generic context src =
wenzelm@55997
   121
  let
wenzelm@55997
   122
    val ((xname, toks), pos) = Args.dest_src src;
wenzelm@55997
   123
    val name = check_name_generic context (xname, pos);
wenzelm@55997
   124
  in Args.src ((name, toks), pos) end;
wenzelm@15703
   125
wenzelm@55997
   126
val check_name = check_name_generic o Context.Proof;
wenzelm@55997
   127
val check_src = check_src_generic o Context.Proof;
wenzelm@21031
   128
wenzelm@21031
   129
wenzelm@21031
   130
(* pretty printing *)
wenzelm@21031
   131
wenzelm@55997
   132
fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
wenzelm@55997
   133
wenzelm@21031
   134
fun pretty_attribs _ [] = []
wenzelm@21031
   135
  | pretty_attribs ctxt srcs =
wenzelm@38329
   136
      [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
wenzelm@21031
   137
wenzelm@15703
   138
wenzelm@18734
   139
(* get attributes *)
wenzelm@5823
   140
wenzelm@47816
   141
fun attribute_generic context =
wenzelm@55997
   142
  let val (_, tab) = get_attributes context in
wenzelm@55997
   143
    fn src =>
wenzelm@16344
   144
      let val ((name, _), pos) = Args.dest_src src in
wenzelm@42380
   145
        (case Symtab.lookup tab name of
wenzelm@55997
   146
          NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
wenzelm@55997
   147
        | SOME (att, _) => att src)
wenzelm@55997
   148
      end
wenzelm@55997
   149
  end;
wenzelm@5823
   150
wenzelm@47816
   151
val attribute = attribute_generic o Context.Proof;
wenzelm@47816
   152
val attribute_global = attribute_generic o Context.Theory;
wenzelm@47815
   153
wenzelm@55997
   154
fun attribute_cmd ctxt = attribute ctxt o check_src ctxt;
wenzelm@55997
   155
fun attribute_cmd_global thy = attribute_global thy o check_src_generic (Context.Theory thy);
wenzelm@18636
   156
wenzelm@5823
   157
wenzelm@17105
   158
(* attributed declarations *)
wenzelm@17105
   159
wenzelm@45390
   160
fun map_specs f = map (apfst (apsnd f));
wenzelm@30759
   161
wenzelm@45390
   162
fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f)));
wenzelm@30759
   163
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
wenzelm@17105
   164
wenzelm@17105
   165
wenzelm@38330
   166
(* fact expressions *)
wenzelm@38330
   167
wenzelm@47249
   168
fun global_notes kind facts thy = thy |>
wenzelm@47815
   169
  Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
wenzelm@47249
   170
wenzelm@47249
   171
fun local_notes kind facts ctxt = ctxt |>
wenzelm@47815
   172
  Proof_Context.note_thmss kind (map_facts (map (attribute ctxt)) facts);
wenzelm@47249
   173
wenzelm@47249
   174
fun generic_notes kind facts context = context |>
wenzelm@47249
   175
  Context.mapping_result (global_notes kind facts) (local_notes kind facts);
wenzelm@47249
   176
wenzelm@38330
   177
fun eval_thms ctxt srcs = ctxt
wenzelm@42360
   178
  |> Proof_Context.note_thmss ""
wenzelm@47815
   179
    (map_facts_refs (map (attribute_cmd ctxt)) (Proof_Context.get_fact ctxt)
wenzelm@38330
   180
      [((Binding.empty, []), srcs)])
wenzelm@38330
   181
  |> fst |> maps snd;
wenzelm@38330
   182
wenzelm@38330
   183
wenzelm@30525
   184
(* attribute setup *)
wenzelm@30525
   185
wenzelm@31306
   186
fun syntax scan = Args.syntax "attribute" scan;
wenzelm@30525
   187
wenzelm@31306
   188
fun setup name scan =
wenzelm@31306
   189
  add_attribute name
wenzelm@31306
   190
    (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
wenzelm@5879
   191
wenzelm@55828
   192
fun attribute_setup name source cmt =
wenzelm@55828
   193
  Context.theory_map (ML_Context.expression (#pos source)
wenzelm@30525
   194
    "val (name, scan, comment): binding * attribute context_parser * string"
wenzelm@30525
   195
    "Context.map_theory (Attrib.setup name scan comment)"
wenzelm@37198
   196
    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
wenzelm@55828
   197
      ML_Lex.read_source source @
wenzelm@37198
   198
      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
wenzelm@30525
   199
wenzelm@30525
   200
wenzelm@55140
   201
(* internal attribute *)
wenzelm@55140
   202
wenzelm@55140
   203
fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
wenzelm@55140
   204
wenzelm@55140
   205
val _ = Theory.setup
wenzelm@55140
   206
 (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
wenzelm@55140
   207
    "internal attribute");
wenzelm@55140
   208
wenzelm@55140
   209
wenzelm@31305
   210
(* add/del syntax *)
wenzelm@5823
   211
wenzelm@31305
   212
fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
wenzelm@5879
   213
wenzelm@5879
   214
wenzelm@25983
   215
wenzelm@25983
   216
(** parsing attributed theorems **)
wenzelm@5879
   217
wenzelm@36950
   218
val thm_sel = Parse.$$$ "(" |-- Parse.list1
wenzelm@36950
   219
 (Parse.nat --| Parse.minus -- Parse.nat >> Facts.FromTo ||
wenzelm@36950
   220
  Parse.nat --| Parse.minus >> Facts.From ||
wenzelm@36950
   221
  Parse.nat >> Facts.Single) --| Parse.$$$ ")";
wenzelm@27812
   222
wenzelm@18636
   223
local
wenzelm@18636
   224
wenzelm@21698
   225
val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
wenzelm@21698
   226
wenzelm@26336
   227
fun gen_thm pick = Scan.depend (fn context =>
wenzelm@26336
   228
  let
wenzelm@42360
   229
    val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
wenzelm@26361
   230
    val get_fact = get o Facts.Fact;
wenzelm@27820
   231
    fun get_named pos name = get (Facts.Named ((name, pos), NONE));
wenzelm@26336
   232
  in
wenzelm@55997
   233
    Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
wenzelm@24008
   234
      let
wenzelm@47815
   235
        val atts = map (attribute_generic context) srcs;
wenzelm@46775
   236
        val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
wenzelm@55740
   237
      in (context', pick ("", Position.none) [th']) end)
wenzelm@26336
   238
    ||
wenzelm@26336
   239
    (Scan.ahead Args.alt_name -- Args.named_fact get_fact
wenzelm@27820
   240
      >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
wenzelm@36950
   241
     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
wenzelm@27820
   242
      Args.named_fact (get_named pos) -- Scan.option thm_sel
wenzelm@27820
   243
        >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
wenzelm@55997
   244
    -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
wenzelm@26336
   245
      let
wenzelm@26336
   246
        val ths = Facts.select thmref fact;
wenzelm@47815
   247
        val atts = map (attribute_generic context) srcs;
wenzelm@46775
   248
        val (ths', context') =
wenzelm@46775
   249
          fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
wenzelm@55740
   250
      in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
wenzelm@26336
   251
  end);
berghofe@15456
   252
wenzelm@18636
   253
in
wenzelm@18636
   254
wenzelm@26336
   255
val thm = gen_thm Facts.the_single;
wenzelm@18998
   256
val multi_thm = gen_thm (K I);
wenzelm@19482
   257
val thms = Scan.repeat multi_thm >> flat;
wenzelm@18636
   258
wenzelm@18636
   259
end;
wenzelm@18636
   260
wenzelm@5823
   261
wenzelm@5879
   262
wenzelm@45586
   263
(** partial evaluation -- observing rule/declaration/mixed attributes **)
wenzelm@45493
   264
wenzelm@45493
   265
local
wenzelm@45526
   266
wenzelm@45493
   267
fun apply_att src (context, th) =
wenzelm@45526
   268
  let
wenzelm@55914
   269
    val src1 = Args.init_assignable src;
wenzelm@47815
   270
    val result = attribute_generic context src1 (context, th);
wenzelm@45526
   271
    val src2 = Args.closure src1;
wenzelm@45526
   272
  in (src2, result) end;
wenzelm@45493
   273
wenzelm@45527
   274
fun err msg src =
wenzelm@45527
   275
  let val ((name, _), pos) = Args.dest_src src
wenzelm@48992
   276
  in error (msg ^ " " ^ quote name ^ Position.here pos) end;
wenzelm@45527
   277
wenzelm@45527
   278
fun eval src ((th, dyn), (decls, context)) =
wenzelm@45527
   279
  (case (apply_att src (context, th), dyn) of
wenzelm@45527
   280
    ((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context))
wenzelm@45527
   281
  | ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src
wenzelm@45527
   282
  | ((src', (SOME context', NONE)), NONE) =>
wenzelm@45493
   283
      let
wenzelm@45493
   284
        val decls' =
wenzelm@45493
   285
          (case decls of
wenzelm@45526
   286
            [] => [(th, [src'])]
wenzelm@45493
   287
          | (th2, srcs2) :: rest =>
wenzelm@52683
   288
              if Thm.eq_thm_strict (th, th2)
wenzelm@45526
   289
              then ((th2, src' :: srcs2) :: rest)
wenzelm@45526
   290
              else (th, [src']) :: (th2, srcs2) :: rest);
wenzelm@45527
   291
      in ((th, NONE), (decls', context')) end
wenzelm@45527
   292
  | ((src', (opt_context', opt_th')), _) =>
wenzelm@45527
   293
      let
wenzelm@45527
   294
        val context' = the_default context opt_context';
wenzelm@45527
   295
        val th' = the_default th opt_th';
wenzelm@45527
   296
        val dyn' =
wenzelm@45527
   297
          (case dyn of
wenzelm@45527
   298
            NONE => SOME (th, [src'])
wenzelm@45527
   299
          | SOME (dyn_th, srcs) => SOME (dyn_th, src' :: srcs));
wenzelm@45527
   300
      in ((th', dyn'), (decls, context')) end);
wenzelm@45493
   301
wenzelm@45493
   302
in
wenzelm@45493
   303
wenzelm@45493
   304
fun partial_evaluation ctxt facts =
wenzelm@45586
   305
  (facts, Context.Proof (Context_Position.set_visible false ctxt)) |->
wenzelm@45586
   306
    fold_map (fn ((b, more_atts), fact) => fn context =>
wenzelm@45586
   307
      let
wenzelm@45586
   308
        val (fact', (decls, context')) =
wenzelm@45586
   309
          (fact, ([], context)) |-> fold_map (fn (ths, atts) => fn res1 =>
wenzelm@45586
   310
            (ths, res1) |-> fold_map (fn th => fn res2 =>
wenzelm@45586
   311
              let
wenzelm@45586
   312
                val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
wenzelm@45586
   313
                val th_atts' =
wenzelm@45586
   314
                  (case dyn' of
wenzelm@45586
   315
                    NONE => (th', [])
wenzelm@45586
   316
                  | SOME (dyn_th', atts') => (dyn_th', rev atts'));
wenzelm@45586
   317
              in (th_atts', res3) end))
wenzelm@45586
   318
          |>> flat;
wenzelm@45586
   319
        val decls' = rev (map (apsnd rev) decls);
wenzelm@45586
   320
        val facts' =
wenzelm@52683
   321
          if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
wenzelm@45586
   322
            [((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
wenzelm@45619
   323
          else if null decls' then [((b, []), fact')]
wenzelm@45586
   324
          else [(empty_binding, decls'), ((b, []), fact')];
wenzelm@45586
   325
      in (facts', context') end)
wenzelm@46906
   326
  |> fst |> flat |> map (apsnd (map (apfst single)))
wenzelm@46906
   327
  |> filter_out (fn (b, fact) => is_empty_binding b andalso forall (null o #2) fact);
wenzelm@45493
   328
wenzelm@45493
   329
end;
wenzelm@45493
   330
wenzelm@45493
   331
wenzelm@45493
   332
wenzelm@24110
   333
(** configuration options **)
wenzelm@24110
   334
wenzelm@24110
   335
(* naming *)
wenzelm@24110
   336
wenzelm@33522
   337
structure Configs = Theory_Data
wenzelm@24713
   338
(
wenzelm@39163
   339
  type T = Config.raw Symtab.table;
wenzelm@24110
   340
  val empty = Symtab.empty;
wenzelm@24110
   341
  val extend = I;
wenzelm@33522
   342
  fun merge data = Symtab.merge (K true) data;
wenzelm@24713
   343
);
wenzelm@5823
   344
wenzelm@52060
   345
fun print_options ctxt =
wenzelm@24110
   346
  let
wenzelm@24110
   347
    fun prt (name, config) =
wenzelm@24110
   348
      let val value = Config.get ctxt config in
wenzelm@50301
   349
        Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
wenzelm@50301
   350
          Pretty.brk 1, Pretty.str (Config.print_value value)]
wenzelm@24110
   351
      end;
wenzelm@55997
   352
    val space = #1 (get_attributes (Context.Proof ctxt));
wenzelm@55997
   353
    val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
wenzelm@24110
   354
  in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
wenzelm@24110
   355
wenzelm@24110
   356
wenzelm@24110
   357
(* concrete syntax *)
wenzelm@23988
   358
wenzelm@24003
   359
local
wenzelm@24003
   360
wenzelm@36950
   361
val equals = Parse.$$$ "=";
wenzelm@24003
   362
wenzelm@24110
   363
fun scan_value (Config.Bool _) =
wenzelm@24110
   364
      equals -- Args.$$$ "false" >> K (Config.Bool false) ||
wenzelm@24110
   365
      equals -- Args.$$$ "true" >> K (Config.Bool true) ||
wenzelm@24110
   366
      Scan.succeed (Config.Bool true)
wenzelm@36950
   367
  | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
wenzelm@40291
   368
  | scan_value (Config.Real _) = equals |-- Parse.real >> Config.Real
wenzelm@24110
   369
  | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
wenzelm@24003
   370
wenzelm@24110
   371
fun scan_config thy config =
wenzelm@36787
   372
  let val config_type = Config.get_global thy config
wenzelm@24110
   373
  in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
wenzelm@24003
   374
wenzelm@42616
   375
fun register binding config thy =
wenzelm@42616
   376
  let val name = Sign.full_name thy binding in
wenzelm@24126
   377
    thy
wenzelm@42616
   378
    |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
wenzelm@24126
   379
    |> Configs.map (Symtab.update (name, config))
wenzelm@24126
   380
  end;
wenzelm@24110
   381
wenzelm@42808
   382
fun declare make coerce binding default =
wenzelm@24110
   383
  let
wenzelm@42616
   384
    val name = Binding.name_of binding;
wenzelm@52039
   385
    val config_value = Config.declare name (make o default);
wenzelm@24110
   386
    val config = coerce config_value;
wenzelm@42616
   387
  in (config, register binding config_value) end;
wenzelm@42616
   388
wenzelm@42616
   389
in
wenzelm@42616
   390
wenzelm@52040
   391
fun register_config config = register (Binding.name (Config.name_of config)) config;
wenzelm@52040
   392
wenzelm@42808
   393
val config_bool = declare Config.Bool Config.bool;
wenzelm@42808
   394
val config_int = declare Config.Int Config.int;
wenzelm@42808
   395
val config_real = declare Config.Real Config.real;
wenzelm@42808
   396
val config_string = declare Config.String Config.string;
wenzelm@42616
   397
wenzelm@42616
   398
end;
wenzelm@24110
   399
wenzelm@42616
   400
wenzelm@42616
   401
(* implicit setup *)
wenzelm@42616
   402
wenzelm@42616
   403
local
wenzelm@24110
   404
wenzelm@42616
   405
fun setup_config declare_config binding default =
wenzelm@42616
   406
  let
wenzelm@42616
   407
    val (config, setup) = declare_config binding default;
wenzelm@53171
   408
    val _ = Theory.setup setup;
wenzelm@42616
   409
  in config end;
wenzelm@42616
   410
wenzelm@42616
   411
in
wenzelm@42616
   412
wenzelm@42616
   413
val setup_config_bool = setup_config config_bool;
wenzelm@42616
   414
val setup_config_int = setup_config config_int;
wenzelm@42616
   415
val setup_config_string = setup_config config_string;
wenzelm@42616
   416
val setup_config_real = setup_config config_real;
wenzelm@24003
   417
wenzelm@24003
   418
end;
wenzelm@23988
   419
wenzelm@23988
   420
wenzelm@52040
   421
(* system options *)
wenzelm@52040
   422
wenzelm@52040
   423
local
wenzelm@52040
   424
wenzelm@52040
   425
fun declare_option coerce name =
wenzelm@52040
   426
  let
wenzelm@52040
   427
    val config = Config.declare_option name;
wenzelm@52040
   428
  in (coerce config, register_config config) end;
wenzelm@52040
   429
wenzelm@52040
   430
fun setup_option coerce name =
wenzelm@52040
   431
  let
wenzelm@52040
   432
    val config = Config.declare_option name;
wenzelm@53171
   433
    val _ = Theory.setup (register_config config);
wenzelm@52040
   434
  in coerce config end;
wenzelm@52040
   435
wenzelm@52040
   436
in
wenzelm@52040
   437
wenzelm@52040
   438
val option_bool = declare_option Config.bool;
wenzelm@52040
   439
val option_int = declare_option Config.int;
wenzelm@52040
   440
val option_real = declare_option Config.real;
wenzelm@52040
   441
val option_string = declare_option Config.string;
wenzelm@52040
   442
wenzelm@52040
   443
val setup_option_bool = setup_option Config.bool;
wenzelm@52040
   444
val setup_option_int = setup_option Config.int;
wenzelm@52040
   445
val setup_option_real = setup_option Config.real;
wenzelm@52040
   446
val setup_option_string = setup_option Config.string;
wenzelm@52040
   447
wenzelm@52040
   448
end;
wenzelm@52040
   449
wenzelm@52040
   450
wenzelm@18636
   451
(* theory setup *)
wenzelm@5823
   452
wenzelm@53171
   453
val _ = Theory.setup
wenzelm@52059
   454
 (register_config quick_and_dirty_raw #>
wenzelm@52059
   455
  register_config Ast.trace_raw #>
wenzelm@43347
   456
  register_config Ast.stats_raw #>
wenzelm@42289
   457
  register_config Printer.show_brackets_raw #>
wenzelm@42289
   458
  register_config Printer.show_sorts_raw #>
wenzelm@42289
   459
  register_config Printer.show_types_raw #>
wenzelm@49657
   460
  register_config Printer.show_markup_raw #>
wenzelm@42289
   461
  register_config Printer.show_structs_raw #>
wenzelm@42289
   462
  register_config Printer.show_question_marks_raw #>
wenzelm@46512
   463
  register_config Syntax.ambiguity_warning_raw #>
wenzelm@46506
   464
  register_config Syntax.ambiguity_limit_raw #>
wenzelm@42284
   465
  register_config Syntax_Trans.eta_contract_raw #>
wenzelm@42669
   466
  register_config Name_Space.names_long_raw #>
wenzelm@42669
   467
  register_config Name_Space.names_short_raw #>
wenzelm@42669
   468
  register_config Name_Space.names_unique_raw #>
wenzelm@41375
   469
  register_config ML_Context.trace_raw #>
wenzelm@42360
   470
  register_config Proof_Context.show_abbrevs_raw #>
wenzelm@39163
   471
  register_config Goal_Display.goals_limit_raw #>
wenzelm@39163
   472
  register_config Goal_Display.show_main_goal_raw #>
wenzelm@39163
   473
  register_config Goal_Display.show_consts_raw #>
wenzelm@39166
   474
  register_config Display.show_hyps_raw #>
wenzelm@39166
   475
  register_config Display.show_tags_raw #>
wenzelm@52709
   476
  register_config Pattern.unify_trace_failure_raw #>
wenzelm@39163
   477
  register_config Unify.trace_bound_raw #>
wenzelm@39163
   478
  register_config Unify.search_bound_raw #>
wenzelm@39163
   479
  register_config Unify.trace_simp_raw #>
wenzelm@39163
   480
  register_config Unify.trace_types_raw #>
wenzelm@41228
   481
  register_config Raw_Simplifier.simp_depth_limit_raw #>
wenzelm@41228
   482
  register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
wenzelm@41228
   483
  register_config Raw_Simplifier.simp_debug_raw #>
wenzelm@53171
   484
  register_config Raw_Simplifier.simp_trace_raw);
wenzelm@5823
   485
wenzelm@5823
   486
end;