src/Pure/Isar/isar_syn.ML
author wenzelm
Fri Sep 01 00:33:14 2000 +0200 (2000-09-01)
changeset 9776 a126bc3b7376
parent 9731 3eb72671e5db
child 9978 d4af3f6fa997
permissions -rw-r--r--
'declare' made proper command;
     1 (*  Title:      Pure/Isar/isar_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Isar/Pure outer syntax.
     7 *)
     8 
     9 signature ISAR_SYN =
    10 sig
    11   val keywords: string list
    12   val parsers: OuterSyntax.parser list
    13 end;
    14 
    15 structure IsarSyn: ISAR_SYN =
    16 struct
    17 
    18 structure P = OuterParse and K = OuterSyntax.Keyword;
    19 
    20 
    21 (** init and exit **)
    22 
    23 val theoryP =
    24   OuterSyntax.command "theory" "begin theory" K.thy_begin
    25     (ThyHeader.args >> (Toplevel.print oo IsarThy.theory));
    26 
    27 val end_excursionP =
    28   OuterSyntax.command "end" "end current excursion" K.thy_end
    29     (Scan.succeed (Toplevel.print o Toplevel.exit));
    30 
    31 val contextP =
    32   OuterSyntax.improper_command "context" "switch theory context" K.thy_switch
    33     (P.name >> (Toplevel.print oo IsarThy.context));
    34 
    35 
    36 
    37 (** markup commands **)
    38 
    39 val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag
    40   (P.comment >> IsarThy.add_header);
    41 
    42 val chapterP = OuterSyntax.markup_command IsarOutput.Markup "chapter" "chapter heading"
    43   K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
    44 
    45 val sectionP = OuterSyntax.markup_command IsarOutput.Markup "section" "section heading"
    46   K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_section));
    47 
    48 val subsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsection" "subsection heading"
    49   K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
    50 
    51 val subsubsectionP =
    52   OuterSyntax.markup_command IsarOutput.Markup "subsubsection" "subsubsection heading"
    53   K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    54 
    55 val textP = OuterSyntax.markup_command IsarOutput.MarkupEnv "text" "formal comment (theory)"
    56   K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text));
    57 
    58 val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw"
    59   "raw document preparation text" K.thy_decl
    60   (P.comment >> (Toplevel.theory o IsarThy.add_text_raw));
    61 
    62 
    63 val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
    64   K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect)));
    65 
    66 val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
    67   K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect)));
    68 
    69 val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
    70   "formal comment (proof)" K.prf_heading
    71   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect)));
    72 
    73 val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
    74   K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
    75 
    76 val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw"
    77   "raw document preparation text (proof)" K.prf_decl
    78   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw)));
    79 
    80 
    81 
    82 (** theory sections **)
    83 
    84 (* classes and sorts *)
    85 
    86 val classesP =
    87   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    88     (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
    89       -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
    90 
    91 val classrelP =
    92   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    93     (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) -- P.marg_comment
    94       >> (Toplevel.theory o IsarThy.add_classrel));
    95 
    96 val defaultsortP =
    97   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    98     (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));
    99 
   100 
   101 (* types *)
   102 
   103 val typedeclP =
   104   OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
   105     (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
   106       Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
   107 
   108 val typeabbrP =
   109   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   110     (Scan.repeat1
   111       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment)
   112       >> (Toplevel.theory o IsarThy.add_tyabbrs o
   113         map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
   114 
   115 val nontermP =
   116   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   117     K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment)
   118       >> (Toplevel.theory o IsarThy.add_nonterminals));
   119 
   120 val aritiesP =
   121   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   122     (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment)
   123       >> (Toplevel.theory o IsarThy.add_arities));
   124 
   125 
   126 (* consts and syntax *)
   127 
   128 val judgmentP =
   129   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   130     (P.const -- P.marg_comment >> (Toplevel.theory o IsarThy.add_judgment));
   131 
   132 val constsP =
   133   OuterSyntax.command "consts" "declare constants" K.thy_decl
   134     (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
   135 
   136 
   137 val mode_spec = 
   138   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
   139 
   140 val opt_mode = Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) ("", true);
   141 
   142 val syntaxP =
   143   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   144     (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment)
   145       >> (Toplevel.theory o uncurry IsarThy.add_modesyntax));
   146 
   147 
   148 (* translations *)
   149 
   150 val trans_pat =
   151   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   152 
   153 fun trans_arrow toks =
   154   (P.$$$ "=>" >> K Syntax.ParseRule ||
   155     P.$$$ "<=" >> K Syntax.PrintRule ||
   156     P.$$$ "==" >> K Syntax.ParsePrintRule) toks;
   157 
   158 val trans_line =
   159   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   160     >> (fn (left, (arr, right)) => arr (left, right));
   161 
   162 val translationsP =
   163   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   164     (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules));
   165 
   166 
   167 (* axioms and definitions *)
   168 
   169 val axiomsP =
   170   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   171     (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
   172 
   173 val opt_overloaded =
   174   Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
   175 
   176 val defsP =
   177   OuterSyntax.command "defs" "define constants" K.thy_decl
   178     (opt_overloaded -- Scan.repeat1 (P.spec_name -- P.marg_comment)
   179   >> (Toplevel.theory o IsarThy.add_defs));
   180 
   181 val constdefsP =
   182   OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
   183     (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment))
   184       >> (Toplevel.theory o IsarThy.add_constdefs));
   185 
   186 
   187 (* theorems *)
   188 
   189 val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1 -- P.marg_comment);
   190 
   191 val theoremsP =
   192   OuterSyntax.command "theorems" "define theorems" K.thy_decl
   193     (name_facts >> (Toplevel.theory o IsarThy.have_theorems));
   194 
   195 val lemmasP =
   196   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   197     (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
   198 
   199 val declareP =
   200   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
   201     (P.xthms1 -- P.marg_comment >> (Toplevel.theory o IsarThy.declare_theorems));
   202 
   203 
   204 (* name space entry path *)
   205 
   206 val globalP =
   207   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   208     (P.marg_comment >> (Toplevel.theory o IsarThy.global_path));
   209 
   210 val localP =
   211   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   212     (P.marg_comment >> (Toplevel.theory o IsarThy.local_path));
   213 
   214 val hideP =
   215   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
   216     (P.name -- Scan.repeat1 P.xname -- P.marg_comment >> (Toplevel.theory o IsarThy.hide_space));
   217 
   218 
   219 (* use ML text *)
   220 
   221 val useP =
   222   OuterSyntax.command "use" "eval ML text from file" K.diag
   223     (P.name -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use));
   224 
   225 val mlP =
   226   OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
   227     (P.text -- P.marg_comment >> IsarCmd.use_mltext true);
   228 
   229 val ml_commandP =
   230   OuterSyntax.command "ML_command" "eval ML text" K.diag
   231     (P.text -- P.marg_comment >> IsarCmd.use_mltext false);
   232 
   233 val ml_setupP =
   234   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
   235     (P.text -- P.marg_comment >> IsarCmd.use_mltext_theory);
   236 
   237 val setupP =
   238   OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
   239     (P.text -- P.marg_comment >> (Toplevel.theory o IsarCmd.use_setup));
   240 
   241 val method_setupP =
   242   OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
   243     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2)
   244       -- P.marg_comment) >> (Toplevel.theory o IsarThy.method_setup));
   245 
   246 
   247 (* translation functions *)
   248 
   249 val parse_ast_translationP =
   250   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
   251     (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_ast_translation));
   252 
   253 val parse_translationP =
   254   OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
   255     (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_translation));
   256 
   257 val print_translationP =
   258   OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
   259     (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_translation));
   260 
   261 val typed_print_translationP =
   262   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   263     K.thy_decl (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.typed_print_translation));
   264 
   265 val print_ast_translationP =
   266   OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
   267     (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_ast_translation));
   268 
   269 val token_translationP =
   270   OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
   271     (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.token_translation));
   272 
   273 
   274 (* oracles *)
   275 
   276 val oracleP =
   277   OuterSyntax.command "oracle" "install oracle" K.thy_decl
   278     ((P.name --| P.$$$ "=") -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle));
   279 
   280 
   281 
   282 (** proof commands **)
   283 
   284 (* statements *)
   285 
   286 fun statement f = (P.opt_thm_name ":" -- P.propp >> P.triple1) -- P.marg_comment >> f;
   287 
   288 val theoremP =
   289   OuterSyntax.command "theorem" "state theorem" K.thy_goal
   290     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   291 
   292 val lemmaP =
   293   OuterSyntax.command "lemma" "state lemma" K.thy_goal
   294     (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   295 
   296 val showP =
   297   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
   298     (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   299 
   300 val haveP =
   301   OuterSyntax.command "have" "state local goal" K.prf_goal
   302     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   303 
   304 val thusP =
   305   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
   306     (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
   307 
   308 val henceP =
   309   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
   310     (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
   311 
   312 
   313 (* facts *)
   314 
   315 val facts = P.and_list1 (P.xthms1 -- P.marg_comment);
   316 
   317 val thenP =
   318   OuterSyntax.command "then" "forward chaining" K.prf_chain
   319     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
   320 
   321 val fromP =
   322   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   323     (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
   324 
   325 val withP =
   326   OuterSyntax.command "with" "forward chaining from given and current facts" K.prf_chain
   327     (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.with_facts)));
   328 
   329 val noteP =
   330   OuterSyntax.command "note" "define facts" K.prf_decl
   331     (name_facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
   332 
   333 
   334 (* proof context *)
   335 
   336 val assumeP =
   337   OuterSyntax.command "assume" "assume propositions" K.prf_asm
   338     (P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   339       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
   340 
   341 val presumeP =
   342   OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
   343     (P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   344       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
   345 
   346 val defP =
   347   OuterSyntax.command "def" "local definition" K.prf_asm
   348     ((P.opt_thm_name ":" -- (P.name -- (P.$$$ "==" |-- P.!!! P.termp)) >> P.triple1)
   349       -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
   350 
   351 val fixP =
   352   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
   353     (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   354       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
   355 
   356 val letP =
   357   OuterSyntax.command "let" "bind text variables" K.prf_decl
   358     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
   359       >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
   360 
   361 val caseP =
   362   OuterSyntax.command "case" "invoke local context" K.prf_asm
   363     (P.xthm -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
   364 
   365 
   366 (* proof structure *)
   367 
   368 val beginP =
   369   OuterSyntax.command "{" "begin explicit proof block" K.prf_open
   370     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block)));
   371 
   372 val endP =
   373   OuterSyntax.command "}" "end explicit proof block" K.prf_close
   374     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block)));
   375 
   376 val nextP =
   377   OuterSyntax.command "next" "enter next proof block" K.prf_block
   378     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.next_block)));
   379 
   380 
   381 (* end proof *)
   382 
   383 val qedP =
   384   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
   385     (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed);
   386 
   387 val terminal_proofP =
   388   OuterSyntax.command "by" "terminal backward proof" K.qed
   389     (P.method -- P.interest -- Scan.option (P.method -- P.interest)
   390       -- P.marg_comment >> IsarThy.terminal_proof);
   391 
   392 val default_proofP =
   393   OuterSyntax.command ".." "default proof" K.qed
   394     (P.marg_comment >> IsarThy.default_proof);
   395 
   396 val immediate_proofP =
   397   OuterSyntax.command "." "immediate proof" K.qed
   398     (P.marg_comment >> IsarThy.immediate_proof);
   399 
   400 val done_proofP =
   401   OuterSyntax.command "done" "done proof" K.qed
   402     (P.marg_comment >> IsarThy.done_proof);
   403 
   404 val skip_proofP =
   405   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
   406     (P.marg_comment >> IsarThy.skip_proof);
   407 
   408 val forget_proofP =
   409   OuterSyntax.command "oops" "forget proof" K.qed_global
   410     (P.marg_comment >> IsarThy.forget_proof);
   411 
   412 
   413 
   414 (* proof steps *)
   415 
   416 val deferP =
   417   OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script
   418     (Scan.option P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
   419 
   420 val preferP =
   421   OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script
   422     (P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
   423 
   424 val applyP =
   425   OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script
   426     (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
   427 
   428 val apply_endP =
   429   OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script
   430     (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
   431 
   432 val proofP =
   433   OuterSyntax.command "proof" "backward proof" K.prf_block
   434     (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
   435       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   436 
   437 
   438 (* calculational proof commands *)
   439 
   440 val calc_args =
   441   Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
   442 
   443 val alsoP =
   444   OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl
   445     (calc_args -- P.marg_comment >> IsarThy.also);
   446 
   447 val finallyP =
   448   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain
   449     (calc_args -- P.marg_comment >> IsarThy.finally);
   450 
   451 val moreoverP =
   452   OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
   453     (P.marg_comment >> IsarThy.moreover);
   454 
   455 val ultimatelyP =
   456   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
   457     K.prf_chain (P.marg_comment >> IsarThy.ultimately);
   458 
   459 
   460 (* proof navigation *)
   461 
   462 val backP =
   463   OuterSyntax.command "back" "backtracking of proof command" K.prf_script
   464     (Scan.optional (P.$$$ "!" >> K true) false -- P.marg_comment >>
   465       (Toplevel.print oo IsarCmd.back));
   466 
   467 
   468 (* history *)
   469 
   470 val cannot_undoP =
   471   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   472     (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
   473 
   474 val clear_undosP =
   475   OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
   476     (P.nat >> (Toplevel.no_timing oo IsarCmd.clear_undos_theory));
   477 
   478 val redoP =
   479   OuterSyntax.improper_command "redo" "redo last command" K.control
   480     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
   481 
   482 val undos_proofP =
   483   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   484     (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof));
   485 
   486 val undoP =
   487   OuterSyntax.improper_command "undo" "undo last command" K.control
   488     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo));
   489 
   490 val killP =
   491   OuterSyntax.improper_command "kill" "kill current history node" K.control
   492     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
   493 
   494 
   495 
   496 (** diagnostic commands (for interactive mode only) **)
   497 
   498 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   499 
   500 
   501 val pretty_setmarginP =
   502   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   503     K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   504 
   505 val print_commandsP =
   506   OuterSyntax.improper_command "print_commands" "print outer syntax (global)" K.diag
   507     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   508 
   509 val print_contextP =
   510   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
   511     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   512 
   513 val print_theoryP =
   514   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   515     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theory));
   516 
   517 val print_syntaxP =
   518   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
   519     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
   520 
   521 val print_theoremsP =
   522   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
   523     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
   524 
   525 val print_attributesP =
   526   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
   527     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   528 
   529 val print_trans_rulesP =
   530   OuterSyntax.improper_command "print_trans_rules" "print transitivity rules in this theory" K.diag
   531     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   532 
   533 val print_methodsP =
   534   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
   535     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
   536 
   537 val print_antiquotationsP =
   538   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
   539     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   540 
   541 val thms_containingP =
   542   OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
   543     K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
   544 
   545 val thm_depsP =
   546   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   547     K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   548 
   549 val print_bindsP =
   550   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   551     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   552 
   553 val print_lthmsP =
   554   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
   555     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_lthms));
   556 
   557 val print_casesP =
   558   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
   559     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   560 
   561 val print_thmsP =
   562   OuterSyntax.improper_command "thm" "print theorems" K.diag
   563     (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   564 
   565 val print_propP =
   566   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   567     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   568 
   569 val print_termP =
   570   OuterSyntax.improper_command "term" "read and print term" K.diag
   571     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   572 
   573 val print_typeP =
   574   OuterSyntax.improper_command "typ" "read and print type" K.diag
   575     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   576 
   577 
   578 
   579 (** system commands (for interactive mode only) **)
   580 
   581 val cdP =
   582   OuterSyntax.improper_command "cd" "change current working directory" K.diag
   583     (P.name >> (Toplevel.no_timing oo IsarCmd.cd));
   584 
   585 val pwdP =
   586   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   587     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   588 
   589 val use_thyP =
   590   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   591     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
   592 
   593 val use_thy_onlyP =
   594   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
   595     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
   596 
   597 val update_thyP =
   598   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   599     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
   600 
   601 val update_thy_onlyP =
   602   OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
   603     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
   604 
   605 val touch_thyP =
   606   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
   607     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
   608 
   609 val touch_all_thysP =
   610   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   611     (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
   612 
   613 val touch_child_thysP =
   614   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
   615     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
   616 
   617 val remove_thyP =
   618   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   619     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   620 
   621 val kill_thyP =
   622   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   623     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   624 
   625 val opt_limits =
   626   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   627 
   628 val prP =
   629   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
   630     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   631 
   632 val disable_prP =
   633   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   634     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   635 
   636 val enable_prP =
   637   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   638     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   639 
   640 val commitP =
   641   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   642     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
   643 
   644 val quitP =
   645   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   646     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   647 
   648 val exitP =
   649   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   650     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   651 
   652 val init_toplevelP =
   653   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
   654     (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
   655 
   656 val welcomeP =
   657   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
   658     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
   659 
   660 
   661 
   662 (** the Pure outer syntax **)
   663 
   664 (*keep keywords consistent with the parsers, including those in
   665   outer_parse.ML, otherwise be prepared for unexpected errors*)
   666 
   667 val keywords =
   668  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   669   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
   670   "files", "in", "infixl", "infixr", "is", "output", "overloaded", "|"];
   671 
   672 val parsers = [
   673   (*theory structure*)
   674   theoryP, end_excursionP, contextP,
   675   (*markup commands*)
   676   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   677   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   678   (*theory sections*)
   679   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   680   aritiesP, judgmentP, constsP, syntaxP, translationsP, axiomsP,
   681   defsP, constdefsP, theoremsP, lemmasP, declareP, globalP, localP,
   682   hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP,
   683   parse_ast_translationP, parse_translationP, print_translationP,
   684   typed_print_translationP, print_ast_translationP,
   685   token_translationP, oracleP,
   686   (*proof commands*)
   687   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   688   defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
   689   nextP, qedP, terminal_proofP, default_proofP, immediate_proofP,
   690   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   691   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   692   cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
   693   (*diagnostic commands*)
   694   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   695   print_syntaxP, print_theoremsP, print_attributesP,
   696   print_trans_rulesP, print_methodsP, print_antiquotationsP,
   697   thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
   698   print_casesP, print_thmsP, print_propP, print_termP, print_typeP,
   699   (*system commands*)
   700   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   701   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
   702   kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
   703   init_toplevelP, welcomeP];
   704 
   705 
   706 end;
   707 
   708 
   709 (*install the Pure outer syntax*)
   710 OuterSyntax.add_keywords IsarSyn.keywords;
   711 OuterSyntax.add_parsers IsarSyn.parsers;