src/Pure/Isar/isar_syn.ML
author wenzelm
Fri Jul 02 19:04:32 1999 +0200 (1999-07-02 ago)
changeset 6888 d0c68ebdabc5
parent 6886 7d0f7ad5a35f
child 6890 05732285677e
permissions -rw-r--r--
skip_proof feature 'sorry' (for quick_and_dirty mode only);
     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 signature ISAR_SYN =
     9 sig
    10   val keywords: string list
    11   val parsers: OuterSyntax.parser list
    12 end;
    13 
    14 structure IsarSyn: ISAR_SYN =
    15 struct
    16 
    17 structure P = OuterParse and K = OuterSyntax.Keyword;
    18 
    19 
    20 (** init and exit **)
    21 
    22 val theoryP =
    23   OuterSyntax.command "theory" "begin theory" K.thy_begin
    24     (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
    25 
    26 val end_excursionP =
    27   OuterSyntax.command "end" "end current excursion" K.thy_end
    28     (Scan.succeed (Toplevel.print o Toplevel.exit));
    29 
    30 val kill_excursionP =
    31   OuterSyntax.improper_command "kill" "kill current excursion" K.control
    32     (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
    33 
    34 val contextP =
    35   OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
    36     (P.name >> (Toplevel.print oo IsarThy.context));
    37 
    38 val update_contextP =
    39   OuterSyntax.improper_command "update_context" "switch theory context, forcing update" K.thy_begin
    40     (P.name >> (Toplevel.print oo IsarThy.update_context));
    41 
    42 
    43 
    44 (** formal comments **)
    45 
    46 val txtP = OuterSyntax.command "txt" "formal comment (proof)" K.prf_decl
    47   (P.comment >> (Toplevel.proof o IsarThy.add_txt));
    48 
    49 val textP = OuterSyntax.command "text" "formal comment (theory)" K.thy_decl
    50   (P.comment >> (Toplevel.theory o IsarThy.add_text));
    51 
    52 val titleP = OuterSyntax.command "title" "document title" K.thy_heading
    53   ((P.comment -- Scan.optional P.comment Comment.none -- Scan.optional P.comment Comment.none)
    54     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    55 
    56 val chapterP = OuterSyntax.command "chapter" "chapter heading" K.thy_heading
    57   (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
    58 
    59 val sectionP = OuterSyntax.command "section" "section heading" K.thy_heading
    60   (P.comment >> (Toplevel.theory o IsarThy.add_section));
    61 
    62 val subsectionP = OuterSyntax.command "subsection" "subsection heading" K.thy_heading
    63   (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
    64 
    65 val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading" K.thy_heading
    66   (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    67 
    68 
    69 
    70 (** theory sections **)
    71 
    72 (* classes and sorts *)
    73 
    74 val classesP =
    75   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    76     (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
    77       -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
    78 
    79 val classrelP =
    80   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    81     (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) -- P.marg_comment
    82       >> (Toplevel.theory o IsarThy.add_classrel));
    83 
    84 val defaultsortP =
    85   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    86     (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));
    87 
    88 
    89 (* types *)
    90 
    91 val typedeclP =
    92   OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
    93     (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
    94       Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
    95 
    96 val typeabbrP =
    97   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    98     (Scan.repeat1
    99       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)) -- P.marg_comment)
   100       >> (Toplevel.theory o IsarThy.add_tyabbrs o
   101         map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
   102 
   103 val nontermP =
   104   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   105     K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment)
   106       >> (Toplevel.theory o IsarThy.add_nonterminals));
   107 
   108 val aritiesP =
   109   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   110     (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment)
   111       >> (Toplevel.theory o IsarThy.add_arities));
   112 
   113 
   114 (* consts and syntax *)
   115 
   116 val constsP =
   117   OuterSyntax.command "consts" "declare constants" K.thy_decl
   118     (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
   119 
   120 val opt_mode =
   121   Scan.optional
   122     (P.$$$ "(" |-- P.!!! (P.name -- Scan.optional (P.$$$ "output" >> K false) true --| P.$$$ ")"))
   123     ("", true);
   124 
   125 val syntaxP =
   126   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   127     (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment)
   128       >> (Toplevel.theory o uncurry IsarThy.add_modesyntax));
   129 
   130 
   131 (* translations *)
   132 
   133 val trans_pat =
   134   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   135 
   136 fun trans_arrow toks =
   137   (P.$$$ "=>" >> K Syntax.ParseRule ||
   138     P.$$$ "<=" >> K Syntax.PrintRule ||
   139     P.$$$ "==" >> K Syntax.ParsePrintRule) toks;
   140 
   141 val trans_line =
   142   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   143     >> (fn (left, (arr, right)) => arr (left, right));
   144 
   145 val translationsP =
   146   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   147     (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules));
   148 
   149 
   150 (* axioms and definitions *)
   151 
   152 val axiomsP =
   153   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   154     (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
   155 
   156 val defsP =
   157   OuterSyntax.command "defs" "define constants" K.thy_decl
   158     (Scan.repeat1 (P.spec_opt_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_defs));
   159 
   160 val constdefsP =
   161   OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
   162     (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment))
   163       >> (Toplevel.theory o IsarThy.add_constdefs));
   164 
   165 
   166 (* theorems *)
   167 
   168 val facts = P.opt_thm_name "=" -- P.xthms1;
   169 
   170 val theoremsP =
   171   OuterSyntax.command "theorems" "define theorems" K.thy_decl
   172     (facts -- P.marg_comment >> (Toplevel.theory o IsarThy.have_theorems));
   173 
   174 val lemmasP =
   175   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   176     (facts -- P.marg_comment >> (Toplevel.theory o IsarThy.have_lemmas));
   177 
   178 
   179 (* name space entry path *)
   180 
   181 val globalP =
   182   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   183     (Scan.succeed (Toplevel.theory PureThy.global_path));
   184 
   185 val localP =
   186   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   187     (Scan.succeed (Toplevel.theory PureThy.local_path));
   188 
   189 val pathP =
   190   OuterSyntax.command "path" "modify name-space entry path" K.thy_decl
   191     (P.xname >> (Toplevel.theory o Theory.add_path));
   192 
   193 
   194 (* use ML text *)
   195 
   196 val useP =
   197   OuterSyntax.command "use" "eval ML text from file" K.diag
   198     (P.name >> IsarCmd.use);
   199 
   200 val mlP =
   201   OuterSyntax.command "ML" "eval ML text" K.diag
   202     (P.text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   203 
   204 val setupP =
   205   OuterSyntax.command "setup" "apply ML theory transformer" K.thy_decl
   206     (P.text >> (Toplevel.theory o IsarThy.use_setup));
   207 
   208 
   209 (* translation functions *)
   210 
   211 val parse_ast_translationP =
   212   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
   213     (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   214 
   215 val parse_translationP =
   216   OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
   217     (P.text >> (Toplevel.theory o IsarThy.parse_translation));
   218 
   219 val print_translationP =
   220   OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
   221     (P.text >> (Toplevel.theory o IsarThy.print_translation));
   222 
   223 val typed_print_translationP =
   224   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   225     K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
   226 
   227 val print_ast_translationP =
   228   OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
   229     (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
   230 
   231 val token_translationP =
   232   OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
   233     (P.text >> (Toplevel.theory o IsarThy.token_translation));
   234 
   235 
   236 (* oracles *)
   237 
   238 val oracleP =
   239   OuterSyntax.command "oracle" "install oracle" K.thy_decl
   240     (P.name -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle));
   241 
   242 
   243 
   244 (** proof commands **)
   245 
   246 (* statements *)
   247 
   248 val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
   249 val propp = P.prop -- Scan.optional is_props [];
   250 fun statement f = (P.opt_thm_name ":" -- propp >> P.triple1) -- P.marg_comment >> f;
   251 
   252 val theoremP =
   253   OuterSyntax.command "theorem" "state theorem" K.thy_goal
   254     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   255 
   256 val lemmaP =
   257   OuterSyntax.command "lemma" "state lemma" K.thy_goal
   258     (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   259 
   260 val showP =
   261   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
   262     (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   263 
   264 val haveP =
   265   OuterSyntax.command "have" "state local goal" K.prf_goal
   266     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   267 
   268 val thusP =
   269   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
   270     (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
   271 
   272 val henceP =
   273   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
   274     (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
   275 
   276 
   277 (* facts *)
   278 
   279 val thenP =
   280   OuterSyntax.command "then" "forward chaining" K.prf_chain
   281     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
   282 
   283 val fromP =
   284   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   285     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
   286 
   287 val withP =
   288   OuterSyntax.command "with" "forward chaining from given and current facts" K.prf_chain
   289     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.with_facts)));
   290 
   291 val noteP =
   292   OuterSyntax.command "note" "define facts" K.prf_decl
   293     (facts -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
   294 
   295 
   296 (* proof context *)
   297 
   298 val assumeP =
   299   OuterSyntax.command "assume" "assume propositions" K.prf_asm
   300     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
   301       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
   302 
   303 val presumeP =
   304   OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
   305     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
   306       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
   307 
   308 val fixP =
   309   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
   310     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
   311       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
   312 
   313 val letP =
   314   OuterSyntax.command "let" "bind text variables" K.prf_decl
   315     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
   316       >> (Toplevel.print oo (Toplevel.proof o IsarThy.match_bind)));
   317 
   318 
   319 (* proof structure *)
   320 
   321 val beginP =
   322   OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
   323     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   324 
   325 val endP =
   326   OuterSyntax.command "}}" "end explicit proof block" K.prf_block
   327     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
   328 
   329 val nextP =
   330   OuterSyntax.command "next" "enter next proof block" K.prf_block
   331     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   332 
   333 
   334 (* end proof *)
   335 
   336 val qed_withP =
   337   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
   338     K.qed_block
   339     (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
   340       >> (uncurry IsarThy.global_qed_with));
   341 
   342 val qedP =
   343   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
   344     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
   345 
   346 val terminal_proofP =
   347   OuterSyntax.command "by" "terminal backward proof" K.qed
   348     (P.method -- P.interest >> IsarThy.terminal_proof);
   349 
   350 val immediate_proofP =
   351   OuterSyntax.command "." "immediate proof" K.qed
   352     (Scan.succeed IsarThy.immediate_proof);
   353 
   354 val default_proofP =
   355   OuterSyntax.command ".." "default proof" K.qed
   356     (Scan.succeed IsarThy.default_proof);
   357 
   358 val skip_proofP =
   359   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
   360     (Scan.succeed IsarThy.skip_proof);
   361 
   362 
   363 (* proof steps *)
   364 
   365 val applyP =
   366   OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
   367     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   368 
   369 val then_applyP =
   370   OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
   371     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   372 
   373 val proofP =
   374   OuterSyntax.command "proof" "backward proof" K.prf_block
   375     (P.interest -- Scan.option (P.method -- P.interest)
   376       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   377 
   378 
   379 (* calculational proof commands *)
   380 
   381 val calc_args =
   382   Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
   383 
   384 val alsoP =
   385   OuterSyntax.command "also" "intermediate calculational proof step" K.prf_decl
   386     (calc_args -- P.marg_comment >> IsarThy.also);
   387 
   388 val finallyP =
   389   OuterSyntax.command "finally" "terminal calculational proof step" K.prf_chain
   390     (calc_args -- P.marg_comment >> IsarThy.finally);
   391 
   392 
   393 (* proof navigation *)
   394 
   395 val backP =
   396   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
   397     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   398 
   399 val prevP =
   400   OuterSyntax.improper_command "prev" "previous proof state" K.control
   401     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   402 
   403 val upP =
   404   OuterSyntax.improper_command "up" "upper proof state" K.control
   405     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   406 
   407 val topP =
   408   OuterSyntax.improper_command "top" "to initial proof state" K.control
   409     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   410 
   411 
   412 (* history *)
   413 
   414 val cannot_undoP =
   415   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   416     (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
   417 
   418 val clear_undoP =
   419   OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
   420     (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
   421 
   422 val redoP =
   423   OuterSyntax.improper_command "redo" "redo last command" K.control
   424     (Scan.succeed (Toplevel.print o IsarCmd.redo));
   425 
   426 val undos_proofP =
   427   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   428     (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
   429 
   430 val kill_proofP =
   431   OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
   432     (Scan.succeed (Toplevel.print o IsarCmd.kill_proof));
   433 
   434 val undoP =
   435   OuterSyntax.improper_command "undo" "undo last command" K.control
   436     (Scan.succeed (Toplevel.print o IsarCmd.undo));
   437 
   438 
   439 
   440 (** diagnostic commands (for interactive mode only) **)
   441 
   442 val print_commandsP =
   443   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
   444     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   445 
   446 val print_theoryP =
   447   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   448     (Scan.succeed IsarCmd.print_theory);
   449 
   450 val print_syntaxP =
   451   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
   452     (Scan.succeed IsarCmd.print_syntax);
   453 
   454 val print_theoremsP =
   455   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
   456     (Scan.succeed IsarCmd.print_theorems);
   457 
   458 val print_attributesP =
   459   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
   460     (Scan.succeed IsarCmd.print_attributes);
   461 
   462 val print_methodsP =
   463   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
   464     (Scan.succeed IsarCmd.print_methods);
   465 
   466 val print_bindsP =
   467   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   468     (Scan.succeed IsarCmd.print_binds);
   469 
   470 val print_lthmsP =
   471   OuterSyntax.improper_command "print_facts" "print local theorems of proof context" K.diag
   472     (Scan.succeed IsarCmd.print_lthms);
   473 
   474 val print_thmsP =
   475   OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms);
   476 
   477 val print_propP =
   478   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   479     (P.term >> IsarCmd.print_prop);
   480 
   481 val print_termP =
   482   OuterSyntax.improper_command "term" "read and print term" K.diag
   483     (P.term >> IsarCmd.print_term);
   484 
   485 val print_typeP =
   486   OuterSyntax.improper_command "typ" "read and print type" K.diag
   487     (P.typ >> IsarCmd.print_type);
   488 
   489 
   490 
   491 (** system commands (for interactive mode only) **)
   492 
   493 val cdP =
   494   OuterSyntax.improper_command "cd" "change current working directory" K.control
   495     (P.name >> IsarCmd.cd);
   496 
   497 val pwdP =
   498   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   499     (Scan.succeed IsarCmd.pwd);
   500 
   501 val use_thyP =
   502   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   503     (P.name >> IsarCmd.use_thy);
   504 
   505 val use_thy_onlyP =
   506   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" K.diag
   507     (P.name >> IsarCmd.use_thy_only);
   508 
   509 val update_thyP =
   510   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   511     (P.name >> IsarCmd.update_thy);
   512 
   513 val prP =
   514   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   515     (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   516 
   517 
   518 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   519 
   520 val commitP =
   521   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   522     (opt_unit >> (K IsarCmd.use_commit));
   523 
   524 val quitP =
   525   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   526     (opt_unit >> (K IsarCmd.quit));
   527 
   528 val exitP =
   529   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   530     (Scan.succeed IsarCmd.exit);
   531 
   532 val restartP =
   533   OuterSyntax.improper_command "restart" "restart Isar loop" K.control
   534     (Scan.succeed IsarCmd.restart);
   535 
   536 val breakP =
   537   OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
   538     (Scan.succeed IsarCmd.break);
   539 
   540 
   541 
   542 (** the Pure outer syntax **)
   543 
   544 (*keep keywords consistent with the parsers, including those in
   545   outer_parse.ML, otherwise be prepared for unexpected errors*)
   546 
   547 val keywords =
   548  ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
   549   "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
   550   "infixl", "infixr", "is", "output", "{", "|", "}"];
   551 
   552 val parsers = [
   553   (*theory structure*)
   554   theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
   555   (*theory sections*)
   556   txtP, textP, titleP, chapterP, sectionP, subsectionP,
   557   subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
   558   typeabbrP, nontermP, aritiesP, constsP, syntaxP, translationsP,
   559   axiomsP, defsP, constdefsP, theoremsP, lemmasP, globalP, localP,
   560   pathP, useP, mlP, setupP, parse_ast_translationP,
   561   parse_translationP, print_translationP, typed_print_translationP,
   562   print_ast_translationP, token_translationP, oracleP,
   563   (*proof commands*)
   564   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   565   fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
   566   qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   567   skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
   568   prevP, upP, topP, cannot_undoP, clear_undoP, redoP, undos_proofP,
   569   kill_proofP, undoP,
   570   (*diagnostic commands*)
   571   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   572   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   573   print_thmsP, print_propP, print_termP, print_typeP,
   574   (*system commands*)
   575   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
   576   quitP, exitP, restartP, breakP];
   577 
   578 
   579 end;
   580 
   581 
   582 (*install the Pure outer syntax*)
   583 OuterSyntax.add_keywords IsarSyn.keywords;
   584 OuterSyntax.add_parsers IsarSyn.parsers;