tuned;
authorwenzelm
Tue May 08 15:01:31 2007 +0200 (2007-05-08 ago)
changeset 228669de680b7d819
parent 22865 da52c2bd66ae
child 22867 165f733c50bd
tuned;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue May 08 15:01:30 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue May 08 15:01:31 2007 +0200
     1.3 @@ -389,15 +389,17 @@
     1.4      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     1.5      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
     1.6        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
     1.7 -      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
     1.8 -        Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
     1.9 +      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
    1.10 +        >> (fn ((x, y), z) => Toplevel.print o
    1.11 +            Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
    1.12  
    1.13  val interpretP =
    1.14    OuterSyntax.command "interpret"
    1.15      "prove and register interpretation of locale expression in proof context"
    1.16      (K.tag_proof K.prf_goal)
    1.17      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
    1.18 -      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
    1.19 +      >> (fn ((x, y), z) => Toplevel.print o
    1.20 +          Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
    1.21  
    1.22  
    1.23  (* classes *)
    1.24 @@ -427,7 +429,7 @@
    1.25        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.26             >> ClassPackage.instance_class_cmd
    1.27        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.28 -           >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
    1.29 +           >> ClassPackage.instance_sort_cmd
    1.30        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.31             >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
    1.32      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.33 @@ -435,6 +437,13 @@
    1.34  end;
    1.35  
    1.36  
    1.37 +(* code generation *)
    1.38 +
    1.39 +val code_datatypeP =
    1.40 +  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
    1.41 +    (Scan.repeat1 P.term >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd));
    1.42 +
    1.43 +
    1.44  
    1.45  (** proof commands **)
    1.46  
    1.47 @@ -697,21 +706,11 @@
    1.48  
    1.49  val undoP =
    1.50    OuterSyntax.improper_command "undo" "undo last command" K.control
    1.51 -    (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo));
    1.52 +    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo));
    1.53  
    1.54  val killP =
    1.55    OuterSyntax.improper_command "kill" "kill current history node" K.control
    1.56 -    (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
    1.57 -
    1.58 -
    1.59 -
    1.60 -(** code generation **)
    1.61 -
    1.62 -val code_datatypeP =
    1.63 -  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (
    1.64 -    Scan.repeat1 P.term
    1.65 -    >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)
    1.66 -  );
    1.67 +    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill));
    1.68  
    1.69  
    1.70  
    1.71 @@ -812,6 +811,8 @@
    1.72    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
    1.73      K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
    1.74  
    1.75 +local
    1.76 +
    1.77  val criterion =
    1.78    P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
    1.79    P.reserved "intro" >> K FindTheorems.Intro ||
    1.80 @@ -820,16 +821,20 @@
    1.81    P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
    1.82    P.term >> FindTheorems.Pattern;
    1.83  
    1.84 +val options =
    1.85 +  Scan.optional
    1.86 +    (P.$$$ "(" |--
    1.87 +      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
    1.88 +        --| P.$$$ ")")) (NONE, true);
    1.89 +in
    1.90 +
    1.91  val find_theoremsP =
    1.92 -  OuterSyntax.improper_command "find_theorems"
    1.93 -    "print theorems meeting specified criteria" K.diag
    1.94 -    (Scan.optional (P.$$$ "(" |-- P.!!!
    1.95 -                        (Scan.option P.nat --
    1.96 -                         Scan.optional (P.reserved "with_dups" >> K false) true
    1.97 -                         --| P.$$$ ")")) (NONE, true) --
    1.98 -     Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.99 +  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
   1.100 +    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   1.101        >> (Toplevel.no_timing oo IsarCmd.find_theorems));
   1.102  
   1.103 +end;
   1.104 +
   1.105  val print_bindsP =
   1.106    OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   1.107      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   1.108 @@ -852,7 +857,8 @@
   1.109  
   1.110  val print_prfsP =
   1.111    OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   1.112 -    (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   1.113 +    (opt_modes -- Scan.option SpecParse.xthms1
   1.114 +      >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   1.115  
   1.116  val print_full_prfsP =
   1.117    OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   1.118 @@ -970,8 +976,8 @@
   1.119  
   1.120  (** the Pure outer syntax **)
   1.121  
   1.122 -(*keep keywords consistent with the parsers, including those in
   1.123 -  outer_parse.ML, otherwise be prepared for unexpected errors*)
   1.124 +(*keep keywords consistent with the parsers, otherwise be prepared for
   1.125 +  unexpected errors*)
   1.126  
   1.127  val _ = OuterSyntax.add_keywords
   1.128   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   1.129 @@ -999,7 +1005,7 @@
   1.130    simproc_setupP, parse_ast_translationP, parse_translationP,
   1.131    print_translationP, typed_print_translationP,
   1.132    print_ast_translationP, token_translationP, oracleP, contextP,
   1.133 -  localeP, classP, instanceP,
   1.134 +  localeP, classP, instanceP, code_datatypeP,
   1.135    (*proof commands*)
   1.136    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   1.137    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
   1.138 @@ -1009,16 +1015,14 @@
   1.139    apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   1.140    cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   1.141    interpretP,
   1.142 -  (*code generation*)
   1.143 -  code_datatypeP,
   1.144    (*diagnostic commands*)
   1.145 -  pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   1.146 -  print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
   1.147 -  print_theoremsP, print_localesP, print_localeP,
   1.148 +  pretty_setmarginP, helpP, print_classesP, print_commandsP,
   1.149 +  print_contextP, print_theoryP, print_syntaxP, print_abbrevsP,
   1.150 +  print_factsP, print_theoremsP, print_localesP, print_localeP,
   1.151    print_registrationsP, print_attributesP, print_simpsetP,
   1.152    print_rulesP, print_induct_rulesP, print_trans_rulesP,
   1.153 -  print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
   1.154 -  find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   1.155 +  print_methodsP, print_antiquotationsP, thy_depsP, class_depsP,
   1.156 +  thm_depsP, find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   1.157    print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   1.158    print_termP, print_typeP, print_codesetupP,
   1.159    (*system commands*)