src/Pure/Isar/isar_syn.ML
author wenzelm
Fri Jul 02 15:04:45 1999 +0200 (1999-07-02 ago)
changeset 6886 7d0f7ad5a35f
parent 6878 1e97e7fbcca5
child 6888 d0c68ebdabc5
permissions -rw-r--r--
added 'txt';
     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 
   359 (* proof steps *)
   360 
   361 val applyP =
   362   OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
   363     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   364 
   365 val then_applyP =
   366   OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
   367     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   368 
   369 val proofP =
   370   OuterSyntax.command "proof" "backward proof" K.prf_block
   371     (P.interest -- Scan.option (P.method -- P.interest)
   372       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   373 
   374 
   375 (* calculational proof commands *)
   376 
   377 val calc_args =
   378   Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
   379 
   380 val alsoP =
   381   OuterSyntax.command "also" "intermediate calculational proof step" K.prf_decl
   382     (calc_args -- P.marg_comment >> IsarThy.also);
   383 
   384 val finallyP =
   385   OuterSyntax.command "finally" "terminal calculational proof step" K.prf_chain
   386     (calc_args -- P.marg_comment >> IsarThy.finally);
   387 
   388 
   389 (* proof navigation *)
   390 
   391 val backP =
   392   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
   393     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   394 
   395 val prevP =
   396   OuterSyntax.improper_command "prev" "previous proof state" K.control
   397     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   398 
   399 val upP =
   400   OuterSyntax.improper_command "up" "upper proof state" K.control
   401     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   402 
   403 val topP =
   404   OuterSyntax.improper_command "top" "to initial proof state" K.control
   405     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   406 
   407 
   408 (* history *)
   409 
   410 val cannot_undoP =
   411   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   412     (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
   413 
   414 val clear_undoP =
   415   OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
   416     (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
   417 
   418 val redoP =
   419   OuterSyntax.improper_command "redo" "redo last command" K.control
   420     (Scan.succeed (Toplevel.print o IsarCmd.redo));
   421 
   422 val undos_proofP =
   423   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   424     (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
   425 
   426 val kill_proofP =
   427   OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
   428     (Scan.succeed (Toplevel.print o IsarCmd.kill_proof));
   429 
   430 val undoP =
   431   OuterSyntax.improper_command "undo" "undo last command" K.control
   432     (Scan.succeed (Toplevel.print o IsarCmd.undo));
   433 
   434 
   435 
   436 (** diagnostic commands (for interactive mode only) **)
   437 
   438 val print_commandsP =
   439   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
   440     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   441 
   442 val print_theoryP =
   443   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   444     (Scan.succeed IsarCmd.print_theory);
   445 
   446 val print_syntaxP =
   447   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
   448     (Scan.succeed IsarCmd.print_syntax);
   449 
   450 val print_theoremsP =
   451   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
   452     (Scan.succeed IsarCmd.print_theorems);
   453 
   454 val print_attributesP =
   455   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
   456     (Scan.succeed IsarCmd.print_attributes);
   457 
   458 val print_methodsP =
   459   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
   460     (Scan.succeed IsarCmd.print_methods);
   461 
   462 val print_bindsP =
   463   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   464     (Scan.succeed IsarCmd.print_binds);
   465 
   466 val print_lthmsP =
   467   OuterSyntax.improper_command "print_facts" "print local theorems of proof context" K.diag
   468     (Scan.succeed IsarCmd.print_lthms);
   469 
   470 val print_thmsP =
   471   OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms);
   472 
   473 val print_propP =
   474   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   475     (P.term >> IsarCmd.print_prop);
   476 
   477 val print_termP =
   478   OuterSyntax.improper_command "term" "read and print term" K.diag
   479     (P.term >> IsarCmd.print_term);
   480 
   481 val print_typeP =
   482   OuterSyntax.improper_command "typ" "read and print type" K.diag
   483     (P.typ >> IsarCmd.print_type);
   484 
   485 
   486 
   487 (** system commands (for interactive mode only) **)
   488 
   489 val cdP =
   490   OuterSyntax.improper_command "cd" "change current working directory" K.control
   491     (P.name >> IsarCmd.cd);
   492 
   493 val pwdP =
   494   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   495     (Scan.succeed IsarCmd.pwd);
   496 
   497 val use_thyP =
   498   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   499     (P.name >> IsarCmd.use_thy);
   500 
   501 val use_thy_onlyP =
   502   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" K.diag
   503     (P.name >> IsarCmd.use_thy_only);
   504 
   505 val update_thyP =
   506   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   507     (P.name >> IsarCmd.update_thy);
   508 
   509 val prP =
   510   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   511     (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   512 
   513 
   514 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   515 
   516 val commitP =
   517   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   518     (opt_unit >> (K IsarCmd.use_commit));
   519 
   520 val quitP =
   521   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   522     (opt_unit >> (K IsarCmd.quit));
   523 
   524 val exitP =
   525   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   526     (Scan.succeed IsarCmd.exit);
   527 
   528 val restartP =
   529   OuterSyntax.improper_command "restart" "restart Isar loop" K.control
   530     (Scan.succeed IsarCmd.restart);
   531 
   532 val breakP =
   533   OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
   534     (Scan.succeed IsarCmd.break);
   535 
   536 
   537 
   538 (** the Pure outer syntax **)
   539 
   540 (*keep keywords consistent with the parsers, including those in
   541   outer_parse.ML, otherwise be prepared for unexpected errors*)
   542 
   543 val keywords =
   544  ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
   545   "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
   546   "infixl", "infixr", "is", "output", "{", "|", "}"];
   547 
   548 val parsers = [
   549   (*theory structure*)
   550   theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
   551   (*theory sections*)
   552   txtP, textP, titleP, chapterP, sectionP, subsectionP,
   553   subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
   554   typeabbrP, nontermP, aritiesP, constsP, syntaxP, translationsP,
   555   axiomsP, defsP, constdefsP, theoremsP, lemmasP, globalP, localP,
   556   pathP, useP, mlP, setupP, parse_ast_translationP,
   557   parse_translationP, print_translationP, typed_print_translationP,
   558   print_ast_translationP, token_translationP, oracleP,
   559   (*proof commands*)
   560   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   561   fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
   562   qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   563   applyP, then_applyP, proofP, alsoP, finallyP, backP, prevP, upP,
   564   topP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP,
   565   undoP,
   566   (*diagnostic commands*)
   567   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   568   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   569   print_thmsP, print_propP, print_termP, print_typeP,
   570   (*system commands*)
   571   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
   572   quitP, exitP, restartP, breakP];
   573 
   574 
   575 end;
   576 
   577 
   578 (*install the Pure outer syntax*)
   579 OuterSyntax.add_keywords IsarSyn.keywords;
   580 OuterSyntax.add_parsers IsarSyn.parsers;