# HG changeset patch
# User haftmann
# Date 1420789019 -3600
# Node ID 468bd3aedfa128b4b0b459e9798ced1e6103bf03
# Parent  8ccecf1415b03a7e8ffed95bdf1853a7f6878c27
modernized and more uniform style

diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/HOL/Library/code_test.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -571,16 +571,15 @@
     "compile test cases to target languages, execute them and report results"
       (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
 
-val _ = Context.>> (Context.map_theory (
-  fold add_driver
-    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
-     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
-     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
-     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
-     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
-     (scalaN, (evaluate_in_scala, Code_Scala.target))]
-    #> fold (fn target => Value.add_evaluator (target, eval_term target))
-      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
-    ))
+val _ = Theory.setup (fold add_driver
+  [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
+   (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
+   (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
+   (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
+   (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
+   (scalaN, (evaluate_in_scala, Code_Scala.target))]
+  #> fold (fn target => Value.add_evaluator (target, eval_term target))
+    [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
+
 end
 
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -134,11 +134,11 @@
 
 (* setup *)
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Code.datatype_interpretation ensure_term_of
   #> Code.abstype_interpretation ensure_term_of
   #> Code.datatype_interpretation ensure_term_of_code
-  #> Code.abstype_interpretation ensure_abs_term_of_code));
+  #> Code.abstype_interpretation ensure_abs_term_of_code);
 
 
 (** termifying syntax **)
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/HOL/Tools/value.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -74,7 +74,7 @@
     (opt_evaluator -- opt_modes -- Parse.term
       >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
   (Thy_Output.antiquotation @{binding value}
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
@@ -82,7 +82,6 @@
         [style (value_maybe_select some_name context t)]))
   #> add_evaluator ("simp", Code_Simp.dynamic_value)
   #> add_evaluator ("nbe", Nbe.dynamic_value)
-  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict))
-);
+  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
 
 end;
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code/code_haskell.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -9,7 +9,6 @@
   val language_params: string
   val target: string
   val print_numeral: string -> int -> string
-  val setup: theory -> theory
 end;
 
 structure Code_Haskell : CODE_HASKELL =
@@ -493,13 +492,8 @@
 
 (** Isar setup **)
 
-val _ =
-  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
-    (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
-      Toplevel.theory (add_monad target raw_bind)));
-
-val setup =
-  Code_Target.add_language
+val _ = Theory.setup
+  (Code_Target.add_language
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "ISABELLE_GHC", make_destination = I,
         make_command = fn module_name =>
@@ -519,6 +513,11 @@
     ]
   #> fold (Code_Target.add_reserved target) prelude_import_unqualified
   #> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr
-  #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr;
+  #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr);
+
+val _ =
+  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
+    (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
+      Toplevel.theory (add_monad target raw_bind)));
 
 end; (*struct*)
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code/code_ml.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -8,7 +8,6 @@
 sig
   val target_SML: string
   val target_OCaml: string
-  val setup: theory -> theory
 end;
 
 structure Code_ML : CODE_ML =
@@ -860,8 +859,8 @@
     print_typ (INFX (1, R)) ty2
   );
 
-val setup =
-  Code_Target.add_language
+val _ = Theory.setup
+  (Code_Target.add_language
     (target_SML, { serializer = serializer_sml, literals = literals_sml,
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
@@ -887,6 +886,6 @@
       "sig", "struct", "then", "to", "true", "try", "type", "val",
       "virtual", "when", "while", "with"
     ]
-  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
+  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
 
 end; (*struct*)
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -280,8 +280,8 @@
   type T = string list option;
   val empty = SOME [];
   val extend = I;
-  fun merge (NONE, d2) = NONE
-    | merge (d1, NONE) = NONE
+  fun merge (NONE, _) = NONE
+    | merge (_, NONE) = NONE
     | merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2));
 );
 
@@ -567,21 +567,26 @@
 
 (** setup **)
 
