# HG changeset patch
# User wenzelm
# Date 1178629291 -7200
# Node ID 9de680b7d8194a79408abc261c81e2f097075898
# Parent  da52c2bd66ae26bd5b83a22f1dafc687099b2225
tuned;

diff -r da52c2bd66ae -r 9de680b7d819 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue May 08 15:01:30 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue May 08 15:01:31 2007 +0200
@@ -389,15 +389,17 @@
     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
-      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
-        Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
+      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
+        >> (fn ((x, y), z) => Toplevel.print o
+            Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
 
 val interpretP =
   OuterSyntax.command "interpret"
     "prove and register interpretation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
-      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
+      >> (fn ((x, y), z) => Toplevel.print o
+          Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
 
 
 (* classes *)
@@ -427,7 +429,7 @@
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
            >> ClassPackage.instance_class_cmd
       || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
-           >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
+           >> ClassPackage.instance_sort_cmd
       || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
            >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
@@ -435,6 +437,13 @@
 end;
 
 
+(* code generation *)
+
+val code_datatypeP =
+  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
+    (Scan.repeat1 P.term >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd));
+
+
 
 (** proof commands **)
 
@@ -697,21 +706,11 @@
 
 val undoP =
   OuterSyntax.improper_command "undo" "undo last command" K.control
-    (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo));
 
 val killP =
   OuterSyntax.improper_command "kill" "kill current history node" K.control
-    (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
-
-
-
-(** code generation **)
-
-val code_datatypeP =
-  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (
-    Scan.repeat1 P.term
-    >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)
-  );
+    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill));
 
 
 
@@ -812,6 +811,8 @@
   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
 
+local
+
 val criterion =
   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
   P.reserved "intro" >> K FindTheorems.Intro ||
@@ -820,16 +821,20 @@
   P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
   P.term >> FindTheorems.Pattern;
 
+val options =
+  Scan.optional
+    (P.$$$ "(" |--
+      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
+        --| P.$$$ ")")) (NONE, true);
+in
+
 val find_theoremsP =
-  OuterSyntax.improper_command "find_theorems"
-    "print theorems meeting specified criteria" K.diag
-    (Scan.optional (P.$$$ "(" |-- P.!!!
-                        (Scan.option P.nat --
-                         Scan.optional (P.reserved "with_dups" >> K false) true
-                         --| P.$$$ ")")) (NONE, true) --
-     Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
+    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
 
+end;
+
 val print_bindsP =
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
@@ -852,7 +857,8 @@
 
 val print_prfsP =
   OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
-    (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
+    (opt_modes -- Scan.option SpecParse.xthms1
+      >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
 
 val print_full_prfsP =
   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
@@ -970,8 +976,8 @@
 
 (** the Pure outer syntax **)
 
-(*keep keywords consistent with the parsers, including those in
-  outer_parse.ML, otherwise be prepared for unexpected errors*)
+(*keep keywords consistent with the parsers, otherwise be prepared for
+  unexpected errors*)
 
 val _ = OuterSyntax.add_keywords
  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
@@ -999,7 +1005,7 @@
   simproc_setupP, parse_ast_translationP, parse_translationP,
   print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP, contextP,
-  localeP, classP, instanceP,
+  localeP, classP, instanceP, code_datatypeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
@@ -1009,16 +1015,14 @@
   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   interpretP,
-  (*code generation*)
-  code_datatypeP,
   (*diagnostic commands*)
-  pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
-  print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
-  print_theoremsP, print_localesP, print_localeP,
+  pretty_setmarginP, helpP, print_classesP, print_commandsP,
+  print_contextP, print_theoryP, print_syntaxP, print_abbrevsP,
+  print_factsP, print_theoremsP, print_localesP, print_localeP,
   print_registrationsP, print_attributesP, print_simpsetP,
   print_rulesP, print_induct_rulesP, print_trans_rulesP,
-  print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
-  find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
+  print_methodsP, print_antiquotationsP, thy_depsP, class_depsP,
+  thm_depsP, find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   print_termP, print_typeP, print_codesetupP,
   (*system commands*)