renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
1.1 --- a/NEWS Sat May 15 23:32:15 2010 +0200
1.2 +++ b/NEWS Sat May 15 23:40:00 2010 +0200
1.3 @@ -505,6 +505,7 @@
1.4 * Renamed some important ML structures, while keeping the old names as
1.5 legacy aliases for some time:
1.6
1.7 + OuterSyntax ~> Outer_Syntax
1.8 OuterKeyword ~> Keyword
1.9 OuterParse ~> Parse
1.10 SpecParse ~> Parse_Spec
2.1 --- a/src/Pure/Isar/isar_document.ML Sat May 15 23:32:15 2010 +0200
2.2 +++ b/src/Pure/Isar/isar_document.ML Sat May 15 23:40:00 2010 +0200
2.3 @@ -276,23 +276,23 @@
2.4 (** concrete syntax **)
2.5
2.6 val _ =
2.7 - OuterSyntax.internal_command "Isar.define_command"
2.8 + Outer_Syntax.internal_command "Isar.define_command"
2.9 (Parse.string -- Parse.string >> (fn (id, text) =>
2.10 Toplevel.position (Position.id_only id) o
2.11 Toplevel.imperative (fn () =>
2.12 - define_command id (OuterSyntax.prepare_command (Position.id id) text))));
2.13 + define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
2.14
2.15 val _ =
2.16 - OuterSyntax.internal_command "Isar.begin_document"
2.17 + Outer_Syntax.internal_command "Isar.begin_document"
2.18 (Parse.string -- Parse.string >> (fn (id, path) =>
2.19 Toplevel.imperative (fn () => begin_document id (Path.explode path))));
2.20
2.21 val _ =
2.22 - OuterSyntax.internal_command "Isar.end_document"
2.23 + Outer_Syntax.internal_command "Isar.end_document"
2.24 (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
2.25
2.26 val _ =
2.27 - OuterSyntax.internal_command "Isar.edit_document"
2.28 + Outer_Syntax.internal_command "Isar.edit_document"
2.29 (Parse.string -- Parse.string --
2.30 Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
2.31 >> (fn ((id, new_id), edits) =>
3.1 --- a/src/Pure/Isar/isar_syn.ML Sat May 15 23:32:15 2010 +0200
3.2 +++ b/src/Pure/Isar/isar_syn.ML Sat May 15 23:40:00 2010 +0200
3.3 @@ -27,52 +27,52 @@
3.4 (** init and exit **)
3.5
3.6 val _ =
3.7 - OuterSyntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
3.8 + Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
3.9 (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
3.10
3.11 val _ =
3.12 - OuterSyntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
3.13 + Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
3.14 (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
3.15
3.16
3.17
3.18 (** markup commands **)
3.19
3.20 -val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
3.21 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
3.22 (Parse.doc_source >> IsarCmd.header_markup);
3.23
3.24 -val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
3.25 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
3.26 Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
3.27
3.28 -val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
3.29 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "section" "section heading"
3.30 Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
3.31
3.32 -val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
3.33 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
3.34 Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
3.35
3.36 val _ =
3.37 - OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
3.38 + Outer_Syntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
3.39 Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
3.40
3.41 -val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
3.42 +val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
3.43 Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
3.44
3.45 -val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
3.46 +val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
3.47 Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
3.48
3.49 -val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
3.50 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
3.51 (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
3.52
3.53 -val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
3.54 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
3.55 (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
3.56
3.57 -val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
3.58 +val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
3.59 (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
3.60
3.61 -val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
3.62 +val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
3.63 (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
3.64
3.65 -val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
3.66 +val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "txt_raw"
3.67 "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
3.68 (Parse.doc_source >> IsarCmd.proof_markup);
3.69
3.70 @@ -83,19 +83,19 @@
3.71 (* classes and sorts *)
3.72
3.73 val _ =
3.74 - OuterSyntax.command "classes" "declare type classes" Keyword.thy_decl
3.75 + Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
3.76 (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
3.77 Parse.!!! (Parse.list1 Parse.xname)) [])
3.78 >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
3.79
3.80 val _ =
3.81 - OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
3.82 + Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
3.83 (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
3.84 |-- Parse.!!! Parse.xname))
3.85 >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
3.86
3.87 val _ =
3.88 - OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables"
3.89 + Outer_Syntax.local_theory "default_sort" "declare default sort for explicit type variables"
3.90 Keyword.thy_decl
3.91 (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
3.92
3.93 @@ -103,40 +103,40 @@
3.94 (* types *)
3.95
3.96 val _ =
3.97 - OuterSyntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
3.98 + Outer_Syntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
3.99 (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
3.100 >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
3.101
3.102 val _ =
3.103 - OuterSyntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
3.104 + Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
3.105 (Scan.repeat1
3.106 (Parse.type_args -- Parse.binding --
3.107 (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
3.108 >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
3.109
3.110 val _ =
3.111 - OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
3.112 + Outer_Syntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
3.113 Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
3.114
3.115 val _ =
3.116 - OuterSyntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
3.117 + Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
3.118 (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
3.119
3.120
3.121 (* consts and syntax *)
3.122
3.123 val _ =
3.124 - OuterSyntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
3.125 + Outer_Syntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
3.126 (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
3.127
3.128 val _ =
3.129 - OuterSyntax.command "consts" "declare constants" Keyword.thy_decl
3.130 + Outer_Syntax.command "consts" "declare constants" Keyword.thy_decl
3.131 (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
3.132
3.133 val opt_overloaded = Parse.opt_keyword "overloaded";
3.134
3.135 val _ =
3.136 - OuterSyntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
3.137 + Outer_Syntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
3.138 (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
3.139
3.140 val mode_spec =
3.141 @@ -147,11 +147,11 @@
3.142 Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
3.143
3.144 val _ =
3.145 - OuterSyntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
3.146 + Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
3.147 (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
3.148
3.149 val _ =
3.150 - OuterSyntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
3.151 + Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
3.152 (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
3.153
3.154
3.155 @@ -171,18 +171,18 @@
3.156 >> (fn (left, (arr, right)) => arr (left, right));
3.157
3.158 val _ =
3.159 - OuterSyntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
3.160 + Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
3.161 (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
3.162
3.163 val _ =
3.164 - OuterSyntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
3.165 + Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
3.166 (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
3.167
3.168
3.169 (* axioms and definitions *)
3.170
3.171 val _ =
3.172 - OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
3.173 + Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
3.174 (Scan.repeat1 Parse_Spec.spec >>
3.175 (Toplevel.theory o
3.176 (IsarCmd.add_axioms o
3.177 @@ -194,7 +194,7 @@
3.178 Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
3.179
3.180 val _ =
3.181 - OuterSyntax.command "defs" "define constants" Keyword.thy_decl
3.182 + Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
3.183 (opt_unchecked_overloaded --
3.184 Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
3.185 >> (Toplevel.theory o IsarCmd.add_defs));
3.186 @@ -215,41 +215,41 @@
3.187 |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
3.188
3.189 val _ =
3.190 - OuterSyntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
3.191 + Outer_Syntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
3.192 (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
3.193
3.194
3.195 (* constant definitions and abbreviations *)
3.196
3.197 val _ =
3.198 - OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl
3.199 + Outer_Syntax.local_theory "definition" "constant definition" Keyword.thy_decl
3.200 (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args));
3.201
3.202 val _ =
3.203 - OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
3.204 + Outer_Syntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
3.205 (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
3.206 >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
3.207
3.208 val _ =
3.209 - OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors"
3.210 + Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
3.211 Keyword.thy_decl
3.212 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
3.213 >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
3.214
3.215 val _ =
3.216 - OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
3.217 + Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
3.218 Keyword.thy_decl
3.219 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
3.220 >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
3.221
3.222 val _ =
3.223 - OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
3.224 + Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
3.225 Keyword.thy_decl
3.226 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
3.227 >> (fn (mode, args) => Specification.notation_cmd true mode args));
3.228
3.229 val _ =
3.230 - OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
3.231 + Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
3.232 Keyword.thy_decl
3.233 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
3.234 >> (fn (mode, args) => Specification.notation_cmd false mode args));
3.235 @@ -258,7 +258,7 @@
3.236 (* constant specifications *)
3.237
3.238 val _ =
3.239 - OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
3.240 + Outer_Syntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
3.241 (Scan.optional Parse.fixes [] --
3.242 Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
3.243 >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
3.244 @@ -270,13 +270,13 @@
3.245 Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
3.246
3.247 val _ =
3.248 - OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
3.249 + Outer_Syntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
3.250
3.251 val _ =
3.252 - OuterSyntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
3.253 + Outer_Syntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
3.254
3.255 val _ =
3.256 - OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl
3.257 + Outer_Syntax.local_theory "declare" "declare theorems" Keyword.thy_decl
3.258 (Parse.and_list1 Parse_Spec.xthms1
3.259 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
3.260
3.261 @@ -284,15 +284,15 @@
3.262 (* name space entry path *)
3.263
3.264 val _ =
3.265 - OuterSyntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
3.266 + Outer_Syntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
3.267 (Scan.succeed (Toplevel.theory Sign.root_path));
3.268
3.269 val _ =
3.270 - OuterSyntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
3.271 + Outer_Syntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
3.272 (Scan.succeed (Toplevel.theory Sign.local_path));
3.273
3.274 fun hide_names name hide what =
3.275 - OuterSyntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
3.276 + Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
3.277 ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
3.278 (Toplevel.theory o uncurry hide));
3.279
3.280 @@ -312,55 +312,55 @@
3.281 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
3.282
3.283 val _ =
3.284 - OuterSyntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
3.285 + Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
3.286 (Parse.path >>
3.287 (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
3.288
3.289 val _ =
3.290 - OuterSyntax.command "ML" "ML text within theory or local theory"
3.291 + Outer_Syntax.command "ML" "ML text within theory or local theory"
3.292 (Keyword.tag_ml Keyword.thy_decl)
3.293 (Parse.ML_source >> (fn (txt, pos) =>
3.294 Toplevel.generic_theory
3.295 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
3.296
3.297 val _ =
3.298 - OuterSyntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
3.299 + Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
3.300 (Parse.ML_source >> (fn (txt, pos) =>
3.301 Toplevel.proof (Proof.map_context (Context.proof_map
3.302 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
3.303
3.304 val _ =
3.305 - OuterSyntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
3.306 + Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
3.307 (Parse.ML_source >> IsarCmd.ml_diag true);
3.308
3.309 val _ =
3.310 - OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
3.311 + Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
3.312 (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
3.313
3.314 val _ =
3.315 - OuterSyntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
3.316 + Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
3.317 (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
3.318
3.319 val _ =
3.320 - OuterSyntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
3.321 + Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
3.322 (Parse.ML_source >> IsarCmd.local_setup);
3.323
3.324 val _ =
3.325 - OuterSyntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
3.326 + Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
3.327 (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
3.328 >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
3.329
3.330 val _ =
3.331 - OuterSyntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
3.332 + Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
3.333 (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
3.334 >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
3.335
3.336 val _ =
3.337 - OuterSyntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
3.338 + Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
3.339 (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
3.340
3.341 val _ =
3.342 - OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
3.343 + Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
3.344 (Parse.name --
3.345 (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
3.346 Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
3.347 @@ -372,27 +372,27 @@
3.348 val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
3.349
3.350 val _ =
3.351 - OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
3.352 + Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
3.353 (Keyword.tag_ml Keyword.thy_decl)
3.354 (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
3.355
3.356 val _ =
3.357 - OuterSyntax.command "parse_translation" "install parse translation functions"
3.358 + Outer_Syntax.command "parse_translation" "install parse translation functions"
3.359 (Keyword.tag_ml Keyword.thy_decl)
3.360 (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
3.361
3.362 val _ =
3.363 - OuterSyntax.command "print_translation" "install print translation functions"
3.364 + Outer_Syntax.command "print_translation" "install print translation functions"
3.365 (Keyword.tag_ml Keyword.thy_decl)
3.366 (trfun >> (Toplevel.theory o IsarCmd.print_translation));
3.367
3.368 val _ =
3.369 - OuterSyntax.command "typed_print_translation" "install typed print translation functions"
3.370 + Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
3.371 (Keyword.tag_ml Keyword.thy_decl)
3.372 (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
3.373
3.374 val _ =
3.375 - OuterSyntax.command "print_ast_translation" "install print ast translation functions"
3.376 + Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
3.377 (Keyword.tag_ml Keyword.thy_decl)
3.378 (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
3.379
3.380 @@ -400,7 +400,7 @@
3.381 (* oracles *)
3.382
3.383 val _ =
3.384 - OuterSyntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
3.385 + Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
3.386 (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
3.387 (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
3.388
3.389 @@ -408,7 +408,7 @@
3.390 (* local theories *)
3.391
3.392 val _ =
3.393 - OuterSyntax.command "context" "enter local theory context" Keyword.thy_decl
3.394 + Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
3.395 (Parse.name --| Parse.begin >> (fn name =>
3.396 Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
3.397
3.398 @@ -421,7 +421,7 @@
3.399 Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
3.400
3.401 val _ =
3.402 - OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl
3.403 + Outer_Syntax.command "locale" "define named proof context" Keyword.thy_decl
3.404 (Parse.binding --
3.405 Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
3.406 >> (fn ((name, (expr, elems)), begin) =>
3.407 @@ -429,7 +429,7 @@
3.408 (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
3.409
3.410 val _ =
3.411 - OuterSyntax.command "sublocale"
3.412 + Outer_Syntax.command "sublocale"
3.413 "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
3.414 (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
3.415 Parse.!!! (Parse_Spec.locale_expression false)
3.416 @@ -437,7 +437,7 @@
3.417 Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
3.418
3.419 val _ =
3.420 - OuterSyntax.command "interpretation"
3.421 + Outer_Syntax.command "interpretation"
3.422 "prove interpretation of locale expression in theory" Keyword.thy_goal
3.423 (Parse.!!! (Parse_Spec.locale_expression true) --
3.424 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
3.425 @@ -445,7 +445,7 @@
3.426 Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
3.427
3.428 val _ =
3.429 - OuterSyntax.command "interpret"
3.430 + Outer_Syntax.command "interpret"
3.431 "prove interpretation of locale expression in proof context"
3.432 (Keyword.tag_proof Keyword.prf_goal)
3.433 (Parse.!!! (Parse_Spec.locale_expression true)
3.434 @@ -460,24 +460,24 @@
3.435 Scan.repeat1 Parse_Spec.context_element >> pair [];
3.436
3.437 val _ =
3.438 - OuterSyntax.command "class" "define type class" Keyword.thy_decl
3.439 + Outer_Syntax.command "class" "define type class" Keyword.thy_decl
3.440 (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
3.441 >> (fn ((name, (supclasses, elems)), begin) =>
3.442 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
3.443 (Class.class_cmd name supclasses elems #> snd)));
3.444
3.445 val _ =
3.446 - OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
3.447 + Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
3.448 (Parse.xname >> Class.subclass_cmd);
3.449
3.450 val _ =
3.451 - OuterSyntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
3.452 + Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
3.453 (Parse.multi_arity --| Parse.begin
3.454 >> (fn arities => Toplevel.print o
3.455 Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
3.456
3.457 val _ =
3.458 - OuterSyntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
3.459 + Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
3.460 ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
3.461 >> Class.classrel_cmd ||
3.462 Parse.multi_arity >> Class.instance_arity_cmd)
3.463 @@ -489,7 +489,7 @@
3.464 (* arbitrary overloading *)
3.465
3.466 val _ =
3.467 - OuterSyntax.command "overloading" "overloaded definitions" Keyword.thy_decl
3.468 + Outer_Syntax.command "overloading" "overloaded definitions" Keyword.thy_decl
3.469 (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
3.470 Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
3.471 >> Parse.triple1) --| Parse.begin
3.472 @@ -500,7 +500,7 @@
3.473 (* code generation *)
3.474
3.475 val _ =
3.476 - OuterSyntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
3.477 + Outer_Syntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
3.478 (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
3.479
3.480
3.481 @@ -510,7 +510,7 @@
3.482 (* statements *)
3.483
3.484 fun gen_theorem schematic kind =
3.485 - OuterSyntax.local_theory_to_proof'
3.486 + Outer_Syntax.local_theory_to_proof'
3.487 (if schematic then "schematic_" ^ kind else kind)
3.488 ("state " ^ (if schematic then "schematic " ^ kind else kind))
3.489 (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
3.490 @@ -528,29 +528,29 @@
3.491 val _ = gen_theorem true Thm.corollaryK;
3.492
3.493 val _ =
3.494 - OuterSyntax.local_theory_to_proof "example_proof"
3.495 + Outer_Syntax.local_theory_to_proof "example_proof"
3.496 "example proof body, without any result" Keyword.thy_schematic_goal
3.497 (Scan.succeed
3.498 (Specification.schematic_theorem_cmd "" NONE (K I)
3.499 Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
3.500
3.501 val _ =
3.502 - OuterSyntax.command "have" "state local goal"
3.503 + Outer_Syntax.command "have" "state local goal"
3.504 (Keyword.tag_proof Keyword.prf_goal)
3.505 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
3.506
3.507 val _ =
3.508 - OuterSyntax.command "hence" "abbreviates \"then have\""
3.509 + Outer_Syntax.command "hence" "abbreviates \"then have\""
3.510 (Keyword.tag_proof Keyword.prf_goal)
3.511 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
3.512
3.513 val _ =
3.514 - OuterSyntax.command "show" "state local goal, solving current obligation"
3.515 + Outer_Syntax.command "show" "state local goal, solving current obligation"
3.516 (Keyword.tag_proof Keyword.prf_asm_goal)
3.517 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
3.518
3.519 val _ =
3.520 - OuterSyntax.command "thus" "abbreviates \"then show\""
3.521 + Outer_Syntax.command "thus" "abbreviates \"then show\""
3.522 (Keyword.tag_proof Keyword.prf_asm_goal)
3.523 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
3.524
3.525 @@ -560,32 +560,32 @@
3.526 val facts = Parse.and_list1 Parse_Spec.xthms1;
3.527
3.528 val _ =
3.529 - OuterSyntax.command "then" "forward chaining"
3.530 + Outer_Syntax.command "then" "forward chaining"
3.531 (Keyword.tag_proof Keyword.prf_chain)
3.532 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
3.533
3.534 val _ =
3.535 - OuterSyntax.command "from" "forward chaining from given facts"
3.536 + Outer_Syntax.command "from" "forward chaining from given facts"
3.537 (Keyword.tag_proof Keyword.prf_chain)
3.538 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
3.539
3.540 val _ =
3.541 - OuterSyntax.command "with" "forward chaining from given and current facts"
3.542 + Outer_Syntax.command "with" "forward chaining from given and current facts"
3.543 (Keyword.tag_proof Keyword.prf_chain)
3.544 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
3.545
3.546 val _ =
3.547 - OuterSyntax.command "note" "define facts"
3.548 + Outer_Syntax.command "note" "define facts"
3.549 (Keyword.tag_proof Keyword.prf_decl)
3.550 (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
3.551
3.552 val _ =
3.553 - OuterSyntax.command "using" "augment goal facts"
3.554 + Outer_Syntax.command "using" "augment goal facts"
3.555 (Keyword.tag_proof Keyword.prf_decl)
3.556 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
3.557
3.558 val _ =
3.559 - OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
3.560 + Outer_Syntax.command "unfolding" "unfold definitions in goal and facts"
3.561 (Keyword.tag_proof Keyword.prf_decl)
3.562 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
3.563
3.564 @@ -593,22 +593,22 @@
3.565 (* proof context *)
3.566
3.567 val _ =
3.568 - OuterSyntax.command "fix" "fix local variables (Skolem constants)"
3.569 + Outer_Syntax.command "fix" "fix local variables (Skolem constants)"
3.570 (Keyword.tag_proof Keyword.prf_asm)
3.571 (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
3.572
3.573 val _ =
3.574 - OuterSyntax.command "assume" "assume propositions"
3.575 + Outer_Syntax.command "assume" "assume propositions"
3.576 (Keyword.tag_proof Keyword.prf_asm)
3.577 (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
3.578
3.579 val _ =
3.580 - OuterSyntax.command "presume" "assume propositions, to be established later"
3.581 + Outer_Syntax.command "presume" "assume propositions, to be established later"
3.582 (Keyword.tag_proof Keyword.prf_asm)
3.583 (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
3.584
3.585 val _ =
3.586 - OuterSyntax.command "def" "local definition"
3.587 + Outer_Syntax.command "def" "local definition"
3.588 (Keyword.tag_proof Keyword.prf_asm)
3.589 (Parse.and_list1
3.590 (Parse_Spec.opt_thm_name ":" --
3.591 @@ -617,24 +617,24 @@
3.592 >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
3.593
3.594 val _ =
3.595 - OuterSyntax.command "obtain" "generalized existence"
3.596 + Outer_Syntax.command "obtain" "generalized existence"
3.597 (Keyword.tag_proof Keyword.prf_asm_goal)
3.598 (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
3.599 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
3.600
3.601 val _ =
3.602 - OuterSyntax.command "guess" "wild guessing (unstructured)"
3.603 + Outer_Syntax.command "guess" "wild guessing (unstructured)"
3.604 (Keyword.tag_proof Keyword.prf_asm_goal)
3.605 (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
3.606
3.607 val _ =
3.608 - OuterSyntax.command "let" "bind text variables"
3.609 + Outer_Syntax.command "let" "bind text variables"
3.610 (Keyword.tag_proof Keyword.prf_decl)
3.611 (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
3.612 >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
3.613
3.614 val _ =
3.615 - OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
3.616 + Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
3.617 (Keyword.tag_proof Keyword.prf_decl)
3.618 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
3.619 >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
3.620 @@ -645,7 +645,7 @@
3.621 Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
3.622
3.623 val _ =
3.624 - OuterSyntax.command "case" "invoke local context"
3.625 + Outer_Syntax.command "case" "invoke local context"
3.626 (Keyword.tag_proof Keyword.prf_asm)
3.627 (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
3.628
3.629 @@ -653,17 +653,17 @@
3.630 (* proof structure *)
3.631
3.632 val _ =
3.633 - OuterSyntax.command "{" "begin explicit proof block"
3.634 + Outer_Syntax.command "{" "begin explicit proof block"
3.635 (Keyword.tag_proof Keyword.prf_open)
3.636 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
3.637
3.638 val _ =
3.639 - OuterSyntax.command "}" "end explicit proof block"
3.640 + Outer_Syntax.command "}" "end explicit proof block"
3.641 (Keyword.tag_proof Keyword.prf_close)
3.642 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
3.643
3.644 val _ =
3.645 - OuterSyntax.command "next" "enter next proof block"
3.646 + Outer_Syntax.command "next" "enter next proof block"
3.647 (Keyword.tag_proof Keyword.prf_block)
3.648 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
3.649
3.650 @@ -671,37 +671,37 @@
3.651 (* end proof *)
3.652
3.653 val _ =
3.654 - OuterSyntax.command "qed" "conclude (sub-)proof"
3.655 + Outer_Syntax.command "qed" "conclude (sub-)proof"
3.656 (Keyword.tag_proof Keyword.qed_block)
3.657 (Scan.option Method.parse >> IsarCmd.qed);
3.658
3.659 val _ =
3.660 - OuterSyntax.command "by" "terminal backward proof"
3.661 + Outer_Syntax.command "by" "terminal backward proof"
3.662 (Keyword.tag_proof Keyword.qed)
3.663 (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
3.664
3.665 val _ =
3.666 - OuterSyntax.command ".." "default proof"
3.667 + Outer_Syntax.command ".." "default proof"
3.668 (Keyword.tag_proof Keyword.qed)
3.669 (Scan.succeed IsarCmd.default_proof);
3.670
3.671 val _ =
3.672 - OuterSyntax.command "." "immediate proof"
3.673 + Outer_Syntax.command "." "immediate proof"
3.674 (Keyword.tag_proof Keyword.qed)
3.675 (Scan.succeed IsarCmd.immediate_proof);
3.676
3.677 val _ =
3.678 - OuterSyntax.command "done" "done proof"
3.679 + Outer_Syntax.command "done" "done proof"
3.680 (Keyword.tag_proof Keyword.qed)
3.681 (Scan.succeed IsarCmd.done_proof);
3.682
3.683 val _ =
3.684 - OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
3.685 + Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
3.686 (Keyword.tag_proof Keyword.qed)
3.687 (Scan.succeed IsarCmd.skip_proof);
3.688
3.689 val _ =
3.690 - OuterSyntax.command "oops" "forget proof"
3.691 + Outer_Syntax.command "oops" "forget proof"
3.692 (Keyword.tag_proof Keyword.qed_global)
3.693 (Scan.succeed Toplevel.forget_proof);
3.694
3.695 @@ -709,27 +709,27 @@
3.696 (* proof steps *)
3.697
3.698 val _ =
3.699 - OuterSyntax.command "defer" "shuffle internal proof state"
3.700 + Outer_Syntax.command "defer" "shuffle internal proof state"
3.701 (Keyword.tag_proof Keyword.prf_script)
3.702 (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
3.703
3.704 val _ =
3.705 - OuterSyntax.command "prefer" "shuffle internal proof state"
3.706 + Outer_Syntax.command "prefer" "shuffle internal proof state"
3.707 (Keyword.tag_proof Keyword.prf_script)
3.708 (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
3.709
3.710 val _ =
3.711 - OuterSyntax.command "apply" "initial refinement step (unstructured)"
3.712 + Outer_Syntax.command "apply" "initial refinement step (unstructured)"
3.713 (Keyword.tag_proof Keyword.prf_script)
3.714 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
3.715
3.716 val _ =
3.717 - OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
3.718 + Outer_Syntax.command "apply_end" "terminal refinement (unstructured)"
3.719 (Keyword.tag_proof Keyword.prf_script)
3.720 (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
3.721
3.722 val _ =
3.723 - OuterSyntax.command "proof" "backward proof"
3.724 + Outer_Syntax.command "proof" "backward proof"
3.725 (Keyword.tag_proof Keyword.prf_block)
3.726 (Scan.option Method.parse >> (fn m => Toplevel.print o
3.727 Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
3.728 @@ -742,22 +742,22 @@
3.729 Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
3.730
3.731 val _ =
3.732 - OuterSyntax.command "also" "combine calculation and current facts"
3.733 + Outer_Syntax.command "also" "combine calculation and current facts"
3.734 (Keyword.tag_proof Keyword.prf_decl)
3.735 (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
3.736
3.737 val _ =
3.738 - OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
3.739 + Outer_Syntax.command "finally" "combine calculation and current facts, exhibit result"
3.740 (Keyword.tag_proof Keyword.prf_chain)
3.741 (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
3.742
3.743 val _ =
3.744 - OuterSyntax.command "moreover" "augment calculation by current facts"
3.745 + Outer_Syntax.command "moreover" "augment calculation by current facts"
3.746 (Keyword.tag_proof Keyword.prf_decl)
3.747 (Scan.succeed (Toplevel.proof' Calculation.moreover));
3.748
3.749 val _ =
3.750 - OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
3.751 + Outer_Syntax.command "ultimately" "augment calculation by current facts, exhibit result"
3.752 (Keyword.tag_proof Keyword.prf_chain)
3.753 (Scan.succeed (Toplevel.proof' Calculation.ultimately));
3.754
3.755 @@ -765,7 +765,7 @@
3.756 (* proof navigation *)
3.757
3.758 val _ =
3.759 - OuterSyntax.command "back" "backtracking of proof command"
3.760 + Outer_Syntax.command "back" "backtracking of proof command"
3.761 (Keyword.tag_proof Keyword.prf_script)
3.762 (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
3.763
3.764 @@ -778,9 +778,9 @@
3.765 (Position.of_properties (Position.default_properties pos props), str));
3.766
3.767 val _ =
3.768 - OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
3.769 + Outer_Syntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
3.770 (props_text :|-- (fn (pos, str) =>
3.771 - (case OuterSyntax.parse pos str of
3.772 + (case Outer_Syntax.parse pos str of
3.773 [tr] => Scan.succeed (K tr)
3.774 | _ => Scan.fail_with (K "exactly one command expected"))
3.775 handle ERROR msg => Scan.fail_with (K msg)));
3.776 @@ -795,145 +795,145 @@
3.777 val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
3.778
3.779 val _ =
3.780 - OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
3.781 + Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
3.782 Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
3.783
3.784 val _ =
3.785 - OuterSyntax.improper_command "help" "print outer syntax commands" Keyword.diag
3.786 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
3.787 + Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
3.788 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
3.789
3.790 val _ =
3.791 - OuterSyntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
3.792 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
3.793 + Outer_Syntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
3.794 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
3.795
3.796 val _ =
3.797 - OuterSyntax.improper_command "print_configs" "print configuration options" Keyword.diag
3.798 + Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
3.799 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
3.800
3.801 val _ =
3.802 - OuterSyntax.improper_command "print_context" "print theory context name" Keyword.diag
3.803 + Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
3.804 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
3.805
3.806 val _ =
3.807 - OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
3.808 + Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
3.809 Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
3.810
3.811 val _ =
3.812 - OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
3.813 + Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
3.814 Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
3.815
3.816 val _ =
3.817 - OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context"
3.818 + Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
3.819 Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
3.820
3.821 val _ =
3.822 - OuterSyntax.improper_command "print_theorems"
3.823 + Outer_Syntax.improper_command "print_theorems"
3.824 "print theorems of local theory or proof context" Keyword.diag
3.825 (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
3.826
3.827 val _ =
3.828 - OuterSyntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
3.829 + Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
3.830 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
3.831
3.832 val _ =
3.833 - OuterSyntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
3.834 + Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
3.835 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
3.836 o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
3.837
3.838 val _ =
3.839 - OuterSyntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
3.840 + Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
3.841 (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
3.842
3.843 val _ =
3.844 - OuterSyntax.improper_command "print_interps"
3.845 + Outer_Syntax.improper_command "print_interps"
3.846 "print interpretations of locale for this theory" Keyword.diag
3.847 (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
3.848
3.849 val _ =
3.850 - OuterSyntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
3.851 + Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
3.852 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
3.853
3.854 val _ =
3.855 - OuterSyntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
3.856 + Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
3.857 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
3.858
3.859 val _ =
3.860 - OuterSyntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
3.861 + Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
3.862 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
3.863
3.864 val _ =
3.865 - OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
3.866 + Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
3.867 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
3.868
3.869 val _ =
3.870 - OuterSyntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
3.871 + Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
3.872 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
3.873
3.874 val _ =
3.875 - OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
3.876 + Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
3.877 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
3.878
3.879 val _ =
3.880 - OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
3.881 + Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
3.882 Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
3.883
3.884 val _ =
3.885 - OuterSyntax.improper_command "class_deps" "visualize class dependencies"
3.886 + Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
3.887 Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
3.888
3.889 val _ =
3.890 - OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
3.891 + Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
3.892 Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
3.893
3.894 val _ =
3.895 - OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
3.896 + Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
3.897 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
3.898
3.899 val _ =
3.900 - OuterSyntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
3.901 + Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
3.902 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
3.903
3.904 val _ =
3.905 - OuterSyntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
3.906 + Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
3.907 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
3.908
3.909 val _ =
3.910 - OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
3.911 + Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
3.912 (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
3.913
3.914 val _ =
3.915 - OuterSyntax.improper_command "thm" "print theorems" Keyword.diag
3.916 + Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
3.917 (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
3.918
3.919 val _ =
3.920 - OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
3.921 + Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
3.922 (opt_modes -- Scan.option Parse_Spec.xthms1
3.923 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
3.924
3.925 val _ =
3.926 - OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
3.927 + Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
3.928 (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
3.929
3.930 val _ =
3.931 - OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag
3.932 + Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
3.933 (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
3.934
3.935 val _ =
3.936 - OuterSyntax.improper_command "term" "read and print term" Keyword.diag
3.937 + Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
3.938 (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
3.939
3.940 val _ =
3.941 - OuterSyntax.improper_command "typ" "read and print type" Keyword.diag
3.942 + Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
3.943 (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
3.944
3.945 val _ =
3.946 - OuterSyntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
3.947 + Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
3.948 (Scan.succeed
3.949 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
3.950 (Code.print_codesetup o Toplevel.theory_of)));
3.951
3.952 val _ =
3.953 - OuterSyntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
3.954 + Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
3.955 (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
3.956 Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
3.957 (Toplevel.no_timing oo IsarCmd.unused_thms));
3.958 @@ -943,66 +943,66 @@
3.959 (** system commands (for interactive mode only) **)
3.960
3.961 val _ =
3.962 - OuterSyntax.improper_command "cd" "change current working directory" Keyword.diag
3.963 + Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
3.964 (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
3.965
3.966 val _ =
3.967 - OuterSyntax.improper_command "pwd" "print current working directory" Keyword.diag
3.968 + Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
3.969 (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
3.970
3.971 val _ =
3.972 - OuterSyntax.improper_command "use_thy" "use theory file" Keyword.diag
3.973 + Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
3.974 (Parse.name >> (fn name =>
3.975 Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
3.976
3.977 val _ =
3.978 - OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
3.979 + Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
3.980 (Parse.name >> (fn name =>
3.981 Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
3.982
3.983 val _ =
3.984 - OuterSyntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
3.985 + Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
3.986 (Parse.name >> (fn name =>
3.987 Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
3.988
3.989 val _ =
3.990 - OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
3.991 + Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
3.992 Keyword.diag (Parse.name >> (fn name =>
3.993 Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
3.994
3.995 val _ =
3.996 - OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
3.997 + Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
3.998 Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
3.999
3.1000 val _ =
3.1001 - OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
3.1002 + Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
3.1003 Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
3.1004
3.1005 val opt_limits =
3.1006 Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
3.1007
3.1008 val _ =
3.1009 - OuterSyntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
3.1010 + Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
3.1011 (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
3.1012
3.1013 val _ =
3.1014 - OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
3.1015 + Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
3.1016 (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
3.1017
3.1018 val _ =
3.1019 - OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
3.1020 + Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
3.1021 (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
3.1022
3.1023 val _ =
3.1024 - OuterSyntax.improper_command "commit" "commit current session to ML database" Keyword.diag
3.1025 + Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
3.1026 (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
3.1027
3.1028 val _ =
3.1029 - OuterSyntax.improper_command "quit" "quit Isabelle" Keyword.control
3.1030 + Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
3.1031 (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
3.1032
3.1033 val _ =
3.1034 - OuterSyntax.improper_command "exit" "exit Isar loop" Keyword.control
3.1035 + Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
3.1036 (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
3.1037
3.1038 end;
4.1 --- a/src/Pure/Isar/outer_syntax.ML Sat May 15 23:32:15 2010 +0200
4.2 +++ b/src/Pure/Isar/outer_syntax.ML Sat May 15 23:40:00 2010 +0200
4.3 @@ -34,7 +34,7 @@
4.4 val load_thy: string -> Position.T -> string list -> bool -> unit -> unit
4.5 end;
4.6
4.7 -structure OuterSyntax: OUTER_SYNTAX =
4.8 +structure Outer_Syntax: OUTER_SYNTAX =
4.9 struct
4.10
4.11 structure T = OuterLex;
4.12 @@ -296,3 +296,7 @@
4.13 in after_load end;
4.14
4.15 end;
4.16 +
4.17 +(*legacy alias*)
4.18 +structure OuterSyntax = Outer_Syntax;
4.19 +
5.1 --- a/src/Pure/Proof/extraction.ML Sat May 15 23:32:15 2010 +0200
5.2 +++ b/src/Pure/Proof/extraction.ML Sat May 15 23:40:00 2010 +0200
5.3 @@ -753,7 +753,7 @@
5.4 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
5.5
5.6 val _ =
5.7 - OuterSyntax.command "realizers"
5.8 + Outer_Syntax.command "realizers"
5.9 "specify realizers for primitive axioms / theorems, together with correctness proof"
5.10 Keyword.thy_decl
5.11 (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
5.12 @@ -761,17 +761,17 @@
5.13 (map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
5.14
5.15 val _ =
5.16 - OuterSyntax.command "realizability"
5.17 + Outer_Syntax.command "realizability"
5.18 "add equations characterizing realizability" Keyword.thy_decl
5.19 (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
5.20
5.21 val _ =
5.22 - OuterSyntax.command "extract_type"
5.23 + Outer_Syntax.command "extract_type"
5.24 "add equations characterizing type of extracted program" Keyword.thy_decl
5.25 (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
5.26
5.27 val _ =
5.28 - OuterSyntax.command "extract" "extract terms from proofs" Keyword.thy_decl
5.29 + Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
5.30 (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
5.31 extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
5.32
6.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat May 15 23:32:15 2010 +0200
6.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat May 15 23:40:00 2010 +0200
6.3 @@ -189,36 +189,36 @@
6.4 (* additional outer syntax for Isar *)
6.5
6.6 fun prP () =
6.7 - OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
6.8 + Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
6.9 (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
6.10 if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
6.11 else (Toplevel.quiet := false; Toplevel.print_state true state))));
6.12
6.13 fun undoP () = (*undo without output -- historical*)
6.14 - OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
6.15 + Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
6.16 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
6.17
6.18 fun restartP () =
6.19 - OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
6.20 + Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
6.21 (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
6.22
6.23 fun kill_proofP () =
6.24 - OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
6.25 + Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
6.26 (Scan.succeed (Toplevel.no_timing o
6.27 Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
6.28
6.29 fun inform_file_processedP () =
6.30 - OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
6.31 + Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
6.32 (Parse.name >> (fn file =>
6.33 Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
6.34
6.35 fun inform_file_retractedP () =
6.36 - OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
6.37 + Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
6.38 (Parse.name >> (Toplevel.no_timing oo
6.39 (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
6.40
6.41 fun process_pgipP () =
6.42 - OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
6.43 + Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
6.44 (Parse.text >> (Toplevel.no_timing oo
6.45 (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
6.46
7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 15 23:32:15 2010 +0200
7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 15 23:40:00 2010 +0200
7.3 @@ -382,7 +382,7 @@
7.4
7.5 (* Sending commands to Isar *)
7.6
7.7 -fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
7.8 +fun isarcmd s = Isar.>>> (Outer_Syntax.parse Position.none s);
7.9
7.10 (* TODO:
7.11 - apply a command given a transition function;
7.12 @@ -1013,7 +1013,7 @@
7.13 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
7.14
7.15 fun init_outer_syntax () =
7.16 - OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
7.17 + Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
7.18 (Parse.text >> (Toplevel.no_timing oo
7.19 (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
7.20
8.1 --- a/src/Pure/System/isar.ML Sat May 15 23:32:15 2010 +0200
8.2 +++ b/src/Pure/System/isar.ML Sat May 15 23:40:00 2010 +0200
8.3 @@ -141,7 +141,7 @@
8.4 Secure.open_unsynchronized ();
8.5 if do_init then init () else ();
8.6 if welcome then writeln (Session.welcome ()) else ();
8.7 - uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
8.8 + uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());
8.9
8.10 end;
8.11
8.12 @@ -164,35 +164,35 @@
8.13 (* global history *)
8.14
8.15 val _ =
8.16 - OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
8.17 + Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
8.18 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
8.19
8.20 val _ =
8.21 - OuterSyntax.improper_command "linear_undo" "undo commands" Keyword.control
8.22 + Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
8.23 (Scan.optional Parse.nat 1 >>
8.24 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
8.25
8.26 val _ =
8.27 - OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
8.28 + Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
8.29 (Scan.optional Parse.nat 1 >>
8.30 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
8.31
8.32 val _ =
8.33 - OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
8.34 + Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
8.35 Keyword.control
8.36 (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
8.37 Toplevel.keep (fn state =>
8.38 if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
8.39
8.40 val _ =
8.41 - OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
8.42 + Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
8.43 Keyword.control
8.44 (Parse.name >>
8.45 (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
8.46 | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
8.47
8.48 val _ =
8.49 - OuterSyntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
8.50 + Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
8.51 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
8.52
8.53 end;
9.1 --- a/src/Pure/System/session.ML Sat May 15 23:32:15 2010 +0200
9.2 +++ b/src/Pure/System/session.ML Sat May 15 23:40:00 2010 +0200
9.3 @@ -48,7 +48,7 @@
9.4 (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
9.5
9.6 val _ =
9.7 - OuterSyntax.improper_command "welcome" "print welcome message" Keyword.diag
9.8 + Outer_Syntax.improper_command "welcome" "print welcome message" Keyword.diag
9.9 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
9.10
9.11
10.1 --- a/src/Pure/Thy/thy_info.ML Sat May 15 23:32:15 2010 +0200
10.2 +++ b/src/Pure/Thy/thy_info.ML Sat May 15 23:40:00 2010 +0200
10.3 @@ -346,7 +346,7 @@
10.4 val _ = CRITICAL (fn () =>
10.5 change_deps name (Option.map (fn {master, text, parents, files, ...} =>
10.6 make_deps upd_time master text parents files)));
10.7 - val after_load = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
10.8 + val after_load = Outer_Syntax.load_thy name pos text (time orelse ! Output.timing);
10.9 val _ =
10.10 CRITICAL (fn () =>
10.11 (change_deps name
11.1 --- a/src/Pure/Tools/find_consts.ML Sat May 15 23:32:15 2010 +0200
11.2 +++ b/src/Pure/Tools/find_consts.ML Sat May 15 23:40:00 2010 +0200
11.3 @@ -154,7 +154,7 @@
11.4 Parse.xname >> Loose;
11.5
11.6 val _ =
11.7 - OuterSyntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
11.8 + Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
11.9 (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
11.10 >> (Toplevel.no_timing oo find_consts_cmd));
11.11
12.1 --- a/src/Pure/Tools/find_theorems.ML Sat May 15 23:32:15 2010 +0200
12.2 +++ b/src/Pure/Tools/find_theorems.ML Sat May 15 23:40:00 2010 +0200
12.3 @@ -483,7 +483,7 @@
12.4 in
12.5
12.6 val _ =
12.7 - OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria"
12.8 + Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
12.9 Keyword.diag
12.10 (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
12.11 >> (Toplevel.no_timing oo find_theorems_cmd));
13.1 --- a/src/Pure/codegen.ML Sat May 15 23:32:15 2010 +0200
13.2 +++ b/src/Pure/codegen.ML Sat May 15 23:40:00 2010 +0200
13.3 @@ -969,7 +969,7 @@
13.4 (Parse.verbatim >> strip_whitespace));
13.5
13.6 val _ =
13.7 - OuterSyntax.command "types_code"
13.8 + Outer_Syntax.command "types_code"
13.9 "associate types with target language types" Keyword.thy_decl
13.10 (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
13.11 (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
13.12 @@ -977,7 +977,7 @@
13.13 (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
13.14
13.15 val _ =
13.16 - OuterSyntax.command "consts_code"
13.17 + Outer_Syntax.command "consts_code"
13.18 "associate constants with target language code" Keyword.thy_decl
13.19 (Scan.repeat1
13.20 (Parse.term --|
13.21 @@ -1018,12 +1018,12 @@
13.22 #> add_preprocessor unfold_preprocessor;
13.23
13.24 val _ =
13.25 - OuterSyntax.command "code_library"
13.26 + Outer_Syntax.command "code_library"
13.27 "generates code for terms (one structure for each theory)" Keyword.thy_decl
13.28 (parse_code true);
13.29
13.30 val _ =
13.31 - OuterSyntax.command "code_module"
13.32 + Outer_Syntax.command "code_module"
13.33 "generates code for terms (single structure, incremental)" Keyword.thy_decl
13.34 (parse_code false);
13.35
14.1 --- a/src/Pure/pure_setup.ML Sat May 15 23:32:15 2010 +0200
14.2 +++ b/src/Pure/pure_setup.ML Sat May 15 23:40:00 2010 +0200
14.3 @@ -9,7 +9,7 @@
14.4 val theory = ThyInfo.get_theory;
14.5
14.6 Context.>> (Context.map_theory
14.7 - (OuterSyntax.process_file (Path.explode "Pure.thy") #>
14.8 + (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
14.9 Theory.end_theory));
14.10 structure Pure = struct val thy = ML_Context.the_global_context () end;
14.11 Context.set_thread_data NONE;