OuterSyntax.(improper_)command;
authorwenzelm
Wed Mar 17 13:34:49 1999 +0100 (1999-03-17 ago)
changeset 6370e71ac23a9111
parent 6369 2be75edfe58c
child 6371 8469852acbc0
OuterSyntax.(improper_)command;
moved axclass / instance to Pure/axclass.ML;
moved spec(') to outer_parse.ML;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Mar 17 13:33:13 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 17 13:34:49 1999 +0100
     1.3 @@ -5,16 +5,11 @@
     1.4  Isar/Pure outer syntax.
     1.5  
     1.6  TODO:
     1.7 +  - '--' (comment) option almost everywhere:
     1.8    - add_parsers: warn if command name coincides with other keyword (if
     1.9      not already present) (!?);
    1.10 -  - constdefs;
    1.11 -  - axclass axioms: attribs;
    1.12 -  - instance: theory_to_proof (with special attribute to add result arity);
    1.13 -  - witness: eliminate (!);
    1.14 -  - result (interactive): print current result (?);
    1.15 +  - 'result' (interactive): print current result (?);
    1.16    - check evaluation of transformers (exns!);
    1.17 -  - 'result' command;
    1.18 -  - '--' (comment) option almost everywhere:
    1.19    - 'thms': xthms1 (vs. 'thm' (!?));
    1.20  *)
    1.21  
    1.22 @@ -33,20 +28,20 @@
    1.23  (** init and exit **)
    1.24  
    1.25  val theoryP =
    1.26 -  OuterSyntax.parser false "theory" "begin theory"
    1.27 +  OuterSyntax.command "theory" "begin theory"
    1.28      (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
    1.29  
    1.30  (*end current theory / sub-proof / excursion*)
    1.31  val endP =
    1.32 -  OuterSyntax.parser false "end" "end current theory / sub-proof / excursion"
    1.33 +  OuterSyntax.command "end" "end current theory / sub-proof / excursion"
    1.34      (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
    1.35  
    1.36  val contextP =
    1.37 -  OuterSyntax.parser true "context" "switch theory context"
    1.38 +  OuterSyntax.improper_command "context" "switch theory context"
    1.39      (name >> (Toplevel.print oo IsarThy.context));
    1.40  
    1.41  val update_contextP =
    1.42 -  OuterSyntax.parser true "update_context" "switch theory context, forcing update"
    1.43 +  OuterSyntax.improper_command "update_context" "switch theory context, forcing update"
    1.44      (name >> (Toplevel.print oo IsarThy.update_context));
    1.45  
    1.46  
    1.47 @@ -55,61 +50,61 @@
    1.48  
    1.49  (* formal comments *)
    1.50  
    1.51 -val textP = OuterSyntax.parser false "text" "formal comments"
    1.52 +val textP = OuterSyntax.command "text" "formal comments"
    1.53    (text >> (Toplevel.theory o IsarThy.add_text));
    1.54  
    1.55 -val titleP = OuterSyntax.parser false "title" "document title"
    1.56 +val titleP = OuterSyntax.command "title" "document title"
    1.57    ((text -- Scan.optional text "" -- Scan.optional text "")
    1.58      >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    1.59  
    1.60 -val chapterP = OuterSyntax.parser false "chapter" "chapter heading"
    1.61 +val chapterP = OuterSyntax.command "chapter" "chapter heading"
    1.62    (text >> (Toplevel.theory o IsarThy.add_chapter));
    1.63  
    1.64 -val sectionP = OuterSyntax.parser false "section" "section heading"
    1.65 +val sectionP = OuterSyntax.command "section" "section heading"
    1.66    (text >> (Toplevel.theory o IsarThy.add_section));
    1.67  
    1.68 -val subsectionP = OuterSyntax.parser false "subsection" "subsection heading"
    1.69 +val subsectionP = OuterSyntax.command "subsection" "subsection heading"
    1.70    (text >> (Toplevel.theory o IsarThy.add_subsection));
    1.71  
    1.72 -val subsubsectionP = OuterSyntax.parser false "subsubsection" "subsubsection heading"
    1.73 +val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
    1.74    (text >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.75  
    1.76  
    1.77  (* classes and sorts *)
    1.78  
    1.79  val classesP =
    1.80 -  OuterSyntax.parser false "classes" "declare type classes"
    1.81 +  OuterSyntax.command "classes" "declare type classes"
    1.82      (Scan.repeat1 (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [])
    1.83        >> (Toplevel.theory o Theory.add_classes));
    1.84  
    1.85  val classrelP =
    1.86 -  OuterSyntax.parser false "classrel" "state inclusion of type classes (axiomatic!)"
    1.87 +  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)"
    1.88      (xname -- ($$$ "<" |-- !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));
    1.89  
    1.90  val defaultsortP =
    1.91 -  OuterSyntax.parser false "defaultsort" "declare default sort"
    1.92 +  OuterSyntax.command "defaultsort" "declare default sort"
    1.93      (sort >> (Toplevel.theory o Theory.add_defsort));
    1.94  
    1.95  
    1.96  (* types *)
    1.97  
    1.98  val typedeclP =
    1.99 -  OuterSyntax.parser false "typedecl" "Pure type declaration"
   1.100 +  OuterSyntax.command "typedecl" "Pure type declaration"
   1.101      (type_args -- name -- opt_infix
   1.102        >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
   1.103  
   1.104  val typeabbrP =
   1.105 -  OuterSyntax.parser false "types" "declare type abbreviations"
   1.106 +  OuterSyntax.command "types" "declare type abbreviations"
   1.107      (Scan.repeat1 (type_args -- name -- ($$$ "=" |-- !!! (typ -- opt_infix)))
   1.108        >> (Toplevel.theory o Theory.add_tyabbrs o
   1.109          map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   1.110  
   1.111  val nontermP =
   1.112 -  OuterSyntax.parser false "nonterminals" "declare types treated as grammar nonterminal symbols"
   1.113 +  OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   1.114      (Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));
   1.115  
   1.116  val aritiesP =
   1.117 -  OuterSyntax.parser false "arities" "state type arities (axiomatic!)"
   1.118 +  OuterSyntax.command "arities" "state type arities (axiomatic!)"
   1.119      (Scan.repeat1 (xname -- ($$$ "::" |-- !!! arity) >> triple2)
   1.120        >> (Toplevel.theory o Theory.add_arities));
   1.121  
   1.122 @@ -117,7 +112,7 @@
   1.123  (* consts and syntax *)
   1.124  
   1.125  val constsP =
   1.126 -  OuterSyntax.parser false "consts" "declare constants"
   1.127 +  OuterSyntax.command "consts" "declare constants"
   1.128      (Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));
   1.129  
   1.130  val opt_mode =
   1.131 @@ -126,7 +121,7 @@
   1.132      ("", true);
   1.133  
   1.134  val syntaxP =
   1.135 -  OuterSyntax.parser false "syntax" "declare syntactic constants"
   1.136 +  OuterSyntax.command "syntax" "declare syntactic constants"
   1.137      (opt_mode -- Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   1.138  
   1.139  
   1.140 @@ -145,22 +140,23 @@
   1.141      >> (fn (left, (arr, right)) => arr (left, right));
   1.142  
   1.143  val translationsP =
   1.144 -  OuterSyntax.parser false "translations" "declare syntax translation rules"
   1.145 +  OuterSyntax.command "translations" "declare syntax translation rules"
   1.146      (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   1.147  
   1.148  
   1.149  (* axioms and definitions *)
   1.150  
   1.151 -val spec = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
   1.152 -val spec' = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
   1.153 -
   1.154  val axiomsP =
   1.155 -  OuterSyntax.parser false "axioms" "state arbitrary propositions (axiomatic!)"
   1.156 -    (Scan.repeat1 spec >> (Toplevel.theory o IsarThy.add_axioms));
   1.157 +  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)"
   1.158 +    (Scan.repeat1 spec_name >> (Toplevel.theory o IsarThy.add_axioms));
   1.159  
   1.160  val defsP =
   1.161 -  OuterSyntax.parser false "defs" "define constants"
   1.162 -    (Scan.repeat1 spec' >> (Toplevel.theory o IsarThy.add_defs));
   1.163 +  OuterSyntax.command "defs" "define constants"
   1.164 +    (Scan.repeat1 spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
   1.165 +
   1.166 +val constdefsP =
   1.167 +  OuterSyntax.command "constdefs" "declare and define constants"
   1.168 +    (Scan.repeat1 (const -- term) >> (Toplevel.theory o IsarThy.add_constdefs));
   1.169  
   1.170  
   1.171  (* theorems *)
   1.172 @@ -168,95 +164,75 @@
   1.173  val facts = opt_thm_name "=" -- xthms1;
   1.174  
   1.175  val theoremsP =
   1.176 -  OuterSyntax.parser false "theorems" "define theorems"
   1.177 +  OuterSyntax.command "theorems" "define theorems"
   1.178      (facts >> (Toplevel.theory o IsarThy.have_theorems));
   1.179  
   1.180  val lemmasP =
   1.181 -  OuterSyntax.parser false "lemmas" "define lemmas"
   1.182 +  OuterSyntax.command "lemmas" "define lemmas"
   1.183      (facts >> (Toplevel.theory o IsarThy.have_lemmas));
   1.184  
   1.185  
   1.186 -(* axclass *)
   1.187 -
   1.188 -val axclassP =
   1.189 -  OuterSyntax.parser false "axclass" "define axiomatic type class"
   1.190 -    (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [] -- Scan.repeat (spec >> fst)
   1.191 -      >> (Toplevel.theory o uncurry AxClass.add_axclass));
   1.192 -
   1.193 -
   1.194 -(* instance *)
   1.195 -
   1.196 -val opt_witness =
   1.197 -  Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) [];
   1.198 -
   1.199 -val instanceP =
   1.200 -  OuterSyntax.parser false "instance" "prove type arity"
   1.201 -    ((xname -- ($$$ "<" |-- xname) >> AxClass.add_inst_subclass ||
   1.202 -      xname -- ($$$ "::" |-- arity) >> (AxClass.add_inst_arity o triple2))
   1.203 -    -- opt_witness >> (fn (f, x) => Toplevel.theory (f x [] None)));
   1.204 -
   1.205 -
   1.206  (* name space entry path *)
   1.207  
   1.208  val globalP =
   1.209 -  OuterSyntax.parser false "global" "disable prefixing of theory name"
   1.210 +  OuterSyntax.command "global" "disable prefixing of theory name"
   1.211      (Scan.succeed (Toplevel.theory PureThy.global_path));
   1.212  
   1.213  val localP =
   1.214 -  OuterSyntax.parser false "local" "enable prefixing of theory name"
   1.215 +  OuterSyntax.command "local" "enable prefixing of theory name"
   1.216      (Scan.succeed (Toplevel.theory PureThy.local_path));
   1.217  
   1.218  val pathP =
   1.219 -  OuterSyntax.parser false "path" "modify name-space entry path"
   1.220 +  OuterSyntax.command "path" "modify name-space entry path"
   1.221      (xname >> (Toplevel.theory o Theory.add_path));
   1.222  
   1.223  
   1.224  (* use ML text *)
   1.225  
   1.226  val useP =
   1.227 -  OuterSyntax.parser false "use" "eval ML text from file"
   1.228 +  OuterSyntax.command "use" "eval ML text from file"
   1.229      (name >> IsarCmd.use);
   1.230  
   1.231  val mlP =
   1.232 -  OuterSyntax.parser false "ML" "eval ML text"
   1.233 +  OuterSyntax.command "ML" "eval ML text"
   1.234      (text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   1.235  
   1.236  val setupP =
   1.237 -  OuterSyntax.parser false "setup" "apply ML theory transformer"
   1.238 +  OuterSyntax.command "setup" "apply ML theory transformer"
   1.239      (text >> (Toplevel.theory o IsarThy.use_setup));
   1.240  
   1.241  
   1.242  (* translation functions *)
   1.243  
   1.244  val parse_ast_translationP =
   1.245 -  OuterSyntax.parser false "parse_ast_translation" "install parse ast translation functions"
   1.246 +  OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   1.247      (text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   1.248  
   1.249  val parse_translationP =
   1.250 -  OuterSyntax.parser false "parse_translation" "install parse translation functions"
   1.251 +  OuterSyntax.command "parse_translation" "install parse translation functions"
   1.252      (text >> (Toplevel.theory o IsarThy.parse_translation));
   1.253  
   1.254  val print_translationP =
   1.255 -  OuterSyntax.parser false "print_translation" "install print translation functions"
   1.256 +  OuterSyntax.command "print_translation" "install print translation functions"
   1.257      (text >> (Toplevel.theory o IsarThy.print_translation));
   1.258  
   1.259  val typed_print_translationP =
   1.260 -  OuterSyntax.parser false "typed_print_translation" "install typed print translation functions"
   1.261 +  OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   1.262      (text >> (Toplevel.theory o IsarThy.typed_print_translation));
   1.263  
   1.264  val print_ast_translationP =
   1.265 -  OuterSyntax.parser false "print_ast_translation" "install print ast translation functions"
   1.266 +  OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   1.267      (text >> (Toplevel.theory o IsarThy.print_ast_translation));
   1.268  
   1.269  val token_translationP =
   1.270 -  OuterSyntax.parser false "token_translation" "install token translation functions"
   1.271 +  OuterSyntax.command "token_translation" "install token translation functions"
   1.272      (text >> (Toplevel.theory o IsarThy.token_translation));
   1.273  
   1.274  
   1.275  (* oracles *)
   1.276  
   1.277  val oracleP =
   1.278 -  OuterSyntax.parser false "oracle" "install oracle"
   1.279 +  OuterSyntax.command "oracle" "install oracle"
   1.280      (name -- text >> (Toplevel.theory o IsarThy.add_oracle));
   1.281  
   1.282  
   1.283 @@ -270,51 +246,51 @@
   1.284  fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
   1.285  
   1.286  val theoremP =
   1.287 -  OuterSyntax.parser false "theorem" "state theorem"
   1.288 +  OuterSyntax.command "theorem" "state theorem"
   1.289      (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   1.290  
   1.291  val lemmaP =
   1.292 -  OuterSyntax.parser false "lemma" "state lemma"
   1.293 +  OuterSyntax.command "lemma" "state lemma"
   1.294      (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   1.295  
   1.296  val showP =
   1.297 -  OuterSyntax.parser false "show" "state local goal, solving current obligation"
   1.298 +  OuterSyntax.command "show" "state local goal, solving current obligation"
   1.299      (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   1.300  
   1.301  val haveP =
   1.302 -  OuterSyntax.parser false "have" "state local goal"
   1.303 +  OuterSyntax.command "have" "state local goal"
   1.304      (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   1.305  
   1.306  
   1.307  (* facts *)
   1.308  
   1.309  val thenP =
   1.310 -  OuterSyntax.parser false "then" "forward chaining"
   1.311 +  OuterSyntax.command "then" "forward chaining"
   1.312      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
   1.313  
   1.314  val fromP =
   1.315 -  OuterSyntax.parser false "from" "forward chaining from given facts"
   1.316 +  OuterSyntax.command "from" "forward chaining from given facts"
   1.317      (xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   1.318  
   1.319  val factsP =
   1.320 -  OuterSyntax.parser false "note" "define facts"
   1.321 +  OuterSyntax.command "note" "define facts"
   1.322      (facts >> (Toplevel.proof o IsarThy.have_facts));
   1.323  
   1.324  
   1.325  (* proof context *)
   1.326  
   1.327  val assumeP =
   1.328 -  OuterSyntax.parser false "assume" "assume propositions"
   1.329 -    (opt_thm_name ":" -- and_list1 propp >>
   1.330 +  OuterSyntax.command "assume" "assume propositions"
   1.331 +    (opt_thm_name ":" -- Scan.repeat1 propp >>
   1.332        (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
   1.333  
   1.334  val fixP =
   1.335 -  OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
   1.336 -    (and_list1 (name -- Scan.option ($$$ "::" |-- typ))
   1.337 +  OuterSyntax.command "fix" "fix variables (Skolem constants)"
   1.338 +    (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
   1.339        >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
   1.340  
   1.341  val letP =
   1.342 -  OuterSyntax.parser false "let" "bind text variables"
   1.343 +  OuterSyntax.command "let" "bind text variables"
   1.344      (and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
   1.345        >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
   1.346  
   1.347 @@ -322,26 +298,26 @@
   1.348  (* proof structure *)
   1.349  
   1.350  val beginP =
   1.351 -  OuterSyntax.parser false "begin" "begin block"
   1.352 +  OuterSyntax.command "begin" "begin block"
   1.353      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   1.354  
   1.355  val nextP =
   1.356 -  OuterSyntax.parser false "next" "enter next block"
   1.357 +  OuterSyntax.command "next" "enter next block"
   1.358      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   1.359  
   1.360  
   1.361  (* end proof *)
   1.362  
   1.363  val qedP =
   1.364 -  OuterSyntax.parser false "qed" "conclude proof"
   1.365 +  OuterSyntax.command "qed" "conclude proof"
   1.366      (Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
   1.367  
   1.368  val qed_withP =
   1.369 -  OuterSyntax.parser true "qed_with" "conclude proof, may patch name and attributes"
   1.370 +  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
   1.371      (Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
   1.372  
   1.373  val kill_proofP =
   1.374 -  OuterSyntax.parser true "kill" "abort current proof"
   1.375 +  OuterSyntax.improper_command "kill" "abort current proof"
   1.376      (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   1.377  
   1.378  
   1.379 @@ -362,50 +338,50 @@
   1.380  val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
   1.381  
   1.382  val immediate_proofP =
   1.383 -  OuterSyntax.parser false "." "immediate proof"
   1.384 +  OuterSyntax.command "." "immediate proof"
   1.385      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
   1.386  
   1.387  val default_proofP =
   1.388 -  OuterSyntax.parser false ".." "default proof"
   1.389 +  OuterSyntax.command ".." "default proof"
   1.390      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
   1.391  
   1.392  
   1.393  (* proof history *)
   1.394  
   1.395  val clear_undoP =
   1.396 -  OuterSyntax.parser true "clear_undo" "clear proof command undo information"
   1.397 +  OuterSyntax.improper_command "clear_undo" "clear proof command undo information"
   1.398      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));
   1.399  
   1.400  val undoP =
   1.401 -  OuterSyntax.parser true "undo" "undo proof command"
   1.402 +  OuterSyntax.improper_command "undo" "undo proof command"
   1.403      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));
   1.404  
   1.405  val redoP =
   1.406 -  OuterSyntax.parser true "redo" "redo proof command"
   1.407 +  OuterSyntax.improper_command "redo" "redo proof command"
   1.408      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));
   1.409  
   1.410  val undosP =
   1.411 -  OuterSyntax.parser true "undos" "undo proof commands"
   1.412 +  OuterSyntax.improper_command "undos" "undo proof commands"
   1.413      (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.undos n)));
   1.414  
   1.415  val redosP =
   1.416 -  OuterSyntax.parser true "redos" "redo proof commands"
   1.417 +  OuterSyntax.improper_command "redos" "redo proof commands"
   1.418      (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.redos n)));
   1.419  
   1.420  val backP =
   1.421 -  OuterSyntax.parser true "back" "backtracking of proof command"
   1.422 +  OuterSyntax.improper_command "back" "backtracking of proof command"
   1.423      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   1.424  
   1.425  val prevP =
   1.426 -  OuterSyntax.parser true "prev" "previous proof state"
   1.427 +  OuterSyntax.improper_command "prev" "previous proof state"
   1.428      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   1.429  
   1.430  val upP =
   1.431 -  OuterSyntax.parser true "up" "upper proof state"
   1.432 +  OuterSyntax.improper_command "up" "upper proof state"
   1.433      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   1.434  
   1.435  val topP =
   1.436 -  OuterSyntax.parser true "top" "to initial proof state"
   1.437 +  OuterSyntax.improper_command "top" "to initial proof state"
   1.438      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   1.439  
   1.440  
   1.441 @@ -413,50 +389,50 @@
   1.442  (** diagnostic commands (for interactive mode only) **)
   1.443  
   1.444  val print_commandsP =
   1.445 -  OuterSyntax.parser true "help" "print outer syntax (global)"
   1.446 +  OuterSyntax.improper_command "help" "print outer syntax (global)"
   1.447      (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   1.448  
   1.449  val print_theoryP =
   1.450 -  OuterSyntax.parser true "print_theory" "print logical theory contents (verbose!)"
   1.451 +  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
   1.452      (Scan.succeed IsarCmd.print_theory);
   1.453  
   1.454  val print_syntaxP =
   1.455 -  OuterSyntax.parser true "print_syntax" "print inner syntax of theory (verbose!)"
   1.456 +  OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)"
   1.457      (Scan.succeed IsarCmd.print_syntax);
   1.458  
   1.459  val print_theoremsP =
   1.460 -  OuterSyntax.parser true "print_theorems" "print theorems known in this theory"
   1.461 +  OuterSyntax.improper_command "print_theorems" "print theorems known in this theory"
   1.462      (Scan.succeed IsarCmd.print_theorems);
   1.463  
   1.464  val print_attributesP =
   1.465 -  OuterSyntax.parser true "print_attributes" "print attributes known in this theory"
   1.466 +  OuterSyntax.improper_command "print_attributes" "print attributes known in this theory"
   1.467      (Scan.succeed IsarCmd.print_attributes);
   1.468  
   1.469  val print_methodsP =
   1.470 -  OuterSyntax.parser true "print_methods" "print methods known in this theory"
   1.471 +  OuterSyntax.improper_command "print_methods" "print methods known in this theory"
   1.472      (Scan.succeed IsarCmd.print_methods);
   1.473  
   1.474  val print_bindsP =
   1.475 -  OuterSyntax.parser true "print_binds" "print term bindings of proof context"
   1.476 +  OuterSyntax.improper_command "print_binds" "print term bindings of proof context"
   1.477      (Scan.succeed IsarCmd.print_binds);
   1.478  
   1.479  val print_lthmsP =
   1.480 -  OuterSyntax.parser true "print_facts" "print local theorems of proof context"
   1.481 +  OuterSyntax.improper_command "print_facts" "print local theorems of proof context"
   1.482      (Scan.succeed IsarCmd.print_lthms);
   1.483  
   1.484  val print_thmsP =
   1.485 -  OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms);
   1.486 +  OuterSyntax.improper_command "thm" "print theorems" (xthm >> IsarCmd.print_thms);
   1.487  
   1.488  val print_propP =
   1.489 -  OuterSyntax.parser true "prop" "read and print proposition"
   1.490 +  OuterSyntax.improper_command "prop" "read and print proposition"
   1.491      (term >> IsarCmd.print_prop);
   1.492  
   1.493  val print_termP =
   1.494 -  OuterSyntax.parser true "term" "read and print term"
   1.495 +  OuterSyntax.improper_command "term" "read and print term"
   1.496      (term >> IsarCmd.print_term);
   1.497  
   1.498  val print_typeP =
   1.499 -  OuterSyntax.parser true "type" "read and print type"
   1.500 +  OuterSyntax.improper_command "type" "read and print type"
   1.501      (typ >> IsarCmd.print_type);
   1.502  
   1.503  
   1.504 @@ -464,46 +440,46 @@
   1.505  (** system commands (for interactive mode only) **)
   1.506  
   1.507  val cdP =
   1.508 -  OuterSyntax.parser true "cd" "change current working directory"
   1.509 +  OuterSyntax.improper_command "cd" "change current working directory"
   1.510      (name >> IsarCmd.cd);
   1.511  
   1.512  val pwdP =
   1.513 -  OuterSyntax.parser true "pwd" "print current working directory"
   1.514 +  OuterSyntax.improper_command "pwd" "print current working directory"
   1.515      (Scan.succeed IsarCmd.pwd);
   1.516  
   1.517  val use_thyP =
   1.518 -  OuterSyntax.parser true "use_thy" "use theory file"
   1.519 +  OuterSyntax.improper_command "use_thy" "use theory file"
   1.520      (name >> IsarCmd.use_thy);
   1.521  
   1.522  val update_thyP =
   1.523 -  OuterSyntax.parser true "update_thy" "update theory file"
   1.524 +  OuterSyntax.improper_command "update_thy" "update theory file"
   1.525      (name >> IsarCmd.update_thy);
   1.526  
   1.527  val prP =
   1.528 -  OuterSyntax.parser true "pr" "print current toplevel state"
   1.529 +  OuterSyntax.improper_command "pr" "print current toplevel state"
   1.530      (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   1.531  
   1.532  
   1.533  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   1.534  
   1.535  val commitP =
   1.536 -  OuterSyntax.parser true "commit" "commit current session to ML database"
   1.537 +  OuterSyntax.improper_command "commit" "commit current session to ML database"
   1.538      (opt_unit >> (K IsarCmd.use_commit));
   1.539  
   1.540  val quitP =
   1.541 -  OuterSyntax.parser true "quit" "quit Isabelle"
   1.542 +  OuterSyntax.improper_command "quit" "quit Isabelle"
   1.543      (opt_unit >> (K IsarCmd.quit));
   1.544  
   1.545  val exitP =
   1.546 -  OuterSyntax.parser true "exit" "exit Isar loop"
   1.547 +  OuterSyntax.improper_command "exit" "exit Isar loop"
   1.548      (Scan.succeed IsarCmd.exit);
   1.549  
   1.550  val restartP =
   1.551 -  OuterSyntax.parser true "restart" "restart Isar loop"
   1.552 +  OuterSyntax.improper_command "restart" "restart Isar loop"
   1.553      (Scan.succeed IsarCmd.restart);
   1.554  
   1.555  val breakP =
   1.556 -  OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
   1.557 +  OuterSyntax.improper_command "break" "discontinue excursion (keep current state)"
   1.558      (Scan.succeed IsarCmd.break);
   1.559  
   1.560  
   1.561 @@ -522,13 +498,13 @@
   1.562    (*theory structure*)
   1.563    theoryP, endP, contextP, update_contextP,
   1.564    (*theory sections*)
   1.565 -  textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,
   1.566 -  classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,
   1.567 -  constsP, syntaxP, translationsP, axiomsP, defsP, theoremsP, lemmasP,
   1.568 -  axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,
   1.569 -  parse_ast_translationP, parse_translationP, print_translationP,
   1.570 -  typed_print_translationP, print_ast_translationP,
   1.571 -  token_translationP, oracleP,
   1.572 +  textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP,
   1.573 +  classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   1.574 +  aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   1.575 +  constdefsP, theoremsP, lemmasP, globalP, localP, pathP, useP, mlP,
   1.576 +  setupP, parse_ast_translationP, parse_translationP,
   1.577 +  print_translationP, typed_print_translationP,
   1.578 +  print_ast_translationP, token_translationP, oracleP,
   1.579    (*proof commands*)
   1.580    theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
   1.581    factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,