src/Pure/Isar/isar_syn.ML
author wenzelm
Wed Jul 25 22:20:51 2007 +0200 (2007-07-25 ago)
changeset 23989 d7df8545f9f6
parent 23865 3ea92c014a3e
child 24115 39b407fd6e82
permissions -rw-r--r--
added command 'print_options';
     1 (*  Title:      Pure/Isar/isar_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar/Pure outer syntax.
     6 *)
     7 
     8 structure IsarSyn: sig end =
     9 struct
    10 
    11 structure P = OuterParse and K = OuterKeyword;
    12 
    13 
    14 (** init and exit **)
    15 
    16 val theoryP =
    17   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
    18     (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory));
    19 
    20 val endP =
    21   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    22     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
    23 
    24 
    25 (** markup commands **)
    26 
    27 val headerP = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
    28   (P.position P.text >> IsarCmd.add_header);
    29 
    30 val chapterP = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
    31   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter);
    32 
    33 val sectionP = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
    34   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section);
    35 
    36 val subsectionP = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
    37   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection);
    38 
    39 val subsubsectionP =
    40   OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
    41   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection);
    42 
    43 val textP = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
    44   K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text);
    45 
    46 val text_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw"
    47   "raw document preparation text"
    48   K.thy_decl (P.position P.text >> IsarCmd.add_text_raw);
    49 
    50 val sectP = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
    51   (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect);
    52 
    53 val subsectP = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
    54   (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect);
    55 
    56 val subsubsectP = OuterSyntax.markup_command ThyOutput.Markup "subsubsect"
    57   "formal comment (proof)" (K.tag_proof K.prf_heading)
    58   (P.position P.text >> IsarCmd.add_subsubsect);
    59 
    60 val txtP = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
    61   (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt);
    62 
    63 val txt_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
    64   "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
    65   (P.position P.text >> IsarCmd.add_txt_raw);
    66 
    67 
    68 
    69 (** theory sections **)
    70 
    71 (* classes and sorts *)
    72 
    73 val classesP =
    74   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    75     (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    76         P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class));
    77 
    78 val classrelP =
    79   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    80     (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
    81     >> (Toplevel.theory o AxClass.axiomatize_classrel));
    82 
    83 val defaultsortP =
    84   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    85     (P.sort >> (Toplevel.theory o Sign.add_defsort));
    86 
    87 val axclassP =
    88   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    89     (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    90         P.!!! (P.list1 P.xname)) []
    91         -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    92       >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y)));
    93 
    94 
    95 (* types *)
    96 
    97 val typedeclP =
    98   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
    99     (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
   100       Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
   101 
   102 val typeabbrP =
   103   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   104     (Scan.repeat1
   105       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
   106       >> (Toplevel.theory o Sign.add_tyabbrs o
   107         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   108 
   109 val nontermP =
   110   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   111     K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals));
   112 
   113 val aritiesP =
   114   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   115     (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
   116 
   117 
   118 (* consts and syntax *)
   119 
   120 val judgmentP =
   121   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   122     (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
   123 
   124 val constsP =
   125   OuterSyntax.command "consts" "declare constants" K.thy_decl
   126     (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts));
   127 
   128 val opt_overloaded = P.opt_keyword "overloaded";
   129 
   130 val finalconstsP =
   131   OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
   132     (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
   133 
   134 val mode_spec =
   135   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
   136 
   137 val opt_mode =
   138   Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
   139 
   140 val syntaxP =
   141   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   142     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
   143 
   144 val no_syntaxP =
   145   OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
   146     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
   147 
   148 
   149 (* translations *)
   150 
   151 val trans_pat =
   152   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   153 
   154 fun trans_arrow toks =
   155   ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
   156     (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
   157     (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
   158 
   159 val trans_line =
   160   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   161     >> (fn (left, (arr, right)) => arr (left, right));
   162 
   163 val translationsP =
   164   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   165     (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
   166 
   167 val no_translationsP =
   168   OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
   169     (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
   170 
   171 
   172 (* axioms and definitions *)
   173 
   174 val axiomsP =
   175   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   176     (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
   177 
   178 val opt_unchecked_overloaded =
   179   Scan.optional (P.$$$ "(" |-- P.!!!
   180     (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
   181       P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
   182 
   183 val defsP =
   184   OuterSyntax.command "defs" "define constants" K.thy_decl
   185     (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
   186       >> (Toplevel.theory o IsarCmd.add_defs));
   187 
   188 
   189 (* old constdefs *)
   190 
   191 val old_constdecl =
   192   P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
   193   P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
   194     --| Scan.option P.where_ >> P.triple1 ||
   195   P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   196 
   197 val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   198 
   199 val structs =
   200   Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
   201 
   202 val constdefsP =
   203   OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
   204     (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
   205 
   206 
   207 (* constant definitions and abbreviations *)
   208 
   209 val constdecl =
   210   P.name --
   211     (P.where_ >> K (NONE, NoSyn) ||
   212       P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
   213       Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   214   >> P.triple2;
   215 
   216 val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   217 
   218 val definitionP =
   219   OuterSyntax.command "definition" "constant definition" K.thy_decl
   220     (P.opt_target -- constdef
   221     >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
   222 
   223 val abbreviationP =
   224   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
   225     (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
   226     >> (fn ((loc, mode), args) =>
   227         Toplevel.local_theory loc (Specification.abbreviation mode args)));
   228 
   229 val notationP =
   230   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
   231     (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   232     >> (fn ((loc, mode), args) =>
   233         Toplevel.local_theory loc (Specification.notation mode args)));
   234 
   235 
   236 (* constant specifications *)
   237 
   238 val axiomatizationP =
   239   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
   240     (P.opt_target --
   241      (Scan.optional P.fixes [] --
   242       Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
   243     >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
   244 
   245 
   246 (* theorems *)
   247 
   248 fun theorems kind = P.opt_target -- SpecParse.name_facts
   249   >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
   250 
   251 val theoremsP =
   252   OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
   253 
   254 val lemmasP =
   255   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
   256 
   257 val declareP =
   258   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl
   259     (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
   260       >> (fn (loc, args) => Toplevel.local_theory loc
   261           (#2 o Specification.theorems "" [(("", []), args)])));
   262 
   263 
   264 (* name space entry path *)
   265 
   266 val globalP =
   267   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   268     (Scan.succeed (Toplevel.theory Sign.root_path));
   269 
   270 val localP =
   271   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   272     (Scan.succeed (Toplevel.theory Sign.local_path));
   273 
   274 val hideP =
   275   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
   276     ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
   277       (Toplevel.theory o uncurry Sign.hide_names));
   278 
   279 
   280 (* use ML text *)
   281 
   282 val useP =
   283   OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
   284     (P.path >> (Toplevel.no_timing oo IsarCmd.use));
   285 
   286 val mlP =
   287   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
   288     (P.text >> IsarCmd.use_mltext true);
   289 
   290 val ml_commandP =
   291   OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
   292     (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
   293 
   294 val ml_setupP =
   295   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
   296     (P.text >> IsarCmd.use_mltext_theory);
   297 
   298 val setupP =
   299   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
   300     (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
   301 
   302 val method_setupP =
   303   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   304     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
   305       >> (Toplevel.theory o Method.method_setup));
   306 
   307 val declarationP =
   308   OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
   309     (P.opt_target -- P.text
   310     >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
   311 
   312 val simproc_setupP =
   313   OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
   314     (P.opt_target --
   315       P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
   316       Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
   317     >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
   318 
   319 
   320 (* translation functions *)
   321 
   322 val trfun = P.opt_keyword "advanced" -- P.text;
   323 
   324 val parse_ast_translationP =
   325   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   326     (K.tag_ml K.thy_decl)
   327     (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   328 
   329 val parse_translationP =
   330   OuterSyntax.command "parse_translation" "install parse translation functions"
   331     (K.tag_ml K.thy_decl)
   332     (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   333 
   334 val print_translationP =
   335   OuterSyntax.command "print_translation" "install print translation functions"
   336     (K.tag_ml K.thy_decl)
   337     (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   338 
   339 val typed_print_translationP =
   340   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   341     (K.tag_ml K.thy_decl)
   342     (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   343 
   344 val print_ast_translationP =
   345   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   346     (K.tag_ml K.thy_decl)
   347     (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   348 
   349 val token_translationP =
   350   OuterSyntax.command "token_translation" "install token translation functions"
   351     (K.tag_ml K.thy_decl)
   352     (P.text >> (Toplevel.theory o IsarCmd.token_translation));
   353 
   354 
   355 (* oracles *)
   356 
   357 val oracleP =
   358   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
   359     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
   360       -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
   361 
   362 
   363 (* local theories *)
   364 
   365 val contextP =
   366   OuterSyntax.command "context" "enter local theory context" K.thy_decl
   367     (P.name --| P.begin >> (fn name =>
   368       Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
   369 
   370 
   371 (* locales *)
   372 
   373 val locale_val =
   374   (SpecParse.locale_expr --
   375     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   376   Scan.repeat1 SpecParse.context_element >> pair Locale.empty);
   377 
   378 val localeP =
   379   OuterSyntax.command "locale" "define named proof context" K.thy_decl
   380     ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) -- P.name
   381         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
   382         -- P.opt_begin
   383       >> (fn (((is_open, name), (expr, elems)), begin) =>
   384           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   385             (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
   386 
   387 val interpretationP =
   388   OuterSyntax.command "interpretation"
   389     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
   390     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
   391       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
   392       SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   393         >> (fn ((x, y), z) => Toplevel.print o
   394             Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
   395 
   396 val interpretP =
   397   OuterSyntax.command "interpret"
   398     "prove and register interpretation of locale expression in proof context"
   399     (K.tag_proof K.prf_goal)
   400     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   401       >> (fn ((x, y), z) => Toplevel.print o
   402           Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
   403 
   404 
   405 (* classes *)
   406 
   407 local
   408 
   409 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
   410 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
   411 
   412 in
   413 
   414 val classP =
   415   OuterSyntax.command "class" "define type class" K.thy_decl (
   416     P.name
   417     -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
   418     --| P.$$$ "=" -- (
   419       class_subP --| P.$$$ "+" -- class_bodyP
   420       || class_subP >> rpair []
   421       || class_bodyP >> pair [])
   422     -- P.opt_begin
   423     >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
   424         Toplevel.begin_local_theory begin
   425           (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
   426 
   427 val instanceP =
   428   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
   429       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   430            >> ClassPackage.instance_class_cmd
   431       || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   432            >> ClassPackage.instance_sort_cmd
   433       || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
   434            >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
   435     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   436 
   437 end;
   438 
   439 
   440 (* code generation *)
   441 
   442 val code_datatypeP =
   443   OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
   444     (Scan.repeat1 P.term >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd));
   445 
   446 
   447 
   448 (** proof commands **)
   449 
   450 (* statements *)
   451 
   452 fun gen_theorem kind =
   453   OuterSyntax.command kind ("state " ^ kind) K.thy_goal
   454     (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   455       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   456       SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
   457       (Toplevel.print o
   458        Toplevel.local_theory_to_proof loc
   459          (Specification.theorem kind NONE (K I) a elems concl))));
   460 
   461 val theoremP = gen_theorem Thm.theoremK;
   462 val lemmaP = gen_theorem Thm.lemmaK;
   463 val corollaryP = gen_theorem Thm.corollaryK;
   464 
   465 val haveP =
   466   OuterSyntax.command "have" "state local goal"
   467     (K.tag_proof K.prf_goal)
   468     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   469 
   470 val henceP =
   471   OuterSyntax.command "hence" "abbreviates \"then have\""
   472     (K.tag_proof K.prf_goal)
   473     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   474 
   475 val showP =
   476   OuterSyntax.command "show" "state local goal, solving current obligation"
   477     (K.tag_proof K.prf_asm_goal)
   478     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   479 
   480 val thusP =
   481   OuterSyntax.command "thus" "abbreviates \"then show\""
   482     (K.tag_proof K.prf_asm_goal)
   483     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   484 
   485 
   486 (* facts *)
   487 
   488 val facts = P.and_list1 SpecParse.xthms1;
   489 
   490 val thenP =
   491   OuterSyntax.command "then" "forward chaining"
   492     (K.tag_proof K.prf_chain)
   493     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
   494 
   495 val fromP =
   496   OuterSyntax.command "from" "forward chaining from given facts"
   497     (K.tag_proof K.prf_chain)
   498     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
   499 
   500 val withP =
   501   OuterSyntax.command "with" "forward chaining from given and current facts"
   502     (K.tag_proof K.prf_chain)
   503     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
   504 
   505 val noteP =
   506   OuterSyntax.command "note" "define facts"
   507     (K.tag_proof K.prf_decl)
   508     (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   509 
   510 val usingP =
   511   OuterSyntax.command "using" "augment goal facts"
   512     (K.tag_proof K.prf_decl)
   513     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
   514 
   515 val unfoldingP =
   516   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
   517     (K.tag_proof K.prf_decl)
   518     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
   519 
   520 
   521 (* proof context *)
   522 
   523 val fixP =
   524   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
   525     (K.tag_proof K.prf_asm)
   526     (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
   527 
   528 val assumeP =
   529   OuterSyntax.command "assume" "assume propositions"
   530     (K.tag_proof K.prf_asm)
   531     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   532 
   533 val presumeP =
   534   OuterSyntax.command "presume" "assume propositions, to be established later"
   535     (K.tag_proof K.prf_asm)
   536     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   537 
   538 val defP =
   539   OuterSyntax.command "def" "local definition"
   540     (K.tag_proof K.prf_asm)
   541     (P.and_list1
   542       (SpecParse.opt_thm_name ":" --
   543         ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   544     >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   545 
   546 val obtainP =
   547   OuterSyntax.command "obtain" "generalized existence"
   548     (K.tag_proof K.prf_asm_goal)
   549     (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   550       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
   551 
   552 val guessP =
   553   OuterSyntax.command "guess" "wild guessing (unstructured)"
   554     (K.tag_proof K.prf_asm_goal)
   555     (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
   556 
   557 val letP =
   558   OuterSyntax.command "let" "bind text variables"
   559     (K.tag_proof K.prf_decl)
   560     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
   561       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
   562 
   563 val case_spec =
   564   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   565     P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
   566 
   567 val caseP =
   568   OuterSyntax.command "case" "invoke local context"
   569     (K.tag_proof K.prf_asm)
   570     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
   571 
   572 
   573 (* proof structure *)
   574 
   575 val begin_blockP =
   576   OuterSyntax.command "{" "begin explicit proof block"
   577     (K.tag_proof K.prf_open)
   578     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
   579 
   580 val end_blockP =
   581   OuterSyntax.command "}" "end explicit proof block"
   582     (K.tag_proof K.prf_close)
   583     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
   584 
   585 val nextP =
   586   OuterSyntax.command "next" "enter next proof block"
   587     (K.tag_proof K.prf_block)
   588     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
   589 
   590 
   591 (* end proof *)
   592 
   593 val qedP =
   594   OuterSyntax.command "qed" "conclude (sub-)proof"
   595     (K.tag_proof K.qed_block)
   596     (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed));
   597 
   598 val terminal_proofP =
   599   OuterSyntax.command "by" "terminal backward proof"
   600     (K.tag_proof K.qed)
   601     (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof));
   602 
   603 val default_proofP =
   604   OuterSyntax.command ".." "default proof"
   605     (K.tag_proof K.qed)
   606     (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
   607 
   608 val immediate_proofP =
   609   OuterSyntax.command "." "immediate proof"
   610     (K.tag_proof K.qed)
   611     (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
   612 
   613 val done_proofP =
   614   OuterSyntax.command "done" "done proof"
   615     (K.tag_proof K.qed)
   616     (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
   617 
   618 val skip_proofP =
   619   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
   620     (K.tag_proof K.qed)
   621     (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
   622 
   623 val forget_proofP =
   624   OuterSyntax.command "oops" "forget proof"
   625     (K.tag_proof K.qed_global)
   626     (Scan.succeed Toplevel.forget_proof);
   627 
   628 
   629 (* proof steps *)
   630 
   631 val deferP =
   632   OuterSyntax.command "defer" "shuffle internal proof state"
   633     (K.tag_proof K.prf_script)
   634     (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
   635 
   636 val preferP =
   637   OuterSyntax.command "prefer" "shuffle internal proof state"
   638     (K.tag_proof K.prf_script)
   639     (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
   640 
   641 val applyP =
   642   OuterSyntax.command "apply" "initial refinement step (unstructured)"
   643     (K.tag_proof K.prf_script)
   644     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   645 
   646 val apply_endP =
   647   OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   648     (K.tag_proof K.prf_script)
   649     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   650 
   651 val proofP =
   652   OuterSyntax.command "proof" "backward proof"
   653     (K.tag_proof K.prf_block)
   654     (Scan.option Method.parse >> (fn m => Toplevel.print o
   655       Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o
   656       Toplevel.skip_proof (History.apply (fn i => i + 1))));
   657 
   658 
   659 (* calculational proof commands *)
   660 
   661 val calc_args =
   662   Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
   663 
   664 val alsoP =
   665   OuterSyntax.command "also" "combine calculation and current facts"
   666     (K.tag_proof K.prf_decl)
   667     (calc_args >> (Toplevel.proofs' o Calculation.also));
   668 
   669 val finallyP =
   670   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
   671     (K.tag_proof K.prf_chain)
   672     (calc_args >> (Toplevel.proofs' o Calculation.finally_));
   673 
   674 val moreoverP =
   675   OuterSyntax.command "moreover" "augment calculation by current facts"
   676     (K.tag_proof K.prf_decl)
   677     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   678 
   679 val ultimatelyP =
   680   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
   681     (K.tag_proof K.prf_chain)
   682     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   683 
   684 
   685 (* proof navigation *)
   686 
   687 val backP =
   688   OuterSyntax.command "back" "backtracking of proof command"
   689     (K.tag_proof K.prf_script)
   690     (Scan.succeed (Toplevel.print o IsarCmd.back));
   691 
   692 
   693 (* history *)
   694 
   695 val cannot_undoP =
   696   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   697     (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
   698 
   699 val redoP =
   700   OuterSyntax.improper_command "redo" "redo last command" K.control
   701     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
   702 
   703 val undos_proofP =
   704   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   705     (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof));
   706 
   707 val undoP =
   708   OuterSyntax.improper_command "undo" "undo last command" K.control
   709     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo));
   710 
   711 val killP =
   712   OuterSyntax.improper_command "kill" "kill current history node" K.control
   713     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill));
   714 
   715 
   716 
   717 (** diagnostic commands (for interactive mode only) **)
   718 
   719 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   720 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
   721 
   722 val pretty_setmarginP =
   723   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   724     K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   725 
   726 val helpP =
   727   OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
   728     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   729 
   730 val print_commandsP =
   731   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
   732     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   733 
   734 val print_optionsP =
   735   OuterSyntax.improper_command "print_options" "print configuration options" K.diag
   736     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_options));
   737 
   738 val print_contextP =
   739   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
   740     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   741 
   742 val print_theoryP =
   743   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   744     (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
   745 
   746 val print_syntaxP =
   747   OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
   748     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
   749 
   750 val print_abbrevsP =
   751   OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
   752     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
   753 
   754 val print_theoremsP =
   755   OuterSyntax.improper_command "print_theorems"
   756       "print theorems of local theory or proof context" K.diag
   757     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
   758 
   759 val print_localesP =
   760   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
   761     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   762 
   763 val print_classesP =
   764   OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
   765     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
   766       o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
   767 
   768 val print_localeP =
   769   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
   770     (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
   771 
   772 val print_registrationsP =
   773   OuterSyntax.improper_command "print_interps"
   774     "print interpretations of named locale" K.diag
   775     (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
   776       >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
   777 
   778 val print_attributesP =
   779   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
   780     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   781 
   782 val print_simpsetP =
   783   OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
   784     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
   785 
   786 val print_rulesP =
   787   OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
   788     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
   789 
   790 val print_induct_rulesP =
   791   OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
   792     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
   793 
   794 val print_trans_rulesP =
   795   OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
   796     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   797 
   798 val print_methodsP =
   799   OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
   800     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
   801 
   802 val print_antiquotationsP =
   803   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
   804     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   805 
   806 val thy_depsP =
   807   OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
   808     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
   809 
   810 val class_depsP =
   811   OuterSyntax.improper_command "class_deps" "visualize class dependencies"
   812     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
   813 
   814 val thm_depsP =
   815   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   816     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   817 
   818 local
   819 
   820 val criterion =
   821   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
   822   P.reserved "intro" >> K FindTheorems.Intro ||
   823   P.reserved "elim" >> K FindTheorems.Elim ||
   824   P.reserved "dest" >> K FindTheorems.Dest ||
   825   P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
   826   P.term >> FindTheorems.Pattern;
   827 
   828 val options =
   829   Scan.optional
   830     (P.$$$ "(" |--
   831       P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
   832         --| P.$$$ ")")) (NONE, true);
   833 in
   834 
   835 val find_theoremsP =
   836   OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
   837     (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   838       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
   839 
   840 end;
   841 
   842 val print_bindsP =
   843   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   844     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   845 
   846 val print_factsP =
   847   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
   848     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
   849 
   850 val print_casesP =
   851   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
   852     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   853 
   854 val print_stmtsP =
   855   OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
   856     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   857 
   858 val print_thmsP =
   859   OuterSyntax.improper_command "thm" "print theorems" K.diag
   860     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   861 
   862 val print_prfsP =
   863   OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   864     (opt_modes -- Scan.option SpecParse.xthms1
   865       >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   866 
   867 val print_full_prfsP =
   868   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   869     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   870 
   871 val print_propP =
   872   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   873     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   874 
   875 val print_termP =
   876   OuterSyntax.improper_command "term" "read and print term" K.diag
   877     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   878 
   879 val print_typeP =
   880   OuterSyntax.improper_command "typ" "read and print type" K.diag
   881     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   882 
   883 val print_codesetupP =
   884   OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
   885     (Scan.succeed
   886       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   887         (CodegenData.print_codesetup o Toplevel.theory_of)));
   888 
   889 
   890 (** system commands (for interactive mode only) **)
   891 
   892 val cdP =
   893   OuterSyntax.improper_command "cd" "change current working directory" K.diag
   894     (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
   895 
   896 val pwdP =
   897   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   898     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   899 
   900 val use_thyP =
   901   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   902     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
   903 
   904 val update_thyP =
   905   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   906     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
   907 
   908 val touch_thyP =
   909   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
   910     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
   911 
   912 val touch_all_thysP =
   913   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   914     (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
   915 
   916 val touch_child_thysP =
   917   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
   918     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
   919 
   920 val remove_thyP =
   921   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   922     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   923 
   924 val kill_thyP =
   925   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   926     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   927 
   928 val display_draftsP =
   929   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
   930     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
   931 
   932 val print_draftsP =
   933   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
   934     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   935 
   936 val opt_limits =
   937   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   938 
   939 val prP =
   940   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
   941     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   942 
   943 val disable_prP =
   944   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   945     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   946 
   947 val enable_prP =
   948   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   949     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   950 
   951 val commitP =
   952   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   953     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
   954 
   955 val quitP =
   956   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   957     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   958 
   959 val exitP =
   960   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   961     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   962 
   963 val init_toplevelP =
   964   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
   965     (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
   966 
   967 val welcomeP =
   968   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
   969     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
   970 
   971 
   972 
   973 (** the Pure outer syntax **)
   974 
   975 (*keep keywords consistent with the parsers, otherwise be prepared for
   976   unexpected errors*)
   977 
   978 val _ = OuterSyntax.add_keywords
   979  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   980   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   981   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   982   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   983   "constrains", "defines", "fixes", "for", "identifier", "if",
   984   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   985   "notes", "obtains", "open", "output", "overloaded", "shows",
   986   "structure", "unchecked", "uses", "where", "|"];
   987 
   988 val _ = OuterSyntax.add_parsers [
   989   (*theory structure*)
   990   theoryP, endP,
   991   (*markup commands*)
   992   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   993   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   994   (*theory sections*)
   995   classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   996   nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
   997   no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
   998   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   999   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
  1000   ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
  1001   simproc_setupP, parse_ast_translationP, parse_translationP,
  1002   print_translationP, typed_print_translationP,
  1003   print_ast_translationP, token_translationP, oracleP, contextP,
  1004   localeP, classP, instanceP, code_datatypeP,
  1005   (*proof commands*)
  1006   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
  1007   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
  1008   withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
  1009   qedP, terminal_proofP, default_proofP, immediate_proofP,
  1010   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
  1011   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
  1012   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
  1013   interpretP,
  1014   (*diagnostic commands*)
  1015   pretty_setmarginP, helpP, print_classesP, print_commandsP,
  1016   print_optionsP, print_contextP, print_theoryP, print_syntaxP,
  1017   print_abbrevsP, print_factsP, print_theoremsP, print_localesP,
  1018   print_localeP, print_registrationsP, print_attributesP,
  1019   print_simpsetP, print_rulesP, print_induct_rulesP,
  1020   print_trans_rulesP, print_methodsP, print_antiquotationsP,
  1021   thy_depsP, class_depsP, thm_depsP, find_theoremsP, print_bindsP,
  1022   print_casesP, print_stmtsP, print_thmsP, print_prfsP,
  1023   print_full_prfsP, print_propP, print_termP, print_typeP,
  1024   print_codesetupP,
  1025   (*system commands*)
  1026   cdP, pwdP, use_thyP, update_thyP, touch_thyP, touch_all_thysP,
  1027   touch_child_thysP, remove_thyP, kill_thyP, display_draftsP,
  1028   print_draftsP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
  1029   init_toplevelP, welcomeP];
  1030 
  1031 end;