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