# HG changeset patch
# User wenzelm
# Date 1236812374 -3600
# Node ID 00323c45ea83b00d027ae62d3293d7428e05d05e
# Parent  c999618d225e376e5f7cb11c4563da74d5ced972
added 'local_setup' command;
tuned;

diff -r c999618d225e -r 00323c45ea83 NEWS
--- a/NEWS	Wed Mar 11 20:54:03 2009 +0100
+++ b/NEWS	Wed Mar 11 23:59:34 2009 +0100
@@ -186,7 +186,7 @@
 stated. Any theorems that could solve the lemma directly are listed
 underneath the goal.
 
-* New command find_consts searches for constants based on type and
+* New command 'find_consts' searches for constants based on type and
 name patterns, e.g.
 
     find_consts "_ => bool"
@@ -198,8 +198,8 @@
 
     find_consts strict: "_ => bool" name: "Int" -"int => int"
 
-* Linear arithmetic now ignores all inequalities when fast_arith_neq_limit
-is exceeded, instead of giving up entirely.
+* New command 'local_setup' is similar to 'setup', but operates on a
+local theory context.
 
 
 *** Document preparation ***
@@ -537,6 +537,9 @@
 * ATP selection (E/Vampire/Spass) is now via Proof General's settings
 menu.
 
+* Linear arithmetic now ignores all inequalities when
+fast_arith_neq_limit is exceeded, instead of giving up entirely.
+
 
 *** HOL-Algebra ***
 
diff -r c999618d225e -r 00323c45ea83 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 11 20:54:03 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 11 23:59:34 2009 +0100
@@ -799,6 +799,7 @@
     @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   \begin{mldecls}
@@ -809,7 +810,7 @@
   \begin{rail}
     'use' name
     ;
-    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
+    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
     ;
   \end{rail}
 
@@ -817,7 +818,7 @@
 
   \item @{command "use"}~@{text "file"} reads and executes ML
   commands from @{text "file"}.  The current theory context is passed
-  down to the ML toplevel and may be modified, using @{ML [source=false]
+  down to the ML toplevel and may be modified, using @{ML
   "Context.>>"} or derived ML commands.  The file name is checked with
   the @{keyword_ref "uses"} dependency declaration given in the theory
   header (see also \secref{sec:begin-thy}).
@@ -845,9 +846,15 @@
   
   \item @{command "setup"}~@{text "text"} changes the current theory
   context by applying @{text "text"}, which refers to an ML expression
-  of type @{ML_type [source=false] "theory -> theory"}.  This enables
-  to initialize any object-logic specific tools and packages written
-  in ML, for example.
+  of type @{ML_type "theory -> theory"}.  This enables to initialize
+  any object-logic specific tools and packages written in ML, for
+  example.
+
+  \item @{command "local_setup"} is similar to @{command "setup"} for
+  a local theory context, and an ML expression of type @{ML_type
+  "local_theory -> local_theory"}.  This allows to
+  invoke local theory specification packages without going through
+  concrete outer syntax, for example.
 
   \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
   theorems produced in ML both in the theory context and the ML
diff -r c999618d225e -r 00323c45ea83 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 11 20:54:03 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 11 23:59:34 2009 +0100
@@ -6,7 +6,8 @@
 
 signature ISAR_CMD =
 sig
-  val generic_setup: string * Position.T -> theory -> theory
+  val global_setup: string * Position.T -> theory -> theory
+  val local_setup: string * Position.T -> Proof.context -> Proof.context
   val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
   val parse_translation: bool * (string * Position.T) -> theory -> theory
   val print_translation: bool * (string * Position.T) -> theory -> theory
@@ -86,12 +87,16 @@
 
 (** theory declarations **)
 
-(* generic_setup *)
+(* generic setup *)
 
-fun generic_setup (txt, pos) =
+fun global_setup (txt, pos) =
   ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup" txt
   |> Context.theory_map;
 
+fun local_setup (txt, pos) =
+  ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup" txt
+  |> Context.proof_map;
+
 
 (* translation functions *)
 
diff -r c999618d225e -r 00323c45ea83 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 11 20:54:03 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 11 23:59:34 2009 +0100
@@ -318,8 +318,12 @@
     (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
 
 val _ =
-  OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
-    (P.ML_source >> (Toplevel.theory o IsarCmd.generic_setup));
+  OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl)
+    (P.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
+
+val _ =
+  OuterSyntax.local_theory "local_setup" "ML local theory setup" (K.tag_ml K.thy_decl)
+    (P.ML_source >> IsarCmd.local_setup);
 
 val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)