Pure outer syntax.
authorwenzelm
Mon Nov 09 15:35:00 1998 +0100 (1998-11-09 ago)
changeset 5832112a67aa9c2c
parent 5831 996361157cfb
child 5833 6d8bceaa07b3
Pure outer syntax.
src/Pure/Isar/isar_syn.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 09 15:35:00 1998 +0100
     1.3 @@ -0,0 +1,496 @@
     1.4 +(*  Title:      Pure/Isar/isar_syn.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Pure outer syntax.
     1.9 +
    1.10 +TODO:
    1.11 +  - constdefs;
    1.12 +  - axclass axioms: attribs;
    1.13 +  - instance: theory_to_proof (with special attribute to add result arity);
    1.14 +  - witness: eliminate (!?);
    1.15 +  - result (interactive): print current result (?);
    1.16 +  - check evaluation of transformers (exns!);
    1.17 +  - print_thm: attributes;
    1.18 +  - 'result' command;
    1.19 +  - '--' (comment) option everywhere;
    1.20 +  - 'chapter', 'section' etc.;
    1.21 +*)
    1.22 +
    1.23 +signature ISAR_SYN =
    1.24 +sig
    1.25 +  val keywords: string list
    1.26 +  val parsers: OuterSyntax.parser list
    1.27 +end;
    1.28 +
    1.29 +structure IsarSyn: ISAR_SYN =
    1.30 +struct
    1.31 +
    1.32 +open OuterParse;
    1.33 +
    1.34 +
    1.35 +(** init and exit **)
    1.36 +
    1.37 +val contextP =
    1.38 +  OuterSyntax.parser false "context" "switch theory context"
    1.39 +    (name >> (fn x => Toplevel.print o Toplevel.init_theory (IsarThy.the_theory x) (K ())));
    1.40 +
    1.41 +val theoryP =
    1.42 +  OuterSyntax.parser false "theory" "begin theory"
    1.43 +    (name -- ($$$ "=" |-- !!! (enum "+" name --| (Scan.ahead eof || $$$ ":")))
    1.44 +      >> (fn x => Toplevel.print o
    1.45 +            Toplevel.init_theory (IsarThy.begin_theory x) IsarThy.end_theory));
    1.46 +
    1.47 +(*end current theory / sub-proof / excursion*)
    1.48 +val endP =
    1.49 +  OuterSyntax.parser false "end" "end current theory / sub-proof / excursion"
    1.50 +    (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
    1.51 +
    1.52 +
    1.53 +
    1.54 +(** theory sections **)
    1.55 +
    1.56 +(* formal comments *)
    1.57 +
    1.58 +val textP = OuterSyntax.parser false "text" "formal comments"
    1.59 +  (text >> K (Toplevel.keep (K ())));
    1.60 +
    1.61 +
    1.62 +(* classes and sorts *)
    1.63 +
    1.64 +val classesP =
    1.65 +  OuterSyntax.parser false "classes" "declare type classes"
    1.66 +    (Scan.repeat1 (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [])
    1.67 +      >> (Toplevel.theory o Theory.add_classes));
    1.68 +
    1.69 +val classrelP =
    1.70 +  OuterSyntax.parser false "classrel" "state inclusion of type classes (axiomatic!)"
    1.71 +    (xname -- ($$$ "<" |-- !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));
    1.72 +
    1.73 +val defaultsortP =
    1.74 +  OuterSyntax.parser false "defaultsort" "declare default sort"
    1.75 +    (sort >> (Toplevel.theory o Theory.add_defsort));
    1.76 +
    1.77 +
    1.78 +(* types *)
    1.79 +
    1.80 +val typedeclP =
    1.81 +  OuterSyntax.parser false "typedecl" "declare logical type"
    1.82 +    (type_args -- name -- opt_infix
    1.83 +      >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
    1.84 +
    1.85 +val typeabbrP =
    1.86 +  OuterSyntax.parser false "types" "declare type abbreviations"
    1.87 +    (Scan.repeat1 (type_args -- name -- ($$$ "=" |-- !!! (typ -- opt_infix)))
    1.88 +      >> (Toplevel.theory o Theory.add_tyabbrs o
    1.89 +        map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    1.90 +
    1.91 +val nontermP =
    1.92 +  OuterSyntax.parser false "nonterminals" "declare types treated as grammar nonterminal symbols"
    1.93 +    (Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));
    1.94 +
    1.95 +val aritiesP =
    1.96 +  OuterSyntax.parser false "arities" "state type arities (axiomatic!)"
    1.97 +    (Scan.repeat1 (xname -- ($$$ "::" |-- !!! arity) >> triple2)
    1.98 +      >> (Toplevel.theory o Theory.add_arities));
    1.99 +
   1.100 +
   1.101 +(* consts and syntax *)
   1.102 +
   1.103 +val constsP =
   1.104 +  OuterSyntax.parser false "consts" "declare constants"
   1.105 +    (Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));
   1.106 +
   1.107 +val opt_mode =
   1.108 +  Scan.optional
   1.109 +    ($$$ "(" |-- !!! (name -- Scan.optional ($$$ "output" >> K false) true --| $$$ ")"))
   1.110 +    ("", true);
   1.111 +
   1.112 +val syntaxP =
   1.113 +  OuterSyntax.parser false "syntax" "declare syntactic constants"
   1.114 +    (opt_mode -- Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   1.115 +
   1.116 +
   1.117 +(* translations *)
   1.118 +
   1.119 +val trans_pat =
   1.120 +  Scan.optional ($$$ "(" |-- !!! (xname --| $$$ ")")) "logic" -- string;
   1.121 +
   1.122 +fun trans_arrow toks =
   1.123 +  ($$$ "=>" >> K Syntax.ParseRule ||
   1.124 +    $$$ "<=" >> K Syntax.PrintRule ||
   1.125 +    $$$ "==" >> K Syntax.ParsePrintRule) toks;
   1.126 +
   1.127 +val trans_line =
   1.128 +  trans_pat -- !!! (trans_arrow -- trans_pat)
   1.129 +    >> (fn (left, (arr, right)) => arr (left, right));
   1.130 +
   1.131 +val translationsP =
   1.132 +  OuterSyntax.parser false "translations" "declare syntax translation rules"
   1.133 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   1.134 +
   1.135 +
   1.136 +(* axioms and definitions *)
   1.137 +
   1.138 +val spec = thm_name -- prop >> (fn ((x, y), z) => ((x, z), y));
   1.139 +val spec' = opt_thm_name -- prop >> (fn ((x, y), z) => ((x, z), y));
   1.140 +
   1.141 +val axiomsP =
   1.142 +  OuterSyntax.parser false "axioms" "state arbitrary propositions (axiomatic!)"
   1.143 +    (Scan.repeat1 spec >> (Toplevel.theory o IsarThy.add_axioms));
   1.144 +
   1.145 +val defsP =
   1.146 +  OuterSyntax.parser false "defs" "define constants"
   1.147 +    (Scan.repeat1 spec' >> (Toplevel.theory o IsarThy.add_defs));
   1.148 +
   1.149 +
   1.150 +(* axclass *)
   1.151 +
   1.152 +val axclassP =
   1.153 +  OuterSyntax.parser false "axclass" "define axiomatic type class"
   1.154 +    (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [] -- Scan.repeat (spec >> fst)
   1.155 +      >> (Toplevel.theory o uncurry AxClass.add_axclass));
   1.156 +
   1.157 +
   1.158 +(* instance *)
   1.159 +
   1.160 +val opt_witness =
   1.161 +  Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) [];
   1.162 +
   1.163 +val instanceP =
   1.164 +  OuterSyntax.parser false "instance" "prove type arity"
   1.165 +    ((xname -- ($$$ "<" |-- xname) >> AxClass.add_inst_subclass ||
   1.166 +      xname -- ($$$ "::" |-- arity) >> (AxClass.add_inst_arity o triple2))
   1.167 +    -- opt_witness >> (fn (f, x) => Toplevel.theory (f x [] None)));
   1.168 +
   1.169 +
   1.170 +(* name space entry path *)
   1.171 +
   1.172 +val globalP =
   1.173 +  OuterSyntax.parser false "global" "disable prefixing of theory name"
   1.174 +    (Scan.succeed (Toplevel.theory PureThy.global_path));
   1.175 +
   1.176 +val localP =
   1.177 +  OuterSyntax.parser false "local" "enable prefixing of theory name"
   1.178 +    (Scan.succeed (Toplevel.theory PureThy.local_path));
   1.179 +
   1.180 +val pathP =
   1.181 +  OuterSyntax.parser false "path" "modify name-space entry path"
   1.182 +    (xname >> (Toplevel.theory o Theory.add_path));
   1.183 +
   1.184 +
   1.185 +(* use ML text *)
   1.186 +
   1.187 +val useP =
   1.188 +  OuterSyntax.parser true "use" "eval ML text from file"
   1.189 +    (string >> IsarCmd.use);
   1.190 +
   1.191 +val mlP =
   1.192 +  OuterSyntax.parser false "ML" "eval ML text"
   1.193 +    (text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   1.194 +
   1.195 +val setupP =
   1.196 +  OuterSyntax.parser false "setup" "apply ML theory transformer"
   1.197 +    (text >> (Toplevel.theory o IsarThy.use_setup));
   1.198 +
   1.199 +
   1.200 +(* translation functions *)
   1.201 +
   1.202 +val parse_ast_translationP =
   1.203 +  OuterSyntax.parser false "parse_ast_translation" "install parse ast translation functions"
   1.204 +    (text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   1.205 +
   1.206 +val parse_translationP =
   1.207 +  OuterSyntax.parser false "parse_translation" "install parse translation functions"
   1.208 +    (text >> (Toplevel.theory o IsarThy.parse_translation));
   1.209 +
   1.210 +val print_translationP =
   1.211 +  OuterSyntax.parser false "print_translation" "install print translation functions"
   1.212 +    (text >> (Toplevel.theory o IsarThy.print_translation));
   1.213 +
   1.214 +val typed_print_translationP =
   1.215 +  OuterSyntax.parser false "typed_print_translation" "install typed print translation functions"
   1.216 +    (text >> (Toplevel.theory o IsarThy.typed_print_translation));
   1.217 +
   1.218 +val print_ast_translationP =
   1.219 +  OuterSyntax.parser false "print_ast_translation" "install print ast translation functions"
   1.220 +    (text >> (Toplevel.theory o IsarThy.print_ast_translation));
   1.221 +
   1.222 +val token_translationP =
   1.223 +  OuterSyntax.parser false "token_translation" "install token translation functions"
   1.224 +    (text >> (Toplevel.theory o IsarThy.token_translation));
   1.225 +
   1.226 +
   1.227 +(* oracles *)
   1.228 +
   1.229 +val oracleP =
   1.230 +  OuterSyntax.parser false "oracle" "install oracle"
   1.231 +    (name -- text >> (Toplevel.theory o IsarThy.add_oracle));
   1.232 +
   1.233 +
   1.234 +
   1.235 +(** proof commands **)
   1.236 +
   1.237 +(* statements *)
   1.238 +
   1.239 +fun statement f = opt_thm_name -- prop >> (fn ((x, y), z) => f x y z);
   1.240 +
   1.241 +val theoremP =
   1.242 +  OuterSyntax.parser false "theorem" "state theorem"
   1.243 +    (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   1.244 +
   1.245 +val lemmaP =
   1.246 +  OuterSyntax.parser false "lemma" "state lemma"
   1.247 +    (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   1.248 +
   1.249 +val showP =
   1.250 +  OuterSyntax.parser false "show" "state local goal, solving current obligation"
   1.251 +    (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   1.252 +
   1.253 +val haveP =
   1.254 +  OuterSyntax.parser false "have" "state local goal"
   1.255 +    (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   1.256 +
   1.257 +
   1.258 +(* forward chaining *)
   1.259 +
   1.260 +val thenP =
   1.261 +  OuterSyntax.parser false "then" "forward chaining"
   1.262 +    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
   1.263 +
   1.264 +val fromP =
   1.265 +  OuterSyntax.parser false "from" "forward chaining, from given facts"
   1.266 +    (enum1 "," xname >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   1.267 +
   1.268 +
   1.269 +(* proof context *)
   1.270 +
   1.271 +val assumeP =
   1.272 +  OuterSyntax.parser false "assume" "assume propositions"
   1.273 +    (opt_thm_name -- enum1 "," prop >>
   1.274 +      (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
   1.275 +
   1.276 +val fixP =
   1.277 +  OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
   1.278 +    (enum1 "," (name -- Scan.option ($$$ "::" |-- typ))
   1.279 +      >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
   1.280 +
   1.281 +val letP =
   1.282 +  OuterSyntax.parser false "let" "bind text variables"
   1.283 +    (enum1 "and" (term -- ($$$ "=" |-- term))
   1.284 +      >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
   1.285 +
   1.286 +
   1.287 +(* proof structure *)
   1.288 +
   1.289 +val beginP =
   1.290 +  OuterSyntax.parser false "begin" "begin block"
   1.291 +    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   1.292 +
   1.293 +val nextP =
   1.294 +  OuterSyntax.parser false "next" "enter next block"
   1.295 +    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   1.296 +
   1.297 +
   1.298 +(* end proof *)
   1.299 +
   1.300 +val qedP =
   1.301 +  OuterSyntax.parser false "qed" "conclude proof"
   1.302 +    (Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
   1.303 +
   1.304 +val qed_withP =
   1.305 +  OuterSyntax.parser true "qed_with" "conclude proof, may patch name and attributes"
   1.306 +    (Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
   1.307 +
   1.308 +val kill_proofP =
   1.309 +  OuterSyntax.parser true "kill" "abort current proof"
   1.310 +    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   1.311 +
   1.312 +
   1.313 +(* proof steps *)
   1.314 +
   1.315 +fun gen_stepP meth int name cmt f =
   1.316 +  OuterSyntax.parser int name cmt
   1.317 +    (meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));
   1.318 +
   1.319 +val stepP = gen_stepP method;
   1.320 +
   1.321 +val tacP = stepP true "tac" "unstructured backward proof step, ignoring facts" IsarThy.tac;
   1.322 +val etacP = stepP true "etac" "unstructured backward proof step, using facts" IsarThy.etac;
   1.323 +
   1.324 +
   1.325 +val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
   1.326 +val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
   1.327 +
   1.328 +val trivial_proofP =
   1.329 +  OuterSyntax.parser false "." "trivial proof"
   1.330 +    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.trivial_proof));
   1.331 +
   1.332 +val default_proofP =
   1.333 +  OuterSyntax.parser false ".." "default proof"
   1.334 +    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
   1.335 +
   1.336 +
   1.337 +(* proof history *)
   1.338 +
   1.339 +val clear_undoP =
   1.340 +  OuterSyntax.parser true "clear_undo" "clear proof command undo information"
   1.341 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));
   1.342 +
   1.343 +val undoP =
   1.344 +  OuterSyntax.parser true "undo" "undo proof command"
   1.345 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));
   1.346 +
   1.347 +val redoP =
   1.348 +  OuterSyntax.parser true "redo" "redo proof command"
   1.349 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));
   1.350 +
   1.351 +val backP =
   1.352 +  OuterSyntax.parser true "back" "backtracking of proof command"
   1.353 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   1.354 +
   1.355 +val prevP =
   1.356 +  OuterSyntax.parser true "prev" "previous proof state"
   1.357 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   1.358 +
   1.359 +val upP =
   1.360 +  OuterSyntax.parser true "up" "upper proof state"
   1.361 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   1.362 +
   1.363 +val topP =
   1.364 +  OuterSyntax.parser true "top" "to initial proof state"
   1.365 +    (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   1.366 +
   1.367 +
   1.368 +
   1.369 +(** diagnostic commands (for interactive mode only) **)
   1.370 +
   1.371 +val print_commandsP =
   1.372 +  OuterSyntax.parser true "help" "print outer syntax (global)"
   1.373 +    (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   1.374 +
   1.375 +val print_theoryP =
   1.376 +  OuterSyntax.parser true "print_theory" "print logical theory contents (verbose!)"
   1.377 +    (Scan.succeed IsarCmd.print_theory);
   1.378 +
   1.379 +val print_syntaxP =
   1.380 +  OuterSyntax.parser true "print_syntax" "print inner syntax of theory (verbose!)"
   1.381 +    (Scan.succeed IsarCmd.print_syntax);
   1.382 +
   1.383 +val print_attributesP =
   1.384 +  OuterSyntax.parser true "print_attributes" "print attributes known in theory"
   1.385 +    (Scan.succeed IsarCmd.print_attributes);
   1.386 +
   1.387 +val print_methodsP =
   1.388 +  OuterSyntax.parser true "print_methods" "print methods known in theory"
   1.389 +    (Scan.succeed IsarCmd.print_methods);
   1.390 +
   1.391 +val print_bindsP =
   1.392 +  OuterSyntax.parser true "print_binds" "print term bindings of proof context"
   1.393 +    (Scan.succeed IsarCmd.print_binds);
   1.394 +
   1.395 +val print_lthmsP =
   1.396 +  OuterSyntax.parser true "print_facts" "print local theorems of proof context"
   1.397 +    (Scan.succeed IsarCmd.print_lthms);
   1.398 +
   1.399 +val print_thmP =
   1.400 +  OuterSyntax.parser true "print_thm" "print stored theorem(s)"
   1.401 +    (xname >> IsarCmd.print_thms);
   1.402 +
   1.403 +val print_propP =
   1.404 +  OuterSyntax.parser true "print_prop" "read and print proposition"
   1.405 +    (term >> IsarCmd.print_prop);
   1.406 +
   1.407 +val print_termP =
   1.408 +  OuterSyntax.parser true "print_term" "read and print term"
   1.409 +    (term >> IsarCmd.print_term);
   1.410 +
   1.411 +val print_typeP =
   1.412 +  OuterSyntax.parser true "print_type" "read and print type"
   1.413 +    (typ >> IsarCmd.print_type);
   1.414 +
   1.415 +
   1.416 +
   1.417 +(** system commands (for interactive mode only) **)
   1.418 +
   1.419 +val cdP =
   1.420 +  OuterSyntax.parser true "cd" "change current working directory"
   1.421 +    (string >> IsarCmd.cd);
   1.422 +
   1.423 +val pwdP =
   1.424 +  OuterSyntax.parser true "pwd" "print current working directory"
   1.425 +    (Scan.succeed IsarCmd.pwd);
   1.426 +
   1.427 +val use_thyP =
   1.428 +  OuterSyntax.parser true "use_thy" "use_thy theory file"
   1.429 +    (string >> IsarCmd.use_thy);
   1.430 +
   1.431 +val loadP =
   1.432 +  OuterSyntax.parser true "load" "load theory file"
   1.433 +    (string >> IsarCmd.load);
   1.434 +
   1.435 +val prP =
   1.436 +  OuterSyntax.parser true "pr" "print current toplevel state"
   1.437 +    (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   1.438 +
   1.439 +
   1.440 +val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   1.441 +
   1.442 +val commitP =
   1.443 +  OuterSyntax.parser true "commit" "commit current session to ML database"
   1.444 +    (opt_unit >> (K IsarCmd.use_commit));
   1.445 +
   1.446 +val quitP =
   1.447 +  OuterSyntax.parser true "quit" "quit Isabelle"
   1.448 +    (opt_unit >> (K IsarCmd.quit));
   1.449 +
   1.450 +val exitP =
   1.451 +  OuterSyntax.parser true "exit" "exit Isar loop"
   1.452 +    (Scan.succeed IsarCmd.exit);
   1.453 +
   1.454 +val breakP =
   1.455 +  OuterSyntax.parser true "break" "discontinue execution"
   1.456 +    (Scan.succeed IsarCmd.break);
   1.457 +
   1.458 +
   1.459 +
   1.460 +(** the Pure outer syntax **)
   1.461 +
   1.462 +(*keep keywords consistent with the parsers, including those in
   1.463 +  outer_parse.ML, otherwise be prepared for unexpected errors*)
   1.464 +
   1.465 +val keywords =
   1.466 + ["(", ")", "*", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
   1.467 +  "?", "[", "]", "and", "binder", "infixl", "infixr", "mixfix", "output",
   1.468 +  "{", "|", "}"];
   1.469 +
   1.470 +val parsers = [
   1.471 +  (*theory structure*)
   1.472 +  contextP, theoryP, endP,
   1.473 +  (*theory sections*)
   1.474 +  textP, classesP, classrelP, defaultsortP, typedeclP, typeabbrP,
   1.475 +  nontermP, aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   1.476 +  axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,
   1.477 +  parse_ast_translationP, parse_translationP, print_translationP,
   1.478 +  typed_print_translationP, print_ast_translationP,
   1.479 +  token_translationP, oracleP,
   1.480 +  (*proof commands*)
   1.481 +  theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
   1.482 +  beginP, nextP, qedP, qed_withP, kill_proofP, tacP, etacP, proofP,
   1.483 +  terminal_proofP, trivial_proofP, default_proofP, clear_undoP, undoP,
   1.484 +  redoP, backP, prevP, upP, topP,
   1.485 +  (*diagnostic commands*)
   1.486 +  print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   1.487 +  print_methodsP, print_bindsP, print_lthmsP, print_thmP, print_propP,
   1.488 +  print_termP, print_typeP,
   1.489 +  (*system commands*)
   1.490 +  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
   1.491 +
   1.492 +
   1.493 +end;
   1.494 +
   1.495 +
   1.496 +(* install the Pure outer syntax *)
   1.497 +
   1.498 +OuterSyntax.add_keywords IsarSyn.keywords;
   1.499 +OuterSyntax.add_parsers IsarSyn.parsers;