-val _ =
+val _ = Theory.setup (
   let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
     fun add_del_attribute_parser process =
       Attrib.add_del (mk_attribute (process Simplifier.add_simp))
         (mk_attribute (process Simplifier.del_simp));
   in
-    Context.>> (Context.map_theory
-      (Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
-        "preprocessing equations for code generator"
-      #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
-        "postprocessing equations for code generator"
-      #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
-        "post- and preprocessing equations for code generator"))
-  end;
+    Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
+      "preprocessing equations for code generator"
+    #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
+      "postprocessing equations for code generator"
+    #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
+      "post- and preprocessing equations for code generator"
+    #> Attrib.setup @{binding code_preproc_trace}
+      ((Scan.lift (Args.$$$ "off" >> K trace_none)
+      || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
+         >> trace_only_ext
+      || Scan.succeed trace_all)
+      >> (Thm.declaration_attribute o K)) "tracing of the code generator preprocessor"
+  end);
 
 val _ =
   Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -8,7 +8,6 @@
 sig
   val target: string
   val case_insensitive: bool Config.T;
-  val setup: theory -> theory
 end;
 
 structure Code_Scala : CODE_SCALA =
@@ -423,8 +422,8 @@
 
 (** Isar setup **)
 
-val setup =
-  Code_Target.add_language
+val _ = Theory.setup
+  (Code_Target.add_language
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "SCALA_HOME",
         make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
@@ -446,6 +445,6 @@
     ]
   #> fold (Code_Target.add_reserved target) [
       "apply", "sys", "scala", "BigInt", "Nil", "List"
-    ];
+    ]);
 
 end; (*struct*)
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code/code_simp.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -14,7 +14,6 @@
     -> Proof.context -> conv
   val static_tac: { ctxt: Proof.context, simpset: simpset option, consts: string list }
     -> Proof.context -> int -> tactic
-  val setup: theory -> theory
   val trace: bool Config.T
 end;
 
@@ -86,10 +85,10 @@
 fun dynamic_value ctxt =
   snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of (Proof_Context.theory_of ctxt);
 
-val setup =
-  Method.setup @{binding code_simp}
+val _ = Theory.setup 
+  (Method.setup @{binding code_simp}
     (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
-    "simplification with code equations";
+    "simplification with code equations");
 
 
 (* evaluation with static code context *)
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code/code_target.ML	Fri Jan 09 08:36:59 2015 +0100
@@ -55,8 +55,6 @@
   val add_reserved: string -> string -> theory -> theory
 
   val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
-
-  val setup: theory -> theory
 end;
 
 structure Code_Target : CODE_TARGET =
@@ -492,15 +490,15 @@
 
 in
 
-val antiq_setup =
-  Thy_Output.antiquotation @{binding code_stmts}
+val _ = Theory.setup
+  (Thy_Output.antiquotation @{binding code_stmts}
     (parse_const_terms --
       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
     (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
         present_code ctxt (mk_cs ctxt)
           (maps (fn f => f ctxt) mk_stmtss)
-          target_name some_width "Example" []);
+          target_name some_width "Example" []));
 
 end;
 
@@ -673,9 +671,4 @@
     | NONE => error ("Bad directive " ^ quote cmd_expr)
   end;
 
-
-(** theory setup **)
-
-val setup = antiq_setup;
-
 end; (*struct*)
diff -r 8ccecf1415b0 -r 468bd3aedfa1 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Jan 08 18:23:29 2015 +0100
+++ b/src/Tools/Code_Generator.thy	Fri Jan 09 08:36:59 2015 +0100
@@ -16,15 +16,6 @@
 
 ML_file "~~/src/Tools/cache_io.ML"
 ML_file "~~/src/Tools/Code/code_preproc.ML"
-
-attribute_setup code_preproc_trace = {*
-  (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
-  || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
-       >> Code_Preproc.trace_only_ext
-  || Scan.succeed Code_Preproc.trace_all)
-  >> (Thm.declaration_attribute o K)
-*} "tracing of the code generator preprocessor"
-
 ML_file "~~/src/Tools/Code/code_symbol.ML"
 ML_file "~~/src/Tools/Code/code_thingol.ML"
 ML_file "~~/src/Tools/Code/code_simp.ML"
@@ -35,14 +26,6 @@
 ML_file "~~/src/Tools/Code/code_haskell.ML"
 ML_file "~~/src/Tools/Code/code_scala.ML"
 
-setup {*
-  Code_Simp.setup
-  #> Code_Target.setup
-  #> Code_ML.setup
-  #> Code_Haskell.setup
-  #> Code_Scala.setup
-*}
-
 code_datatype "TYPE('a\<Colon>{})"
 
 definition holds :: "prop" where