src/Pure/Isar/isar_syn.ML
author wenzelm
Mon Jul 12 10:02:38 1999 +0200 (1999-07-12 ago)
changeset 6972 3ae2eeabde80
parent 6953 b3f6c39aaa2e
child 7002 01a4e15ee253
permissions -rw-r--r--
def: ==;
     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.print oo (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 fun statement f = (P.opt_thm_name ":" -- P.propp >> P.triple1) -- P.marg_comment >> f;
   249 
   250 val theoremP =
   251   OuterSyntax.command "theorem" "state theorem" K.thy_goal
   252     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   253 
   254 val lemmaP =
   255   OuterSyntax.command "lemma" "state lemma" K.thy_goal
   256     (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   257 
   258 val showP =
   259   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
   260     (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   261 
   262 val haveP =
   263   OuterSyntax.command "have" "state local goal" K.prf_goal
   264     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   265 
   266 val thusP =
   267   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
   268     (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
   269 
   270 val henceP =
   271   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
   272     (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
   273 
   274 
   275 (* facts *)
   276 
   277 val thenP =
   278   OuterSyntax.command "then" "forward chaining" K.prf_chain
   279     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
   280 
   281 val thenceP =
   282   OuterSyntax.command "thence" "forward chaining, including full export" K.prf_chain
   283     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.export_chain)));
   284 
   285 val fromP =
   286   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   287     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
   288 
   289 val withP =
   290   OuterSyntax.command "with" "forward chaining from given and current facts" K.prf_chain
   291     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.with_facts)));
   292 
   293 val noteP =
   294   OuterSyntax.command "note" "define facts" K.prf_decl
   295     (facts -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
   296 
   297 
   298 (* proof context *)
   299 
   300 val assumeP =
   301   OuterSyntax.command "assume" "assume propositions" K.prf_asm
   302     ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
   303       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
   304 
   305 val presumeP =
   306   OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
   307     ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment
   308       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
   309 
   310 val defP =
   311   OuterSyntax.command "def" "local definition" K.prf_asm
   312     ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
   313       (P.$$$ "==" |-- P.termp)) >> P.triple1) -- P.marg_comment
   314       >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
   315 
   316 val fixP =
   317   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
   318     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
   319       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
   320 
   321 val letP =
   322   OuterSyntax.command "let" "bind text variables" K.prf_decl
   323     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
   324       >> (Toplevel.print oo (Toplevel.proof o IsarThy.match_bind)));
   325 
   326 
   327 (* proof structure *)
   328 
   329 val beginP =
   330   OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
   331     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   332 
   333 val endP =
   334   OuterSyntax.command "}}" "end explicit proof block" K.prf_block
   335     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
   336 
   337 val nextP =
   338   OuterSyntax.command "next" "enter next proof block" K.prf_block
   339     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   340 
   341 
   342 (* end proof *)
   343 
   344 val qedP =
   345   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
   346     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
   347 
   348 val terminal_proofP =
   349   OuterSyntax.command "by" "terminal backward proof" K.qed
   350     (P.method -- P.interest -- Scan.option (P.method -- P.interest) >> IsarThy.terminal_proof);
   351 
   352 val immediate_proofP =
   353   OuterSyntax.command "." "immediate proof" K.qed
   354     (Scan.succeed IsarThy.immediate_proof);
   355 
   356 val default_proofP =
   357   OuterSyntax.command ".." "default proof" K.qed
   358     (Scan.succeed IsarThy.default_proof);
   359 
   360 val skip_proofP =
   361   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
   362     (Scan.succeed IsarThy.skip_proof);
   363 
   364 
   365 (* proof steps *)
   366 
   367 val applyP =
   368   OuterSyntax.improper_command "apply" "unstructured backward proof step, ignoring facts"
   369     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   370 
   371 val then_applyP =
   372   OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
   373     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   374 
   375 val proofP =
   376   OuterSyntax.command "proof" "backward proof" K.prf_block
   377     (P.interest -- Scan.option (P.method -- P.interest)
   378       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   379 
   380 
   381 (* calculational proof commands *)
   382 
   383 val calc_args =
   384   Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest));
   385 
   386 val alsoP =
   387   OuterSyntax.command "also" "intermediate calculational proof step" K.prf_decl
   388     (calc_args -- P.marg_comment >> IsarThy.also);
   389 
   390 val finallyP =
   391   OuterSyntax.command "finally" "terminal calculational proof step" K.prf_chain
   392     (calc_args -- P.marg_comment >> IsarThy.finally);
   393 
   394 
   395 (* proof navigation *)
   396 
   397 val backP =
   398   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
   399     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   400 
   401 
   402 (* history *)
   403 
   404 val cannot_undoP =
   405   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   406     (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
   407 
   408 val clear_undoP =
   409   OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
   410     (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
   411 
   412 val redoP =
   413   OuterSyntax.improper_command "redo" "redo last command" K.control
   414     (Scan.succeed (Toplevel.print o IsarCmd.redo));
   415 
   416 val undos_proofP =
   417   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   418     (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
   419 
   420 val kill_proofP =
   421   OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
   422     (Scan.succeed (Toplevel.print o IsarCmd.kill_proof));
   423 
   424 val undoP =
   425   OuterSyntax.improper_command "undo" "undo last command" K.control
   426     (Scan.succeed (Toplevel.print o IsarCmd.undo));
   427 
   428 
   429 
   430 (** diagnostic commands (for interactive mode only) **)
   431 
   432 val print_commandsP =
   433   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
   434     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   435 
   436 val print_theoryP =
   437   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   438     (Scan.succeed IsarCmd.print_theory);
   439 
   440 val print_syntaxP =
   441   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
   442     (Scan.succeed IsarCmd.print_syntax);
   443 
   444 val print_theoremsP =
   445   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
   446     (Scan.succeed IsarCmd.print_theorems);
   447 
   448 val print_attributesP =
   449   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
   450     (Scan.succeed IsarCmd.print_attributes);
   451 
   452 val print_methodsP =
   453   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
   454     (Scan.succeed IsarCmd.print_methods);
   455 
   456 val print_bindsP =
   457   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   458     (Scan.succeed IsarCmd.print_binds);
   459 
   460 val print_lthmsP =
   461   OuterSyntax.improper_command "print_facts" "print local theorems of proof context" K.diag
   462     (Scan.succeed IsarCmd.print_lthms);
   463 
   464 val print_thmsP =
   465   OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms);
   466 
   467 val print_propP =
   468   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   469     (P.term >> IsarCmd.print_prop);
   470 
   471 val print_termP =
   472   OuterSyntax.improper_command "term" "read and print term" K.diag
   473     (P.term >> IsarCmd.print_term);
   474 
   475 val print_typeP =
   476   OuterSyntax.improper_command "typ" "read and print type" K.diag
   477     (P.typ >> IsarCmd.print_type);
   478 
   479 
   480 
   481 (** system commands (for interactive mode only) **)
   482 
   483 val cdP =
   484   OuterSyntax.improper_command "cd" "change current working directory" K.control
   485     (P.name >> IsarCmd.cd);
   486 
   487 val pwdP =
   488   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   489     (Scan.succeed IsarCmd.pwd);
   490 
   491 val use_thyP =
   492   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   493     (P.name >> IsarCmd.use_thy);
   494 
   495 val use_thy_onlyP =
   496   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" K.diag
   497     (P.name >> IsarCmd.use_thy_only);
   498 
   499 val update_thyP =
   500   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   501     (P.name >> IsarCmd.update_thy);
   502 
   503 val prP =
   504   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   505     (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   506 
   507 
   508 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   509 
   510 val commitP =
   511   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   512     (opt_unit >> (K IsarCmd.use_commit));
   513 
   514 val quitP =
   515   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   516     (opt_unit >> (K IsarCmd.quit));
   517 
   518 val exitP =
   519   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   520     (Scan.succeed IsarCmd.exit);
   521 
   522 val restartP =
   523   OuterSyntax.improper_command "restart" "restart Isar loop" K.control
   524     (Scan.succeed IsarCmd.restart);
   525 
   526 val breakP =
   527   OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
   528     (Scan.succeed IsarCmd.break);
   529 
   530 
   531 
   532 (** the Pure outer syntax **)
   533 
   534 (*keep keywords consistent with the parsers, including those in
   535   outer_parse.ML, otherwise be prepared for unexpected errors*)
   536 
   537 val keywords =
   538  ["!", "!!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<",
   539   "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
   540   "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
   541   "}"];
   542 
   543 val parsers = [
   544   (*theory structure*)
   545   theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
   546   (*theory sections*)
   547   txtP, textP, titleP, chapterP, sectionP, subsectionP,
   548   subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
   549   typeabbrP, nontermP, aritiesP, constsP, syntaxP, translationsP,
   550   axiomsP, defsP, constdefsP, theoremsP, lemmasP, globalP, localP,
   551   pathP, useP, mlP, setupP, parse_ast_translationP,
   552   parse_translationP, print_translationP, typed_print_translationP,
   553   print_ast_translationP, token_translationP, oracleP,
   554   (*proof commands*)
   555   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   556   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   557   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
   558   skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
   559   cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   560   (*diagnostic commands*)
   561   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   562   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   563   print_thmsP, print_propP, print_termP, print_typeP,
   564   (*system commands*)
   565   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
   566   quitP, exitP, restartP, breakP];
   567 
   568 
   569 end;
   570 
   571 
   572 (*install the Pure outer syntax*)
   573 OuterSyntax.add_keywords IsarSyn.keywords;
   574 OuterSyntax.add_parsers IsarSyn.parsers;